Recording Completion for Certificates in Equational Reasoning

Abstract

We introduce recording completion, a variant of Knuth-Bendix completion which facilitates the construction of certificates for various equational logic proofs (completion proofs, entailment proofs and dis-proofs). The approach generalizes to more powerful variants of completion such as ordered completion and AC completion. We implemented recording completion in the tools KBCV and MKBTT. Both tools allow to choose among different formats of proof certificates, namely conversions, proof trees, and conversions with history. We report on experimental results in which all generated certificates have been verified by the trustable checker CeTA.