Orderings for term-rewriting systems

DOI10.1016/0304-3975(82)90026-3zbMath0525.68054OpenAlexW2086747974WikidataQ56814377 ScholiaQ56814377MaRDI QIDQ593789

Publication date: 1982

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(82)90026-3

zbMATH Keywords

term-rewriting systems termination simplification ordering term ordering

Mathematics Subject Classification ID

Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).

Related Items (only showing first 100 items - show all)

Combinations of simplifying conditional term rewriting systems ⋮ Sufficient conditions for modular termination of conditional term rewriting systems ⋮ Termination of combined (rewrite and λ-calculus) systems ⋮ Implementing contextual rewriting ⋮ Conditional rewriting in focus ⋮ A maximal-literal unit strategy for horn clauses ⋮ On finite representations of infinite sequences of terms ⋮ Proof by consistency in conditional equational theories ⋮ An universal termination condition for solving goals in equational languages ⋮ Trees, ordinals and termination ⋮ History and Prospects for First-Order Automated Deduction ⋮ Proof normalization for resolution and paramodulation ⋮ An overview of LP, the Larch Prover ⋮ A local termination property for term rewriting systems ⋮ Embedding with patterns and associated recursive path ordering ⋮ Rewriting techniques for program synthesis ⋮ Extensions and comparison of simplification orderings ⋮ Incremental termination proofs and the length of derivations ⋮ Time bounded rewrite systems and termination proofs by generalized embedding ⋮ On fairness of completion-based theorem proving strategies ⋮ Topics in termination ⋮ Linear interpretations by counting patterns ⋮ A termination ordering for higher order rewrite systems ⋮ A complete characterization of termination of 0p 1q→1r 0s ⋮ Generating polynomial orderings for termination proofs ⋮ Termination of constructor systems ⋮ A recursive path ordering for higher-order terms in η-long β-normal form ⋮ Dummy elimination: Making termination easier ⋮ Unnamed Item ⋮ Polynomials over the reals in proofs of termination : from theory to practice ⋮ Unnamed Item ⋮ E-Unification based on Generalized Embedding ⋮ Size-based termination of higher-order rewriting ⋮ CLP(H):Constraint logic programming for hedges ⋮ AC-KBO revisited ⋮ Complete equational unification based on an extension of the Knuth-Bendix completion procedure ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Unnamed Item ⋮ The Logic of Public Announcements, Common Knowledge, and Private Suspicions ⋮ Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities ⋮ Termination Proof of S-Expression Rewriting Systems with Recursive Path Relations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The Computability Path Ordering: The End of a Quest ⋮ The order types of termination orderings on monadic terms, strings and multisets ⋮ Canonized Rewriting and Ground AC Completion Modulo Shostak Theories ⋮ Unnamed Item ⋮ Logic and functional programming by retractions : operational semantics ⋮ 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 ⋮ Finite complete rewriting systems for groups ⋮ AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS ⋮ Canonicity1 1This research was supported in part by the Israel Science Foundation (grant no. 254/01). ⋮ Gap Embedding for Well-Quasi-Orderings ⋮ Unnamed Item ⋮ Termination Tools in Ordered Completion ⋮ Combinable Extensions of Abelian Groups ⋮ A general framework to build contextual cover set induction provers ⋮ Two applications of analytic functors ⋮ On the longest perpetual reductions in orthogonal expression reduction systems ⋮ Simple termination revisited ⋮ Termination orderings for rippling ⋮ Theories of orders on the set of words ⋮ 10th Asian Logic Conference ⋮ CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates ⋮ Termination proofs by multiset path orderings imply primitive recursive derivation lengths ⋮ Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered ⋮ Upper Bounds on Stream I/O Using Semantic Interpretations ⋮ Transforming SAT into Termination of Rewriting ⋮ From Kruskal’s theorem to Friedman’s gap condition ⋮ Proving Termination with (Boolean) Satisfaction ⋮ Generalized sufficient conditions for modular termination of rewriting ⋮ Higher-order interpretations and program complexity ⋮ Minimal bad sequences are necessary for a uniform Kruskal theorem ⋮ On recursive path ordering ⋮ Reductions in tree replacement systems ⋮ On total regulators generated by derivation relations ⋮ Pattern matching as cut elimination ⋮ Deciding confluence of certain term rewriting systems in polynomial time ⋮ Automated deduction with associative-commutative operators ⋮ Parameter-preserving data type specifications ⋮ The undecidability of self-embedding for finite semi-Thue and Thue systems ⋮ Weights for total division orderings on strings ⋮ Coq formalization of the higher-order recursive path ordering ⋮ Termination of rewriting ⋮ Corrigendum to ``Termination of rewriting ⋮ Rewrite method for theorem proving in first order theory with equality ⋮ On quasi-interpretations, blind abstractions and implicit complexity ⋮ Path of subterms ordering and recursive decomposition ordering revisited ⋮ Termination of string rewriting proved automatically ⋮ Mechanically proving termination using polynomial interpretations ⋮ History and basic features of the critical-pair/completion procedure ⋮ An effective proof of the well-foundedness of the multiset path ordering ⋮ Proving termination of context-sensitive rewriting by transformation ⋮ On termination of the direct sum of term-rewriting systems ⋮ SAT solving for termination proofs with recursive path orders and dependency pairs

Uses Software

Cites Work

This page was built for publication: Orderings for term-rewriting systems