-------------------
leanCoP ReadMe File

-----------
Description

leanCoP is a compact theorem prover for classical first-order logic
implemented in Prolog. See http://www.leancop.de for more details.

--------
Contents

ReadMe_leancop - this ReadMe file
leancop.sh     - shell script to invoke leanCoP
leancop20.pl   - the leanCoP core prover
def_mm.pl      - clausal form transformation
leancop_tlimit - invokes leanCoP with a time limit
format.leancop - format file for the TPTP2X tool

------------
Installation

Set the path for the ECLiPSe Prolog system (version 5 or greater)
and the path for the leanCoP prover in the file leancop.sh.

---------
Execution

./leancop.sh %s [%d]
where %s is the name of the problem file and %d is the (optional)
time limit in seconds.

Example: ./leancop.sh SET/SET009+3 600

Output if formula is valid:    %s is a Theorem
Output if formula is invalid:  %s is a Non-Theorem

Example: SET/SET009+3 is a Theorem

------
Syntax

The problem file has to contain a Prolog term of the form
   f(<formula>).
in which <formula> is a first-order formula made up of Prolog
terms (atomic formulae), the logical connectives '~' (negation),
';' (disjunction), ',' (conjunction), '=>' (implication), '<=>'
(equivalence), and the logical quantifiers 'all X:' (universal)
and 'ex X:' (existential) where X is a Prolog variable.

Example: f( ((p , all X:(p=>q(X))) => q(a)) ).

--------------
Transformation

Problems in the TPTP syntax are translated into the leanCoP format
by using the TPTP2X tool.

Format file:  format.leancop
Options:      stdfof+add_equality

Example: ./tptp2X -f leancop -t stdfof+add_equality SET/SET009+3.p

-----------
At a Glance

System:    leanCoP
Version:   2.0
URL:       http://www.leancop.de
Command:   ./leancop.sh %s %d
Format:    leancop
Transform: stdfof+add_equality
Proved:    %s is a Theorem
Refuted:   %s is a Non-Theorem