Research Group Deduction at IMN/HTWK Leipzig

ProCom/CaPrI and the Shell ProTop

ProCom

ProCom is a theorem prover written in ECLiPSe Prolog. It is based on the PTTP paradigm.

ProCom is highly configurable. This means adaptability at various levels. ProCom has dozens of flags which influence its behaviour. The intermediate Prolog program which is generated to perform the proof task is made up of small pieces of Prolog code. Those pieces are collected in libraries and can be completely exchanged by the user.

To go further, even the inference rules to be used can be specified by the user. This can be done using the calculi programming interface CaPrI.

CaPrI

CaPrI is the Calculi Programming Interface of ProCom. This interface allows the user to program various calculi. Those high level descriptions of calculi are used to controll the translation in a PTTP-like mannor.

ProTop

ProTop is a shell for theorem provers. It provides means for the automation of experiments with internal and external theorem provers. Internal theorem provers are theorem provers written in Prolog which are loaded into the system and make use of the features of ProTop. External theorem provers are separate programs which are called by some interface modules from within ProTop.

Currently the internal provers ProCom and Pool are part of thye distribution. The external provers Otter and Setheo are prepared to be used from within ProTop. Only the interface modules are included in the distribution.

References

Gerd Neugebauer, Uwe Petermann: Specifications of Inference Rules and Their Automatic Translation: This is a paper describing the calculi programming interface CaPrI. It has been presented at the Workshop on Analytic Tableaux and related Methods, St. Goar 1995.
Gerd Neugebauer: ProCom/CaPrI and the Shell ProTop. User's Guide: This is the draft version of the users manual. This is also contained in the distribution.
Gerd Neugebauer: Reachability Analysis for a Certain Class of Calculi: Submitted to LOPSTR'95

Getting ProCom

You can get ProCom per ftp from koralle.htwk-leipzig.de:pub/ProCom/procom.tar.gz.

Unpack it with the command

gunzip < procom.tar.gz | tar -xvf - This will create a directory ProCom. This directory contains the files README and INSTALL. Follow the instructions mentioned there to install the program.

uwe@imn.htwk-leipzig.de Fri Mar 30 09:51:42 MET DST 2001)