-------------------
leanCoP-SInE (v2.1)
Jens Otten, Thomas Raths
University of Potsdam
-----------
Description
leanCoP-SInE is an automated theorem prover for classical first-
order logic. It combines the systems SInE 0.4 and leanCoP 2.1.
SInE is an axiom selection system for first-order theories. It
uses a syntactic approach based on symbols' presence in axioms
and the conjecture. SInE is developed by Krystof Hoder. See also
http://www.cs.man.ac.uk/~hoderk/sine.
leanCoP is a compact theorem prover for classical first-order
logic implemented in Prolog. See http://www.leancop.de for more
details.
------------
Installation
A Prolog system and Python are required to run leanCoP-SInE.
Set the path for the Prolog system (either ECLiPSe, SICStus
or SWI) and the path for the leanCoP-SInE prover in the file
leancop_sine.sh. This file also includes parameters to control
the output of the proof and to specify the proof layout.
---------
Execution
The command to run the prover is
./sine_batch.py -e leancop -t