Home |
Manual | Library |

The Zermelo Proof Checker (ZPC) is a lightweight proof assistant based on standard set theory and Hindley-Milner type theory. ## Obtaining and installing ZPCEnsure that your computer is Unix-compatible. If you are running Microsoft Windows, you may need to install Cygwin. Ensure that the following programs are installed: OCaml and the E Theorem Prover. $ ocamlc -version 3.12.1 $ eprover --version E 1.4 Namring Download the latest release: ZPC-1.0.tgz. 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
## ExampleHere is a proof that a Cauchy sequence
of rational numbers is always bounded. If you save it
as [~]$ zpc Example.zl [~]$ The result is an empty file called |