-----------------------
leanCoP 1.0 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_leancop10 - this ReadMe file
leancop.pl       - the leanCoP prover
 (or leancop_ec5.pl, leancop_sicstus.pl, leancop_swi.pl)
nnf_mm.pl        - clausal form transformation
format.leancop   - format file for the TPTP2X tool

--------
Starting

At first leanCoP 1.0 has to be loaded into the Prolog system:
   [leancop].
For non-clausal formulae the clausal form translation is required:
   [nnf_mm].

Afterwards leanCoP is invoked with
   prove(M).
or
   prove(F).
where M is a matrix, i.e. a list of clauses, and clauses are lists
of literals where negation is expressed by "-". F is a first-order
formula made up of Prolog terms (atomic formulae), the logical
connectives '~' (negation), ';' (disjunction), ',' (conjunction),
'=>' (implication), '<=>' (equivalence), and quantifiers 'all X:'
(universal) and 'ex X:' (existential) where X is a Prolog variable.

If this call succeeds the entered matrix/formula is valid. If it
fails the matrix/formula is not valid.

Example: prove( [[q(a)],[-p],[p,-q(X)]] ).
         prove( ((p,all X:(p=>q(X)))=>all Y:q(Y)) ).

--------------
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