The formal proofs are inside the archive boolean_completeness.zip. You can also browse the generated documentation as colored HTML code here.
In order to compile the sources, you need the Coq proof assistant version 8.2.
If you are on a Unix-like system, and the executable coqc is in your PATH variable, you can just run the command make from inside a terminal window. If coqc is not in your path, you can either set it, or open the Coq IDE and run Make from the Compile menu.
If you are on a Windows system, you do not have make, and coqc is not in your PATH, the simplest solution is to open Coq IDE and compile one by one file, making sure to do it in the following order: pairing/extEqualNat.v, pairing/misc.v, pairing/primRec.v, pairing/cPair.v, lists.v, filters.v, classcomp.v.
Note: The formalisation is not complete, sorting of lists in lists.v remains to be finished.
Back to Danko Ilik's home page