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 ver...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
LibraryPress@UF
2025-05-01
|
| Series: | Proceedings of the International Florida Artificial Intelligence Research Society Conference |
| Online Access: | https://journals.flvc.org/FLAIRS/article/view/138642 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849727870645043200 |
|---|---|
| author | Geoff Sutcliffe Frédéric Blanqui Guillaume Burel |
| author_facet | Geoff Sutcliffe Frédéric Blanqui Guillaume Burel |
| author_sort | Geoff Sutcliffe |
| collection | DOAJ |
| description |
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.
|
| format | Article |
| id | doaj-art-f6c4b4e54e13446e848623fd8a13ebb4 |
| institution | DOAJ |
| issn | 2334-0754 2334-0762 |
| language | English |
| publishDate | 2025-05-01 |
| publisher | LibraryPress@UF |
| record_format | Article |
| series | Proceedings of the International Florida Artificial Intelligence Research Society Conference |
| spelling | doaj-art-f6c4b4e54e13446e848623fd8a13ebb42025-08-20T03:09:44ZengLibraryPress@UFProceedings of the International Florida Artificial Intelligence Research Society Conference2334-07542334-07622025-05-0138110.32473/flairs.38.1.138642Proof Verification with GDV and LambdaPi - It's a Matter of TrustGeoff Sutcliffe0https://orcid.org/0000-0001-9120-3927Frédéric Blanqui1https://orcid.org/0000-0001-7438-5554Guillaume Burel2University of MiamiUniversité Paris-Saclay, ENS Paris-Saclay, CNRS, INRIA, Laboratoire Méthodes FormellesGuillaume Burel Laboratoire Samovar École Nationale Supérieure d’Informatique pour l’Industrie et l’Entreprise 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. https://journals.flvc.org/FLAIRS/article/view/138642 |
| spellingShingle | Geoff Sutcliffe Frédéric Blanqui Guillaume Burel Proof Verification with GDV and LambdaPi - It's a Matter of Trust Proceedings of the International Florida Artificial Intelligence Research Society Conference |
| title | Proof Verification with GDV and LambdaPi - It's a Matter of Trust |
| title_full | Proof Verification with GDV and LambdaPi - It's a Matter of Trust |
| title_fullStr | Proof Verification with GDV and LambdaPi - It's a Matter of Trust |
| title_full_unstemmed | Proof Verification with GDV and LambdaPi - It's a Matter of Trust |
| title_short | Proof Verification with GDV and LambdaPi - It's a Matter of Trust |
| title_sort | proof verification with gdv and lambdapi it s a matter of trust |
| url | https://journals.flvc.org/FLAIRS/article/view/138642 |
| work_keys_str_mv | AT geoffsutcliffe proofverificationwithgdvandlambdapiitsamatteroftrust AT fredericblanqui proofverificationwithgdvandlambdapiitsamatteroftrust AT guillaumeburel proofverificationwithgdvandlambdapiitsamatteroftrust |