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

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

Cites work

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

Cited in

(55)

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

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)