---------------------------- nanoCoP-M ReadMe File (v2.0) ----------- Description nanoCoP-M is a compact non-clausal connection theorem prover for the first-order modal logics D, T, S4, and S5 (with constant, cumulative or varying domains) implemented in Prolog. It also supports heterogeneous multimodal logics (D, T, S4, S5). See the web site at http://www.leancop.de/nanocop-m/ for more details. -------- Contents ReadMe_nanoCoP-M - this ReadMe file nanocopm.sh - shell script to invoke nanoCoP-M nanocopm20.pl - the nanoCoP-M core prover (nanocopm20_swi.pl for SWI Prolog) nanocopm_main.pl - invokes the nanoCoP-M core prover nanocopm_proof.pl - presents proof found by nanoCoP-M nanocop_qmltp2.pl - translates problems that are in QMLTP syntax ------------ Installation Set the path for the Prolog system (ECLiPSe 5.x or SWI) and the path for the nanoCoP-M prover in the file nanocopm.sh. The modal logic and domain condition are specified through the variables LOGIC (d,t,s4,s5,multi) and DOMAIN (const,cumul,vary). This file also includes parameters to control the output of the proof and to specify the proof layout. --------- Execution ./nanocopm.sh %s [%d] where %s is the name of the problem file and %d is the (optional) time limit in seconds (used for the internal strategy scheduling). Example: ./nanocopm.sh SYM/SYM002+1 Output if formula is valid: %s is a modal () Theorem Output if formula is invalid: %s is a modal () Non-Theorem where is the selected modal logic and domain condition. Example: SYM/SYM002+1 is a modal (s4/cumul) 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), '#' (box operator), '*' (diamond operator), ';' (disjunction), ',' (conjunction), '=>' (implication), '<=>' (equivalence), and the logical quantifiers 'all X:' (universal) and 'ex X:' (existential) where X is a Prolog variable. Example: f( ((# (all X: p(X))) => (all X: (* p(X)))) ). For multimodal logic, each modal operator is indexed with a Prolog term (identifier) and a modal logic (d,t,s4,s5). Example: f( ((# 1^s4: p) => ((# 1^s4: p) ; (* 2^s5: q))) ). Alternatively, the problem file may contain a formula in QMLTP syntax (see http://www.iltp.de/qmltp/). ----------- At a Glance System: nanoCoP-M Version: 2.0 URL: http://www.leancop.de/nanocop-m/ Command: ./nanocopm.sh %s %d Format: leancop/nanocop or qmltp Output: - valid: %s is a modal () Theorem - invalid: %s is a modal () Non-Theorem - unsatisfiable(*): %s is modal () Unsatisfiable - satisfiable(*): %s is modal () Satisfiable (*: for problems in QMLTP syntax without conjecture)