Proof Verification with GDV and LambdaPi - It's a Matter of Trust

Geoff Sutcliffe; Frédéric Blanqui; Guillaume Burel

doi:10.32473/flairs.38.1.138642

Proof Verification with GDV and LambdaPi - It's a Matter of Trust

Authors

Geoff Sutcliffe University of Miami https://orcid.org/0000-0001-9120-3927
Frédéric Blanqui Université Paris-Saclay, ENS Paris-Saclay, CNRS, INRIA, Laboratoire Méthodes Formelles https://orcid.org/0000-0001-7438-5554
Guillaume Burel Guillaume Burel Laboratoire Samovar École Nationale Supérieure d’Informatique pour l’Industrie et l’Entreprise

DOI:

https://doi.org/10.32473/flairs.38.1.138642

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 paper traces one such path for TPTP format proofs generated by ATP systems, via the GDV derivation verifier, and ending at the LambdaPi checker.

Downloads

Published

14-05-2025

How to Cite

Sutcliffe, G., Blanqui, F., & Burel, G. (2025). Proof Verification with GDV and LambdaPi - It’s a Matter of Trust. The International FLAIRS Conference Proceedings, 38(1). https://doi.org/10.32473/flairs.38.1.138642