Checkers is a λ-prolog implementation of a tool for checking proofs output by theorem provers. It is based on the theory of foundational proof certificates (see, for example, here).
Currently it has support for checking some of the proofs from e-prover. This means we are able to parse the proofs into λ-prolog modules which can than be checked by checkers.
The proof checking component of checkers is implemented in λ-prolog. The E-prover parser is implemented in OCaml.
- Checkers depends on the Teyjus implementation of λ-prolog. Teyjus can be found here here. Please install version 2.1 or later.
- The parser can be found in
proofs/tstpparser. Just typemakeinside this directory and you will obtain an executabletstpparser
The executable tstpparser can be run on e-prover's proof evidence resulting on
a .mod and a .sig λ-prolog files (proof certificates). For instance,
the following set of commands:
cd proofs/tstpparser
make
cd ..
./tstpparser/tstpparser simple.out simple
will generate the simple.mod and simple.sig files in the
proofs directory which correspond to the certificate of the
proof in simple.out.
The script prover.sh can be used to compile and run \checkers\ on given certificates.
The argument for Checkers is the name of the .mod and .sig files of the certificate, which must be placed in the src folder.
For example, in order to check the proof certificate contained in the
files param2.mod and param2.sig, one needs to place them in the src folder and execute the following command:
./prover.sh param2
Checkers was tested under Debian 8 and Fedora 21. The shell scripts are written for bash.
The program contains the following files and directories.
proofsdirectory which contains utilities and examples for interfacing with E-prover.srcdirectory contains the λ-prolog code of the program, including theFPCfor E-prover.READMEfile which contains instructions of how to run the program.prover.shscript for running Checkers on a given certificate name.prover-debug.shscript for running Checkers in debugging mode. This should mainly be used by implementors of FPCs.
Some certificates for testing can be found in the folder src/tests/resolution.
These certificates are already included in the path and can be checked without the need to copy them first to the src folder.
Checkers currently supports certification of two forms of resolution proofs. Please refer to the system description of Checkers
for more information about the two formats.
Examples of the two forms can be seen in the problems eprover1 and eprover2 which can be found in the tests directory.
- Checkers requires the latest version of Teyjus in order to properly handle paths. It should be noted that the program prover-debug.sh does not require the latest version of Teyjus and can be tried without the intallation of the later.
./prover-debug.sh module_name