Abstract

Current tools for automated deduction are often powerful and complex. Due to their complexity there is a risk that they contain bugs and thus deliver wrong results. To ensure reliability of these tools, one possibility is to develop certifiers which check the results of tools with the help of a trusted proof assistant. We present a framework which illustrates the essential steps to develop stand-alone certifiers which efficiently check generated proofs outside the employed proof assistant. Our framework has already been used to develop certifiers for various properties, including termination, confluence, completion, and tree automata related properties.

BibTeX

@inproceedings{CSRT-LSFA14,
  author    = "Christian Sternagel and Ren\'e Thiemann",
  title     = "A Framework for Developing Stand-Alone Certifiers",
  booktitle = "Proceedings of the 9th Workshop on
              on Logical and Semantic Frameworks, with Applications",
  journal   = "Electronic Notes in Theoretical Computer Science",
  volume    = 312,
  pages     = "51--67",
  year      = 2015,
  doi       = "10.1016/j.entcs.2015.04.004"
}