HLK ProofTool
TU Vienna logic.at Theory and Logic Group (E185-2)


The current source version (Beta 9) for Linux and Mac OS X:

For installation instructions please be referenced to the README file located in the root directory of the download package.

At this time only Linux and Mac OS X are supported. CERES has been tested and is known to run on various Linux Distributions (e.g. Debian stable/testing, Redhat 9.x, Fedora, Suse 9.x) and Mac OS X Tiger.

However the system is written in ANSI-C++, i.e. the C++ Programming Language following the International Standard 14882:1998 approved as an American National Standard, and it is therefore likely to run on other systems - including Windows - as well. Note that if you try to run the system on a currently unsupported operating system it is on your own account. Nevertheless we will try to support you as well as possible.

To be able to comfortably use CERES, you may want to use HLK (beta 7 or higher) to write proofs in a higher-level language and Proof Tool (beta 6 or higher) to view proofs.

In any case the system CERES requires the automated theorem prover Prover 9 or its predecessor Otter to perform all tasks dependent on resolution refutations.


Alternative theorem provers

Supplemental Material

The XML DTD defining the input and the output format:

Virtual Machines

Note: This virtual machine is based on an older version of CERES. It supports all main features of CERES, but some newer ones (e.g. support for alternative theorem provers) are not included in this version.

The most comfortable way of using or just trying out CERES and some of its examples is to download the following virtual machine. You will find pre-installed the CERES system along with the HLK compiler and the Proof Tool on an Ubuntu operating system with graphical user interface.

Note that in order to use the virtual machine you need to install the appropriate version for your operating system of the free VMware Player.