A Framework for Developing Stand-Alone Certifiers

AbstractCurrent 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