cl-banner

Recording Completion for Certificates in Equational Reasoning

Thomas Sternagel, Sarah Winkler, and Harald Zankl

Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP 2015), pp. 41 – 47, 2015.

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.

 

  PDF |    doi:10.1145/2676724.2693171  |  © Creative Commons License – NC – ND

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"
Nach oben scrollen