About the rewriting systems produced by the Knuth-Bendix completion algorithm

DOI10.1016/0020-0190(83)90009-1zbMath0506.68032OpenAlexW2093318042MaRDI QIDQ1836978

Yves Métivier

Publication date: 1983

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0020-0190(83)90009-1

zbMATH Keywords

congruencecomplete rewriting systemfree F-algebra

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Related Items

Efficient ground completion ⋮ Equivalences and transformations of regular systems - applications to recursive program schemes and grammars ⋮ Termination of rewriting ⋮ History and basic features of the critical-pair/completion procedure ⋮ Computing a Gröbner basis of a polynomial ideal over a Euclidean domain ⋮ Multi-completion with termination tools ⋮ Higher-dimensional normalisation strategies for acyclicity ⋮ Rigid E-unification: NP-completeness and applications to equational matings ⋮ How to decide the lark ⋮ On interreduction of semi-complete term rewriting systems ⋮ Calcul de longueurs de chaînes de réécriture dans le monoïde libre ⋮ Abstract canonical presentations ⋮ Unnamed Item ⋮ Confluence by critical pair analysis revisited ⋮ On the descriptive power of term rewriting systems ⋮ Polygraphs of finite derivation type ⋮ On the duality of abduction and model generation in a framework for model generation with equality

Cites Work

• A complete proof of correctness of the Knuth-Bendix completion algorithm
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Unnamed Item
• Unnamed Item