Existence, Uniqueness, and Construction of Rewrite Systems
From MaRDI portal
Publication:3806799
DOI10.1137/0217039zbMath0658.68029OpenAlexW2022122724MaRDI QIDQ3806799
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
terminationequational theoriesKnuth-Bendix completion procedureterm-rewriting system modulo a congruence
Abstract data types; algebraic specification (68Q65) Mechanization of proofs and logical operations (03B35) Equational logic, Mal'tsev conditions (08B05) Equational classes, universal algebra in model theory (03C05)
Related Items (9)
Linear completion ⋮ Effective codescent morphisms in the varieties determined by convergent term rewriting systems. ⋮ Divergence phenomena during completion ⋮ Open problems in rewriting ⋮ Multi-completion with termination tools ⋮ Canonical Inference for Implicational Systems ⋮ Canonical Ground Horn Theories ⋮ Abstract canonical presentations ⋮ Schematization of infinite sets of rewrite rules generated by divergent completion processes
This page was built for publication: Existence, Uniqueness, and Construction of Rewrite Systems
