A note on simplification orderings

DOI10.1016/0020-0190(79)90071-1zbMath0433.68044OpenAlexW1999927144MaRDI QIDQ1139374

Nachum Dershowitz

Publication date: 1979

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2027/uiuo.ark:/13960/t8jd6fq9h

zbMATH Keywords

terminationterm-rewriting system

Mathematics Subject Classification ID

Artificial intelligence (68T99) Theory of computing (68Q99)

Related Items (33)

Generalized sufficient conditions for modular termination of rewriting ⋮ Simulating Buchberger's algorithm by Knuth-Bendix completion ⋮ Termination of constructor systems ⋮ On the modularity of termination of term rewriting systems ⋮ Buchberger's algorithm: The term rewriter's point of view ⋮ Termination of rewriting ⋮ History and basic features of the critical-pair/completion procedure ⋮ A bibliography of quantifier elimination for real closed fields ⋮ Proving termination of context-sensitive rewriting by transformation ⋮ Polynomials over the reals in proofs of termination : from theory to practice ⋮ Orderings for term-rewriting systems ⋮ Size-based termination of higher-order rewriting ⋮ An improved general path order ⋮ Some general results about proof normalization ⋮ Simple termination of rewrite systems ⋮ Termination of just/fair computations in term rewriting ⋮ An analysis of loop checking mechanisms for logic programs ⋮ The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques ⋮ Unnamed Item ⋮ Canonical Ground Horn Theories ⋮ Well rewrite orderings and well quasi-orderings ⋮ Monotonicity Criteria for Polynomial Interpretations over the Naturals ⋮ On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting ⋮ Simple termination revisited ⋮ Explicit substitution. On the edge of strong normalization ⋮ Derivational complexity and context-sensitive Rewriting ⋮ Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms* ⋮ Real or natural number interpretation and their effect on complexity ⋮ Algebra of communicating processes with abstraction ⋮ Modular termination proofs for rewriting using dependency pairs ⋮ Generating polynomial orderings ⋮ Termination orderings for associative-commutative rewriting systems ⋮ Proving termination of (conditional) rewrite systems. A semantic approach

Cites Work

• Proving termination with multiset orderings
• Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A note on simplification orderings