A complete proof of correctness of the Knuth-Bendix completion algorithm

Decidability of theories and sets of sentences (03B25) Abstract data types; algebraic specification (68Q65) Algebraic structures (08A99) Algorithms in computer science (68W99)

Cites work

scientific article; zbMATH DE number 3299786 (Why is no real title available?)
Complete Sets of Reductions for Some Equational Theories
Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
New decision algorithms for finitely presented commutative semigroups

Cited in

(55)

A completion procedure for conditional equations
About the rewriting systems produced by the Knuth-Bendix completion algorithm
On fairness of completion-based theorem proving strategies
Problems in rewriting III
Rewrite method for theorem proving in first order theory with equality
Larry Wos: visions of automated reasoning
Set of support, demodulation, paramodulation: a historical perspective
A superposition oriented theorem prover
Meta-rule synthesis from crossed rewrite systems
Analysis of Dehn's algorithm by critical pairs
Chain properties of rule closures
scientific article; zbMATH DE number 3821100 (Why is no real title available?)
Pregeometric spaces from Wolfram model rewriting systems as homotopy types
Open problems in rewriting
Complete equational unification based on an extension of the Knuth-Bendix completion procedure
Canonical ground Horn theories
Schematization of infinite sets of rewrite rules generated by divergent completion processes
Effective codescent morphisms in the varieties determined by convergent term rewriting systems.
Refutational theorem proving using term-rewriting systems
Buchberger's algorithm: The term rewriter's point of view
Formalising confluence in PVS
A categorical formulation for critical-pair/completion procedures
Towards a foundation of completion procedures as semidecision procedures
Theorem-proving with resolution and superposition
Automatic proofs by induction in theories without constructors
A rewriting approach to satisfiability procedures.
On proving properties of completion strategies
Automating inductionless induction using test sets
Essential unifiers
Rewriting Systems and Embedding of Monoids in Groups
Unnecessary inferences in associative-commutative completion procedures
Completion for unification
Strong normalisation in the \(\pi\)-calculus
Completion for multiple reduction orderings
Fuzzy term-rewriting system
Equational completion in order-sorted algebras
History and basic features of the critical-pair/completion procedure
Model-theoretic aspects of unification
Abstract canonical presentations
Rewrite systems for varieties of semigroups
Canonicity!
On how to move mountains ‘associatively and commutatively’
Equational methods in first order predicate calculus
Critical pair criteria for completion
Completion procedures as semidecision procedures
Chain properties of rule closures
On interreduction of semi-complete term rewriting systems
Partial completion of equational theories
scientific article; zbMATH DE number 3926235 (Why is no real title available?)
The Maude strategy language
scientific article; zbMATH DE number 6712184 (Why is no real title available?)
A strong restriction of the inductive completion procedure
Linear completion
On merging software extensions
On solving the equality problem in theories defined by Horn clauses

This page was built for publication: A complete proof of correctness of the Knuth-Bendix completion algorithm

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