Existence, Uniqueness, and Construction of Rewrite Systems

DOI10.1137/0217039MaRDI QIDQ3806799zbMATH OpenOpenAlexFDO

Authors Nachum Dershowitz, Leo Marcus, Andrzej Tarlecki

Publication date 1988

Published in SIAM Journal on Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1137/0217039

zbMATH Keywords

equational theoriesKnuth-Bendix completion procedureterm-rewriting system modulo a congruencetermination

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Equational classes, universal algebra in model theory (03C05) Equational logic, Mal'tsev conditions (08B05) Abstract data types; algebraic specification (68Q65)

Recommendations

• scientific article; zbMATH DE number 3890721
• The Knuth-Bendix Completion Procedure and Thue Systems
• A Completion Method to Decide Reachability in Rewrite Systems
• Completion of a Set of Rules Modulo a Set of Equations
• scientific article; zbMATH DE number 4016226

Cited in

(20)

• Schematization of infinite sets of rewrite rules generated by divergent completion processes
• A finiteness condition for rewriting systems
• A property of left-linear rewrite systems preserving recognizability
• Rewriting systems over similarity and generalized pseudometric spaces and their properties
• Invariants and closures in the theory of rewrite systems
• Abstract canonical presentations
• Effective codescent morphisms in the varieties determined by convergent term rewriting systems.
• Multi-completion with termination tools
• Canonical Inference for Implicational Systems
• scientific article; zbMATH DE number 5708984 (Why is no real title available?)
• Antimirov and Mosses’s Rewrite System Revisited
• scientific article; zbMATH DE number 67429 (Why is no real title available?)
• J-SYSTEM RECONSTRUCT/ABILITY: A FORMALIZED STUDY
• scientific article; zbMATH DE number 1373518 (Why is no real title available?)
• Canonical ground Horn theories
• scientific article; zbMATH DE number 1419256 (Why is no real title available?)
• Divergence phenomena during completion
• Open problems in rewriting
• An Automated Confluence Proof for an Infinite Rewrite System Parametrized over an Integro-Differential Algebra
• Linear completion

This page was built for publication: Existence, Uniqueness, and Construction of Rewrite Systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3806799)