Critical pair criteria for completion (Q1106659)

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).