Theory-Extensible Sequent Calculus (TESC) is a low-level, mechanically checkable proof format for first-order ATPs. Simple independent verifiers can check an input pair of a TPTP problem and a TESC proof, using the latter to verify that the former is unsatisfiable.
You can generate TESC proof files by compiling them from TSTP solution files using the TPTP-TSTP-TESC Processor (T3P) tool. T3P can also verify TESC proofs using one of three backend checkers: a formally verified checker written and verified in Agda, a performance-optimized checker written in Rust, and a debugging/backup checker written in Prolog.
T3P can be compiled using make. The following programs and variables
should be available on the path for successful compilation and usage:
- swipl for compiling the main T3P script.
- cargo (with Rust) for compilation of the TPTP parser and optimized TESC verifier.
- agda (with its standard library) for compiling the verified TESC verifier. You may need to use the exact version of the standard library for correct compilation.
- cadical and drat-trim for handling AVATAR steps used in Vampire's TSTP solutions.
- Environment variables
$TPTPand$TESCshould be set to the TPTP and TESC directory paths, respectively.
Installation and usage was only tested on Linux.
t3p compile [SOLVER] [PROBLEM] [SOLUTION] [PROOF] compiles a TPTP problem
[PROBLEM] and its TSTP solution [SOLUTION] to a new TESC proof [PROOF],
where [SOLVER] is the ATP used to generate [SOLUTION]. Currently supported
options for [SOLVER] are vampire and eprover.
t3p verify [VERIFIER] [PROBLEM] [PROOF] uses the TESC proof [PROOF]
to check that the TPTP problem [PROBLEM] is unsatisfiable. Currently
supported options for [VERIFIER] are vtv, otv, and dtv for the
Agda, Rust, and Prolog verifiers, respectively. [VERIFIER] may be
omitted, in which case T3P default otv.