A complete proof of correctness of the Knuth-Bendix completion algorithm
From MaRDI portal
Publication:1154801
DOI10.1016/0022-0000(81)90002-7zbMath0465.68014OpenAlexW1991856459WikidataQ55952378 ScholiaQ55952378MaRDI QIDQ1154801
Publication date: 1981
Published in: Journal of Computer and System Sciences (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/inria-00076536/file/RR-0025.pdf
Abstract data types; algebraic specification (68Q65) Decidability of theories and sets of sentences (03B25) Algebraic structures (08A99) Algorithms in computer science (68W99)
Related Items
A categorical formulation for critical-pair/completion procedures, Meta-rule synthesis from crossed rewrite systems, Completion procedures as semidecision procedures, Linear completion, Effective codescent morphisms in the varieties determined by convergent term rewriting systems., On merging software extensions, On solving the equality problem in theories defined by Horn clauses, Unnamed Item, 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, Problems in rewriting III, Buchberger's algorithm: The term rewriter's point of view, 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, Strong normalisation in the \(\pi\)-calculus, Unnecessary inferences in associative-commutative completion procedures, The Maude strategy language, Complete equational unification based on an extension of the Knuth-Bendix completion procedure, A rewriting approach to satisfiability procedures., Model-theoretic aspects of unification, Unnamed Item, Equational completion in order-sorted algebras, Chain properties of rule closures, Canonicity!, Completion for unification, Fuzzy term-rewriting system, Unnamed Item, Towards a foundation of completion procedures as semidecision procedures, Canonical Ground Horn Theories, Unnamed Item, On interreduction of semi-complete term rewriting systems, Essential unifiers, Abstract canonical presentations, Rewriting Systems and Embedding of Monoids in Groups, Completion for multiple reduction orderings, Schematization of infinite sets of rewrite rules generated by divergent completion processes, Chain properties of rule closures, Theorem-proving with resolution and superposition, A completion procedure for conditional equations, Automating inductionless induction using test sets, 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, Partial completion of equational theories, A superposition oriented theorem prover, Larry Wos: visions of automated reasoning, Set of support, demodulation, paramodulation: a historical perspective, Refutational theorem proving using term-rewriting systems, Equational methods in first order predicate calculus
Cites Work
