Proof Verification with GDV and LambdaPi
It's a Matter of Trust
Abstract
Automated Theorem Proving (ATP) is concerned with the development and use of software that
automates sound reasoning.
An ATP system can be required to output a proof that serves as a certificate for the system's
claim.
To ensure that a proof is correct, verification can be required.
If the verifier outputs evidence in a form that can be independently checked, that evidence serves
as a certificate for the verifier's claim.
The sequence of finding a proof, verifying the proof, and certifying the verification, builds an
increasing level of trust in the system.
This talk traces one such path for TPTP format proofs generated by ATP systems, via the GDV
derivation verifier, and ending at the LambdaPi checker.