Proof Verification with GDV and LambdaPi - It's a Matter of Trust
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.
Authors
- Frédéric Blanqui (ORCID: https://orcid.org/0000-0001-7438-5554)
- Guillaume Burel
- Geoff Sutcliffe (ORCID: https://orcid.org/0000-0001-9120-3927)
Institutions
- École Normale Supérieure Paris-Saclay (FR)
- Centre National de la Recherche Scientifique (FR)
- University of Miami (US)
- Université Paris-Saclay (FR)
- École Normale Supérieure - PSL (FR)
- École Nationale Supérieure d’Informatique pour l’Industrie et l’Entreprise (FR)
- Laboratoire Spécification et Vérification (FR)
- Laboratoire de Biologie et Pharmacologie Appliquée (FR)
- Télécom SudParis (FR)
Publication Details
- Journal
- Proceedings of the ... International Florida Artificial Intelligence Research Society Conference
- Published
- 2025-05-14
- DOI
- https://doi.org/10.32473/flairs.38.1.138642
- Primary Topic
- Mathematics, Computing, and Information Processing
- Type
- article
- Field-Weighted Citation Impact
- 0.00