Termination of rewriting
From MaRDI portal
Publication:1098624
DOI10.1016/S0747-7171(87)80022-6zbMath0637.68035WikidataQ56814378 ScholiaQ56814378MaRDI QIDQ1098624
Publication date: 1987
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Symbolic computation and algebraic computation (68W30) Abstract data types; algebraic specification (68Q65)
Related Items (only showing first 100 items - show all)
Generalized sufficient conditions for modular termination of rewriting ⋮ Rewriting modulo isotopies in pivotal linear \((2,2)\)-categories ⋮ On termination of confluent one-rule string-rewriting systems ⋮ The translation power of top-down tree-to-graph transducers ⋮ Some results on the confluence property of combined term rewriting systems ⋮ An overview of the Tecton proof system ⋮ Simple termination is difficult ⋮ On the termination of clause graph resolution ⋮ The data type variety of stack algebras ⋮ A path ordering for proving termination of AC rewrite systems ⋮ Weights for total division orderings on strings ⋮ Head boundedness of nonterminating rewritings ⋮ Ensuring the quasi-termination of needed narrowing computations ⋮ Buchberger's algorithm: The term rewriter's point of view ⋮ Proving Ramsey's theory by the cover set induction: A case and comparision study. ⋮ Termination proofs for string rewriting systems via inverse match-bounds ⋮ Extension functions for multiset orderings ⋮ Proving termination of context-sensitive rewriting by transformation ⋮ On termination of the direct sum of term-rewriting systems ⋮ Decision procedures for the security of protocols with probabilistic encryption against offline dictionary attacks ⋮ Total termination of term rewriting ⋮ New uses of linear arithmetic in automated theorem proving by induction ⋮ A calculus for and termination of rippling ⋮ Leanest quasi-orderings ⋮ Unification in sort theories and its applications ⋮ Mechanizing and improving dependency pairs ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Combination of constraint solvers for free and quasi-free structures ⋮ Reasoning with conditional axioms ⋮ An improved general path order ⋮ Jumping and escaping: modular termination and the abstract path ordering ⋮ Interaction nets and term-rewriting systems ⋮ Simple termination of rewrite systems ⋮ The first-order theory of lexicographic path orderings is undecidable ⋮ Unification of infinite sets of terms schematized by primal grammars ⋮ Practical algorithms for deciding path ordering constraint satisfaction. ⋮ Analysing the implicit complexity of programs. ⋮ Constraint-based correctness proofs for logic program transformations ⋮ Modular term rewriting systems and the termination ⋮ The derivational complexity of string rewriting systems ⋮ Equational completion in order-sorted algebras ⋮ On the recursive decomposition ordering with lexicographical status and other related orderings ⋮ Automated proofs of the Moufang identities in alternative rings ⋮ Weighted graphs: A tool for studying the halting problem and time complexity in term rewriting systems and logic programming ⋮ Chain properties of rule closures ⋮ A note on division orderings on strings ⋮ Rigid E-unification: NP-completeness and applications to equational matings ⋮ Overlap closures do not suffice for termination of general term rewriting systems ⋮ Binary decision diagrams for first-order predicate logic. ⋮ Termination of just/fair computations in term rewriting ⋮ Rewriting modulo isotopies in Khovanov-Lauda-Rouquier's categorification of quantum groups ⋮ Efficient solution of a class of quantified constraints with quantifier prefix exists-forall ⋮ What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory ⋮ Termination of term rewriting using dependency pairs ⋮ Some experiments with a completion theorem prover ⋮ Using induction and rewriting to verify and complete parameterized specifications ⋮ Modular termination of \(r\)-consistent and left-linear term rewriting systems ⋮ Towards a foundation of completion procedures as semidecision procedures ⋮ Loop detection in term rewriting using the eliminating unfoldings ⋮ Natural termination ⋮ A total AC-compatible ordering based on RPO ⋮ Some undecidable termination problems for semi-Thue systems ⋮ A combinatory logic approach to higher-order E-unification ⋮ Associative-commutative reduction orderings ⋮ On the complexity of recursive path orderings ⋮ Simulation of Turing machines by a regular rewrite rule ⋮ Termination and completion modulo associativity, commutativity and identity ⋮ Termination proofs by multiset path orderings imply primitive recursive derivation lengths ⋮ A field guide to equational logic ⋮ A general criterion for avoiding infinite unfolding during partial deduction ⋮ Adding algebraic rewriting to the untyped lambda calculus ⋮ Match-bounded string rewriting systems ⋮ Rationality of division orderings ⋮ Well rewrite orderings and well quasi-orderings ⋮ A new method for undecidability proofs of first order theories ⋮ Decision problems for semi-Thue systems with a few rules ⋮ Termination of narrowing via termination of rewriting ⋮ Zero, successor and equality in BDDs ⋮ Totally correct logic program transformations via well-founded annotations ⋮ Complete sets of transformations for general E-unification ⋮ Automating the Knuth Bendix ordering ⋮ Termination by completion ⋮ Using forcing to prove completeness of resolution and paramodulation ⋮ Theorem-proving with resolution and superposition ⋮ A completion procedure for conditional equations ⋮ Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering ⋮ On equational theories, unification, and (un)decidability ⋮ Decidability and complexity analysis by basic paramodulation ⋮ Termination of narrowing revisited ⋮ Pattern-matching algorithms based on term rewrite systems ⋮ Partial completion of equational theories ⋮ On terminating lemma speculations. ⋮ Context-sensitive rewriting strategies ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ Simplification orderings: Putting them to the test ⋮ Modular termination proofs for rewriting using dependency pairs ⋮ Generating polynomial orderings ⋮ Automated proofs of equality problems in Overbeek's competition ⋮ Deductive and inductive synthesis of equational programs ⋮ Proving termination of (conditional) rewrite systems. A semantic approach
Uses Software
Cites Work
- Orderings for term-rewriting systems
- A property which guarantees termination in weak combinatory logic and subtree replacement systems
- On regularity of context-free languages
- The undecidability of self-embedding for term rewriting systems
- Another generalization of Higman's well quasi order result on \(\Sigma ^*\)
- Termination orderings for associative-commutative rewriting systems
- Constructing recursion operators in intuitionistic type theory
- Extension functions for multiset orderings
- Computing in systems described by equations
- A note on simplification orderings
- New decision algorithms for finitely presented commutative semigroups
- On multiset orderings
- About the rewriting systems produced by the Knuth-Bendix completion algorithm
- Calcul de longueurs de chaînes de réécriture dans le monoïde libre
- The theory of well-quasi-ordering: a frequently discovered concept
- Konstruktiver Aufbau eines Abschnitts der zweiten Cantorschen Zahlenklasse
- On theories with a combinatorial definition of 'equivalence'
- On Proving Uniform Termination and Restricted Termination of Rewriting Systems
- Nichtbeweisbarkeit von gewissen kombinatorischen Eigenschaften endlicher Bäume;Unprovability of certain combinatorial properties of finite trees
- Completion of a Set of Rules Modulo a Set of Equations
- Proving termination with multiset orderings
- TREES AND BALL GAMES
- Operational and Semantic Equivalence Between Recursive Programs
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Accessible Independence Results for Peano Arithmetic
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- Extensions of arithmetic for proving termination of computations
- On the Church-Rosser property for the direct sum of term rewriting systems
- Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
- Systems of predicative analysis, II: Representations of ordinals
- Decision procedures for real and p‐adic fields
- Tree-Manipulating Systems and Church-Rosser Theorems
- Ordering by Divisibility in Abstract Algebras
- Partial well‐ordering of sets of vectors
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Termination of rewriting