Schematization of infinite sets of rewrite rules generated by divergent completion processes

DOI10.1016/0304-3975(89)90007-8zbMath0686.68025OpenAlexW2118813891WikidataQ126536349 ScholiaQ126536349MaRDI QIDQ1262755

Hélène Kirchner

Publication date: 1989

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

Full work available at URL: https://doi.org/10.1016/0304-3975(89)90007-8

zbMATH Keywords

term-rewriting systemsKnuth-Bendix completion procedure

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Abstract data types; algebraic specification (68Q65) Thue and Post systems, etc. (03D03)

Related Items

Confluence of terminating membership conditional TRS, A strategy to deal with divergent rewrite systems, A new approach to general E-unification based on conditional rewriting systems, On finite representations of infinite sequences of terms, Meta-rule synthesis from crossed rewrite systems, Proving equational and inductive theorems by completion and embedding techniques, Unification of infinite sets of terms schematized by primal grammars, On the non-termination of MDG-based abstract state enumeration, Chain properties of rule closures, Solving divergence in Knuth--Bendix completion by enriching signatures, Completion of rewrite systems with membership constraints

Uses Software

• 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
• Termination of rewriting systems by polynomial interpretations and its implementation
• Unification under associativity and idempotence is of type nullary
• Orderings for term-rewriting systems
• Proofs by induction in equational theories with constructors
• About the descriptive power of certain classes of finite string-rewriting systems
• Chain properties of rule closures
• A finite Thue system with decidable word problem and without equivalent finite canonical system
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• Rewriting systems on FP expressions to reduce the number of sequences yielded
• Complete sets of unifiers and matchers in equational theories
• Existence, Uniqueness, and Construction of Rewrite Systems
• Completion of a Set of Rules Modulo a Set of Equations
• Programming with Equations