-------------------- 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 " ". ------ Syntax The problem file has to contain a Prolog term of the form f(). in which 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)) ). If the problem file contains equality ('='), then equality axioms are added. Alternatively, the problem file can use the TPTP syntax. -------------- Transformation Problems in the TPTP syntax are automatically translated into the leanCoP format by using the built-in translation (leancop_tptp2.pl), which also adds the equality axioms. This is the recommended method. Alternatively, problems can be translated by using the TPTP2X tool: Format file: format.leancop Options: stdfof Example: ./tptp2X -f leancop -t stdfof SET/SET009+3.p ----------- At a Glance System: randoCoP Version: 1.1 URL: http://www.leancop.de Command: ./randocop %s %d Format: leancop or tptp Transform: stdfof (for leancop format) Proved: %s is a Theorem Refuted: %s is a Non-Theorem Unsatisfiable: %s is Unsatisfiable Satisfiable: %s is Satisfiable