The Zermelo Proof Checker

back to jeremybem.org

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
    $ eprover --version
    E 1.8-001 Gopaldhara
    

    The E version can also be 1.7. Other versions may not work.

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

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

    [~]$ tar xzvf ZPC-1.1.tgz
    [~]$ cd ZPC-1.1
    [~/ZPC-1.1]$ ./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.