Research Group Deduction at IMN/HTWK Leipzig
ProCom/CaPrI and the Shell ProTop
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 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
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
are prepared to be used from within ProTop. Only the interface modules
are included in the distribution.
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.
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.
Neugebauer: Reachability Analysis for a Certain Class of Calculi
Submitted to LOPSTR'95
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
Fri Mar 30 09:51:42 MET DST 2001)