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.