The Zermelo Proof Checker

The Zermelo Proof Checker (ZPC) is a lightweight proof assistant based on standard set theory and Hindley-Milner type theory.

Obtaining and installing ZPC

1. Ensure that your computer is Unix-compatible. If you are running Microsoft Windows, you may need to install Cygwin.

2. Ensure that the following programs are installed: OCaml and the E Theorem Prover.

   $ ocamlc -version
   3.12.1
   $ eprover --version
   E 1.4 Namring
   

3. Download the latest release: ZPC-1.0.tgz.

4. Follow the standard procedure for installing Unix-style software:

   [~]$ tar xzvf ZPC-1.0.tgz
   [~]$ cd ZPC-1.0
   [~/ZPC-1.0]$ ./configure && make && sudo make install
   

Example

Here is a proof that a Cauchy sequence of rational numbers is always bounded. If you save it as Example.zl in your home directory, the following command should succeed:

[~]$ zpc Example.zl
[~]$

The result is an empty file called Example.czo. It has a timestamp and can be viewed as certificate that the proof was checked.