------------------------ ileanCoP 1.0 ReadMe File ----------- Description ileanCoP is a theorem prover for intuitionistic first-order logic implemented in Prolog. See http://www.leancop.de for more details. -------- Contents ReadMe_ileancop10 - this ReadMe file ileancop.pl - the ileanCoP prover (or ileancop_sicstus.pl, ileancop_swi.pl) nnf_mm_intu.pl - clausal form transformation format.leancop - format file for the TPTP2X tool -------- Starting At first ileanCoP 1.0 has to be loaded into the Prolog system: [ileancop]. Afterwards ileanCoP is invoked with prove(F). where 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 formula is intuitionistically valid. If it fails the formula is not intuitionistically valid. Example: 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