--------------------
randoCoP ReadMe File
-----------
Description
randoCoP is a theorem prover for classical first-order logic that
integrates randomized search techniques into the connection prover
leanCoP. See http://www.leancop.de for more details.
--------
Contents
ReadMe_randocop - this ReadMe file
randocop.sh - shell script to invoke randoCoP_sched
randocop_sched.pl - strategy scheduling for the core prover
leancop20_rando.pl - the extended leanCoP core prover
def_mm.pl - clausal form transformation
leancop_proof - presents proof found by leanCoP
leancop_tptp2 - translates problems in TPTP syntax
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 randoCoP prover in the file randocop.sh.
---------
Execution
./randocop.sh %s [%d]
where %s is the name of the problem file and %d is the (optional)
time limit in seconds. The proof is written to the standard output.
Example: ./randocop.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
Alternatively, the file %s can contain a list of problems, i.e.
for each problem a line "