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.

BibTeX

@inproceedings{TSSWHZ-CPP15,
  author    = "Thomas Sternagel and Sarah Winkler and Harald Zankl",
  title     = "Recording Completion for Certificates in Equational
               Reasoning",
  booktitle = "Proceedings of the 4th ACM-SIGPLAN Conference on Certified
               Programs and Proofs",
  editor    = "Xavier Leroy and Alwen Tiu",
  pages     = "41--47",
  year      = 2015,
  doi       = "10.1145/2676724.2693171"
}