SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912484256907264 |
|---|---|
| author | Cailler, Julie Guilloud, Simon |
| author_facet | Cailler, Julie Guilloud, Simon |
| contents | Motivated by the transfer of proofs between proof systems, and in particular from first order automated theorem provers (ATPs) to interactive theorem provers (ITPs), we specify an extension of the TPTP derivation text format to describe proofs in first-order logic: SC-TPTP. To avoid multiplication of standards, our proposed format over-specifies the TPTP derivation format by focusing on sequent formalisms. By doing so, it provides a high level of detail, is faithful to mathematical tradition, and cover multiple existing tools and in particular tableaux-based strategies. We make use of this format to allow the Lisa proof assistant to query the Goéland automated theorem prover, and implement a library of tools able to parse, print and check SC-TPTP proofs, export them into Coq files, and rebuild low-level proof steps from advanced ones. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_11349 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus Cailler, Julie Guilloud, Simon Logic in Computer Science Motivated by the transfer of proofs between proof systems, and in particular from first order automated theorem provers (ATPs) to interactive theorem provers (ITPs), we specify an extension of the TPTP derivation text format to describe proofs in first-order logic: SC-TPTP. To avoid multiplication of standards, our proposed format over-specifies the TPTP derivation format by focusing on sequent formalisms. By doing so, it provides a high level of detail, is faithful to mathematical tradition, and cover multiple existing tools and in particular tableaux-based strategies. We make use of this format to allow the Lisa proof assistant to query the Goéland automated theorem prover, and implement a library of tools able to parse, print and check SC-TPTP proofs, export them into Coq files, and rebuild low-level proof steps from advanced ones. |
| title | SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2507.11349 |