Orderings for term-rewriting systems
From MaRDI portal
Cites work
- A note on simplification orderings
- Algebraic simplification
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- Automatic Proofs of Theorems in Analysis Using Nonstandard Techniques
- Complete Sets of Reductions for Some Equational Theories
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Decision procedures for real and p‐adic fields
- scientific article; zbMATH DE number 3635501 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- scientific article; zbMATH DE number 3198033 (Why is no real title available?)
- scientific article; zbMATH DE number 3068536 (Why is no real title available?)
- New decision algorithms for finitely presented commutative semigroups
- Proving termination with multiset orderings
- Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
Cited in
(only showing first 100 items - show all)- Match-bounds revisited
- A superposition oriented theorem prover
- The undecidability of self-embedding for term rewriting systems
- Algebra of communicating processes with abstraction
- Termination orderings for associative-commutative rewriting systems
- On recursive path ordering
- Reductions in tree replacement systems
- On total regulators generated by derivation relations
- Parameter-preserving data type specifications
- The undecidability of self-embedding for finite semi-Thue and Thue systems
- Termination of rewriting
- Corrigendum to ``Termination of rewriting
- Rewrite method for theorem proving in first order theory with equality
- Path of subterms ordering and recursive decomposition ordering revisited
- History and basic features of the critical-pair/completion procedure
- On termination of the direct sum of term-rewriting systems
- A geometrical approach to multiset orderings
- Using unavoidable set of trees to generalize Kruskal's theorem
- A notation for lambda terms. A generalization of environments
- Fuzzy term-rewriting system
- What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory
- Modularity of simple termination of term rewriting systems with shared constructors
- Termination proofs by multiset path orderings imply primitive recursive derivation lengths
- C-expressions: A variable-free calculus for equational logic programming
- A new method for undecidability proofs of first order theories
- Schematization of infinite sets of rewrite rules generated by divergent completion processes
- Complexity analysis of term-rewriting systems
- Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
- Simplification orderings: Putting them to the test
- Rewriting systems of Coxeter groups
- Proving termination of (conditional) rewrite systems. A semantic approach
- Generalized sufficient conditions for modular termination of rewriting
- Automated deduction with associative-commutative operators
- Weights for total division orderings on strings
- Abstract data type systems
- Simple termination of rewrite systems
- A fully syntactic AC-RPO.
- A characterisation of multiply recursive functions with Higman's lemma.
- Analysing the implicit complexity of programs.
- Superposition with completely built-in abelian groups
- Correspondences between classical, intuitionistic and uniform provability
- Invariants, patterns and weights for ordering terms
- Richer types for \(Z\)
- Proof of termination of the rewriting system SUBSET on CCL
- Induction = I-axiomatization + first-order consistency.
- Pattern matching as cut elimination
- Deciding confluence of certain term rewriting systems in polynomial time
- A calculus for and termination of rippling
- Linear and unit-resulting refutations for Horn theories
- An improved general path order
- Jumping and escaping: modular termination and the abstract path ordering
- Determinization of conditional term rewriting systems
- Superposition decides the first-order logic fragment over ground theories
- Termination of term rewriting using dependency pairs
- Set of support, demodulation, paramodulation: a historical perspective
- An efficient subsumption test pipeline for BS(LRA) clauses
- Term orderings for non-reachability of (conditional) rewriting
- Minimal bad sequences are necessary for a uniform Kruskal theorem
- Regaining cut admissibility in deduction modulo using abstract completion
- Dependent choice as a termination principle
- SAT solving for termination proofs with recursive path orders and dependency pairs
- Drags: a compositional algebraic framework for graph rewriting
- Enhancing dependency pair method using strong computability in simply-typed term rewriting
- Abstract canonical presentations
- Normal forms for binary relations
- The undecidability of iterated modal relativization
- Higher-order interpretations and program complexity
- Outermost ground termination
- Proving termination of context-sensitive rewriting with MU-TERM
- On quasi-interpretations, blind abstractions and implicit complexity
- Normal higher-order termination
- The logic of public announcements, common knowledge, and private suspicions
- Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
- AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
- scientific article; zbMATH DE number 3860380 (Why is no real title available?)
- Theories of orders on the set of words
- History and prospects for first-order automated deduction
- Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
- Termination Proof of S-Expression Rewriting Systems with Recursive Path Relations
- Paramodulation with non-monotonic orderings and simplification
- The Computability Path Ordering: The End of a Quest
- 10th Asian Logic Conference
- Upper Bounds on Stream I/O Using Semantic Interpretations
- scientific article; zbMATH DE number 3821100 (Why is no real title available?)
- scientific article; zbMATH DE number 3926235 (Why is no real title available?)
- Logic and functional programming by retractions : operational semantics
- The order types of termination orderings on monadic terms, strings and multisets
- Finite complete rewriting systems for groups
- On deciding satisfiability by theorem proving with speculative inferences
- Size-based termination of higher-order rewriting
- CLP(\(\mathsf{H}\)): constraint logic programming for hedges
- AC-KBO revisited
- R n - and G n -logics
- Theorem proving with group presentations: examples and questions
- Transforming termination by self-labelling
- Algebra and automated deduction
- Walther recursion
- Defining recursive predicates in graph orders
- Canonicity1 1This research was supported in part by the Israel Science Foundation (grant no. 254/01).
This page was built for publication: Orderings for term-rewriting systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q593789)
