Created: 2012-08-21 08:31
Updated: 2018-08-01 11:04
License: gpl-2.0



A simple OCaml proof-checker for TSTP cnf/fof derivations. It calls external provers to check every proof step that is annotated with thm (other handled annotations are esa, cth and the file() sources). It does not check the reduction to CNF or the correlation between axioms declared in the derivation, and actual axioms from a problem file, only the structure of the proof and the correctness of the proof steps.

The derivation is accepted if it contains a step with $false as formula, and if the set of steps that eventually yield this formula -- the correctness of which can be established using external, trusted theorem provers -- have a DAG structure.


Since the TPTP parser/lexer are from Darwin which is under GPL, the present software is also under GPLv2. A copy of the GPLv2 is attached to the project, in the file LICENSE.


You will need ocaml (3.12 or higher works; 3.11 or lower may work, I did not test). Type


It should build files (using ocamlbuild). Other dependencies are the provers used to check proof steps by default:

  • the E prover
  • the SPASS prover


Typical usage (pass -help as an option to get more details):

./tstp_check.native [options] derivation
Cookies help us deliver our services. By using our services, you agree to our use of cookies Learn more