Simptcheck: Simple Proof Term Checker

(New) April 19, 2008: I formulated conditions related to consistency of Quine's NF in Simptcheck notation. You can use Simptcheck to verify a solution (which would prove Quine's NF consistent) or to verify a proof that my approach to constructing a model of NF cannot work.

Simptcheck is a simple proof term checker written in OCaml written by Chad E. Brown in March 2008. Simptcheck is designed to separate the formulation of a problem from the formulation of its solution.

Download Here

Here is how simptcheck is intended to be used:

User A writes files file₁,...,file_n specifying an underlying theory and a problem containing some missing definitions d₁,...,d_m and open claims c₁,...,c_k. Simptcheck can check that the problem is well-formed as follows:
simptcheck file₁ ... file_n

User B can either provide files giving a solution or proving the problem is inconsistent (has no solution).

User B provides a solution by giving files file_n+1,...,file_n+p which gives terms defining d₁,...,d_m and proof terms for the claims c₁,...,c_k. The new files cannot contain any new constants or axioms. User A can use simptcheck to check that the new files form a solution as follows:
simptcheck file₁ ... file_n -s file_n+1 ... file_n+p

User B shows the problem has no solution by giving files file_n+1,...,file_n+p which proves false by treating d₁,...,d_m as constants and c₁,...,c_k as axioms. The new files cannot contain any new constants or axioms. User A can use simptcheck to check that the new files form a proof of inconsistency as follows:
simptcheck file₁ ... file_n -n file_n+1 ... file_n+p