Critical pair criteria for completion

DOI10.1016/S0747-7171(88)80018-XzbMath0651.68030MaRDI QIDQ1106659

Leo Bachmair, Nachum Dershowitz

Publication date: 1988

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

Knuth-Bendix completioncritical pairequational inference systemorderings on equational proofs

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Related Items

Relative termination via dependency pairs, Computing ground reducibility and inductively complete positions, Consider only general superpositions in completion procedures, Simulating Buchberger's algorithm by Knuth-Bendix completion, AC-complete unification and its application to theorem proving, Confluence of terminating conditional rewrite systems revisited, Buchberger's algorithm: The term rewriter's point of view, The CADE-28 Automated Theorem Proving System Competition – CASC-28, Multi-completion with termination tools, Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties, Automated proofs of the Moufang identities in alternative rings, The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9, Towards a foundation of completion procedures as semidecision procedures, Redundancy criteria for constrained completion, Harald Ganzinger’s Legacy: Contributions to Logics and Programming, Redundancy criteria for constrained completion, On pot, pans and pudding or how to discover generalised critical Pairs, Completion for rewriting modulo a congruence, Blocking and other enhancements for bottom-up model generation methods, Twee: an equational theorem prover, On the modelling of search in theorem proving -- towards a theory of strategy analysis, Ground joinability and connectedness in the superposition calculus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proofs by induction in equational theories with constructors
• Refutational theorem proving using term-rewriting systems
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• Computing with rewrite systems
• Completion of a Set of Rules Modulo a Set of Equations
• Proving termination with multiset orderings
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Complete Sets of Reductions for Some Equational Theories
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity