A certified proof checker for Fitch-style propositional logic proofs as defined in the book Logic for Computer Science by Huth and Ryan.
Coq definitions and proofs:
- Coq (8.16 or later)
- Coq Ott library (0.33 or later)
HOL4 definitions and proofs:
Executable OCaml checkers:
OCaml 4.05(or later)menhirOCamlbuildocamlfind
Executable CakeML checker:
Make sure Ott's Coq auxiliary library has been installed in Coq's user-contrib library directory. One easy way to install Ott and its Coq library is via opam:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-ott
Then, run make. This will compile the Coq syntax and relational definitions and check all proofs.
Run make hol. This will compile the HOL4 syntax and relational definitions and check all proofs.
To build the default executable checker program, run make checker. Example proofs (.nd files) can then be checked as follows:
$ ./checker.native examples/imp.nd
To generate an OCaml program with the alternative Prolog file format parser, run make prolog in the root directory. Example proofs (.pl files) can then be checked as follows:
$ ./prolog.native examples/imp_perm.pl
A verified executable checker in CakeML can be obtained using the CakeML proof-producing synthesis tool ("compiler frontend 1"). To generate it, go to the cakeml directory and adjust the CAKEMLDIR variable in the Holmake file to point to the directory with CakeML release 1009. Then, run Holmake.
For convenience, a pretty-printed version of the verified CakeML code is available; note that the pretty-printing itself has not been verified. Moreover, there is currently no parser for for the surface syntax.
To generate a document (fitch.pdf) describing the proof system and proofs, run make fitch.pdf (requires LaTeX and Ott).