Critical pair criteria for completion
From MaRDI portal
We formulate the Knuth-Bendix completion method at an abstract level, as an equational inference system, and formalize the notion of critical pair criterion using orderings on equational proofs. We prove the correctness of standard completion and verify all known criteria for completion, including those for which correctness had not been established previously. What distinguishes our approach from others is that our results apply to a large class of completion procedures, not just to a particular version. Proof ordering techniques therefore provide a basis for the design and verification of specific completion procedures (with or without criteria).
Recommendations
Cites work
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- Complete Sets of Reductions for Some Equational Theories
- Completion of a Set of Rules Modulo a Set of Equations
- Computing with rewrite systems
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- scientific article; zbMATH DE number 3649988 (Why is no real title available?)
- scientific article; zbMATH DE number 3870585 (Why is no real title available?)
- scientific article; zbMATH DE number 3896290 (Why is no real title available?)
- scientific article; zbMATH DE number 3928345 (Why is no real title available?)
- scientific article; zbMATH DE number 3928346 (Why is no real title available?)
- scientific article; zbMATH DE number 3981150 (Why is no real title available?)
- scientific article; zbMATH DE number 4078851 (Why is no real title available?)
- scientific article; zbMATH DE number 43246 (Why is no real title available?)
- scientific article; zbMATH DE number 44069 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- Proofs by induction in equational theories with constructors
- Proving termination with multiset orderings
- Refutational theorem proving using term-rewriting systems
Cited in
(35)- A criterion for proving noetherianity of a relation
- Completion for rewriting modulo a congruence
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- Buchberger's algorithm: The term rewriter's point of view
- Declarative representation of algorithms of completion by critical pairs
- Proof lengths for equational completion
- Twee: an equational theorem prover
- Ground joinability and connectedness in the superposition calculus
- Blocking and other enhancements for bottom-up model generation methods
- Relative termination via dependency pairs
- Encoding dependency pair techniques and control strategies for maximal completion
- Multi-completion with termination tools
- scientific article; zbMATH DE number 3952003 (Why is no real title available?)
- scientific article; zbMATH DE number 4076598 (Why is no real title available?)
- scientific article; zbMATH DE number 4090851 (Why is no real title available?)
- Equational inference, canonical proofs, and proof orderings
- scientific article; zbMATH DE number 778200 (Why is no real title available?)
- Harald Ganzinger's legacy: contributions to logics and programming
- Computing ground reducibility and inductively complete positions
- Consider only general superpositions in completion procedures
- Simulating Buchberger's algorithm by Knuth-Bendix completion
- Redundancy criteria for constrained completion
- AC-complete unification and its application to theorem proving
- Confluence of terminating conditional rewrite systems revisited
- The CADE-28 Automated Theorem Proving System Competition – CASC-28
- The 9th IJCAR automated theorem proving system competition -- CASC-J9
- On pot, pans and pudding or how to discover generalised critical pairs
- A categorical formulation for critical-pair/completion procedures
- Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
- Proof transformation for non-compatible rewriting
- Towards a foundation of completion procedures as semidecision procedures
- Redundancy criteria for constrained completion
- Partial redundancy in saturation
- Reducibility constraints in superposition
- Automated proofs of the Moufang identities in alternative rings
This page was built for publication: Critical pair criteria for completion
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1106659)
