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

Title not available (Why is that?)
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)

Pregeometric spaces from Wolfram model rewriting systems as homotopy types
The Maude strategy language
About the rewriting systems produced by the Knuth-Bendix completion algorithm
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
Meta-rule synthesis from crossed rewrite systems
A superposition oriented theorem prover
Analysis of Dehn's algorithm by critical pairs
Title not available (Why is that?)
Chain properties of rule closures
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.
Formalising confluence in PVS
Refutational theorem proving using term-rewriting systems
Buchberger's algorithm: The term rewriter's point of view
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
On proving properties of completion strategies
A rewriting approach to satisfiability procedures.
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
Equational completion in order-sorted algebras
Fuzzy term-rewriting system
Model-theoretic aspects of unification
History and basic features of the critical-pair/completion procedure
Rewrite systems for varieties of semigroups
Canonicity!
Abstract canonical presentations
On how to move mountains ‘associatively and commutatively’
Completion procedures as semidecision procedures
Equational methods in first order predicate calculus
On interreduction of semi-complete term rewriting systems
Chain properties of rule closures
Critical pair criteria for completion
Partial completion of equational theories
Title not available (Why is that?)
Title not available (Why is that?)
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
On fairness of completion-based theorem proving strategies
Problems in rewriting III
A completion procedure for conditional equations

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)