Termination of rewriting

DOI10.1016/S0747-7171(87)80022-6zbMath0637.68035DBLPjournals/jsc/Dershowitz87WikidataQ56814378 ScholiaQ56814378MaRDI QIDQ1098624

Nachum Dershowitz

Publication date: 1987

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

surveyterm rewritingrewrite rulesorderings on termstermination proofs

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Abstract data types; algebraic specification (68Q65)

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

Termination of term rewriting by interpretation ⋮ Path orderings for termination of associative-commutative rewriting ⋮ Trace rewriting systems ⋮ A calculus for conditional inductive theorem proving ⋮ A maximal-literal unit strategy for horn clauses ⋮ A proof system for conditional algebraic specifications ⋮ A survey of ordinal interpretations of type ɛ0 for termination of rewriting systems ⋮ Meta-rule synthesis from crossed rewrite systems ⋮ Completion procedures as semidecision procedures ⋮ Clausal rewriting ⋮ Term rewriting and its application to recognizing handwritten Hindu numerals ⋮ Relative termination via dependency pairs ⋮ Trees, ordinals and termination ⋮ Automatically Proving and Disproving Feasibility Conditions ⋮ From Outermost Reduction Semantics to Abstract Machine ⋮ Reducing Relative Termination to Dependency Pair Problems ⋮ Proof normalization for resolution and paramodulation ⋮ An equational logic sampler ⋮ Embedding with patterns and associated recursive path ordering ⋮ Efficient ground completion ⋮ Adding algebraic rewriting to the untyped lambda calculus (extended abstract) ⋮ Incremental termination proofs and the length of derivations ⋮ An efficient representation of arithmetic for term rewriting ⋮ Decidability of confluence and termination of monadic term rewriting systems ⋮ Proving equational and inductive theorems by completion and embedding techniques ⋮ Simulating Buchberger's algorithm by Knuth-Bendix completion ⋮ Topics in termination ⋮ A precedence-based total AC-compatible ordering ⋮ Linear interpretations by counting patterns ⋮ Automatic termination proofs with transformation orderings ⋮ Combination of constraint solving techniques: An algebraic point of view ⋮ Generating polynomial orderings for termination proofs ⋮ Termination of constructor systems ⋮ On the termination problem for one-rule semi-Thue system ⋮ Dummy elimination: Making termination easier ⋮ Modular and incremental proofs of AC-termination ⋮ Polynomials over the reals in proofs of termination : from theory to practice ⋮ On explicit substitution with names ⋮ Inductive synthesis of term rewriting systems ⋮ E-Unification based on Generalized Embedding ⋮ Applying term rewriting methods to finite groups ⋮ Optimization of rewriting and complexity of rewriting ⋮ AC-Termination of rewrite systems: A modified Knuth-Bendix ordering ⋮ Proving termination of general Prolog programs ⋮ First order data types and first order logic ⋮ Higher order conditional rewriting and narrowing ⋮ Solving simplification ordering constraints ⋮ On termination of graph rewriting ⋮ The complexity of counting problems in equational matching ⋮ Unnamed Item ⋮ Deciding Innermost Loops ⋮ Fast offline partial evaluation of logic programs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Proving Group Protocols Secure Against Eavesdroppers ⋮ The order types of termination orderings on monadic terms, strings and multisets ⋮ The Ideal Approach to Computing Closed Subsets in Well-Quasi-orderings ⋮ Strong WQO Tree Theorems ⋮ Extension orderings ⋮ Termination of theorem proving by reuse ⋮ Theorem proving with group presentations: Examples and questions ⋮ Transforming termination by self-labelling ⋮ Constructing Bachmair-Ganzinger Models ⋮ Automatic Proofs of Termination With Elementary Interpretations ⋮ Essentials of Term Graph Rewriting ⋮ \(\exists\)-Universal termination of logic programs ⋮ Regular path expressions in feature logic ⋮ Simple termination is difficult ⋮ Any ground associative-commutative theory has a finite canonical system ⋮ Termination Graphs for Java Bytecode ⋮ Preuves de terminaison de systèmes de réécriture fondées sur les interprétations polynomiales. Une méthode basée sur le théorème de Sturm ⋮ Derivation lengths and order types of Knuth--Bendix orders ⋮ Proof Relevant Corecursive Resolution ⋮ Termination of Narrowing in Left-Linear Constructor Systems ⋮ Mechanizable inductive proofs for a class of ∀ ∃ formulas ⋮ Simple termination revisited ⋮ Termination orderings for rippling ⋮ A completion-based method for mixed universal and rigid E-unification ⋮ Total termination of term rewriting ⋮ Chain properties of rule closures ⋮ Non-Looping String Rewriting ⋮ Dependent choice as a termination principle ⋮ Termination proofs by multiset path orderings imply primitive recursive derivation lengths ⋮ Extensions of arithmetic for proving termination of computations ⋮ Proving Termination with (Boolean) Satisfaction ⋮ Termination Analysis of Logic Programs Based on Dependency Graphs ⋮ Termination Analysis of CHR Revisited ⋮ Search Techniques for Rational Polynomial Orders ⋮ One-rule semi-Thue systems with loops of length one, two or three ⋮ The size-change principle and dependency pairs for termination of term rewriting ⋮ Modular and incremental automated termination proofs ⋮ Termination analysis for partial functions ⋮ Interaction nets and term rewriting systems (extended abstract) ⋮ Termination by absence of infinite chains of dependency pairs ⋮ 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

Uses Software

• RRL
• REVE

Cites Work

• 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
• 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

This page was built for publication: Termination of rewriting