Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
a simple OCaml proof-checker for TSTP cnf/fof derivations. It calls external provers to check every proof step.
OCaml
Branch: master

Fetching latest commit…

Cannot retrieve the latest commit at this time

Failed to load latest commit information.
src
.gitignore
.header
LICENSE
Makefile
README.md

README.md

tstp-proof-checker

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.

License

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.

Build

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

make

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

  • the E prover
  • the SPASS prover

Use

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

./tstp_check.native [options] derivation
Something went wrong with that request. Please try again.