Schematization of infinite sets of rewrite rules generated by divergent completion processes
From MaRDI portal
Publication:1262755
DOI10.1016/0304-3975(89)90007-8zbMath0686.68025OpenAlexW2118813891WikidataQ126536349 ScholiaQ126536349MaRDI QIDQ1262755
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
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
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