The TPTP Format for Clausal Tableau Proofs
History
- Hilbert proofs vs. Refutations
Saturation vs. Tableaux (and connection matrices and model elimination)
- The leanCoP format (~2008) was not not adopted elsewhere
- The Otten-Sutcliffe proposal (2010) never gained traction
- The Otten-Holden proposal (2023) provided inspiration
- Online proposal
Requirements
- Easy reconstruction of the tableau
- Information for structural verification
- Information for semantic verification
- Concise and simple
- Readable by humans as well as ATP tools
The Format
- path terms to record tableau structure
- Six (so far) recognized inference rules for structural verification
start, extension, connection, reduction,
lemma, lemma_extension,
- SZS status values for semantic verification
- Concise and simple TPTP format is human readable