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

The System CERESω

The CERESω system implements the calculus LKsk and the characteristic clause set extraction. The aim is to replace the older CERES system as soon as it subsumes all of its functionality. The system is implemented as part of the Generic architecture for proofs (GAPT) framework, which also contains the rewrite of the ATP theorem prover and an improved Prooftool graphical user interface.

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