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