---------------------------- nanoCoP-i ReadMe File (v1.0) ----------- Description nanoCoP-i is a compact non-clausal connection theorem prover for intuitionstic first-order logic implemented in Prolog. See the web site http://www.leancop.de/nanocop-i/ for more details. -------- Contents ReadMe_nanoCoP-i - this ReadMe file nanocopi.sh - shell script to invoke nanoCoP-i nanocopi.pl - the nanoCoP-i core prover nanocopi_main.pl - invokes the nanoCoP-i core prover nanocop_tptp2.pl - translates problems that are in TPTP syntax ------------ Installation Set the path for the Prolog system (ECLiPSe 5.x) and the path for the nanoCoP-i prover in the file nanocopi.sh. --------- Execution ./nanocopi.sh %s where %s is the name of the problem file. Example: ./nanocopi.sh SET/SET009+3 Output if formula is valid: %s is an intuitionistic Theorem Output if formula is invalid: %s is an intuitionistic Non-Theorem Example: SET/SET009+3 is an intuitionistic Theorem ------ Syntax The problem file has to contain a Prolog term of the form f(). in which is a first-order formula built from 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)) ). Alternatively, the problem file may contain a formula in TPTP syntax (see http://www.tptp.org). If the problem file contains equality ('=') all equality axioms are added automatically. ----------- At a Glance System: nanoCoP-i Version: 1.0 URL: http://www.leancop.de/nanocop-i/ Command: ./nanocopi.sh %s Format: leancop/nanocop or (raw) tptp Output: - valid: %s is an intuitionistic Theorem - invalid: %s is an intuitionistic Non-Theorem - unsatisfiable(*): %s is intuitionistically Unsatisfiable - satisfiable(*): %s is intuitionistically Satisfiable (*: for problems in TPTP syntax without conjecture)