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

Generic Architecture for Proofs

Since the CERES system is tailored to first order logic, the CERESω method was implemented in a new system, the Generic Architecture of Proofs (GAPT) framework. Our aim is to replace the older CERES system as soon as it subsumes all of its functionality.

GAPT contains parsers and object representations for typed lambda calculus as well as for first- and higher order logic. Additionally to the calculi required for first order CERES it implements LKsk. Also many algorithms like skolemization or extraction of the characteristic clause set and the struct are already present.

First order resolution proofs are handed to Prover 9 or ATP. We plan to connect higher order therorem provers to GAPT in the future.

Apart from CERES, the GAPT project also contains the rewrite of the ATP theorem prover and a new Prooftool suited for higher order proofs.

System Documentation

At the moment, both the end-user and developer documentation is contained in the GAPT Wiki.

Downloads

The latest development version of GAPT is availiable via Subversion, the GAPT Wiki contains detailed instructions on how to install and run the system.

You can download a precompiled version of the CERES commandline interface (currently version 1.9) at the project's download page.