Copyright 2020 Marianna Girlando, Lutz Straßburger. This file is part of MOIN. MOIN is free software: you can redistribute it and or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, version 3 of the License. MOIN is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with MOIN. If not, see . ---------------------------------------- MOIN theorem prover MOdal and Intuitionistic Nested sequents ---------------------------------------- ---------------------------------------- MOIN is a Prolog theorem prover for classical and intuitionistic modal logics. It implements three kinds of nested calculi: 1. nested calculi for classical modal logics 2. single-conclustion nested calculi for intuitionistic modal logics 3. multi-conclustion nested calculi for intuitionistic modal logics The user selects the formula to be tested, the logic in which the formula needs to be tested, and the proof system to be used. MOIN implements a backwards proof search on the formula, yielding a derivation or, for proof systems 1 and 3, a countermodel. The axioms of the logics can be found at the end of this file, along with some bibliographic references. Syntax ------ Atomic formulas are Prolog atoms a, b, c,..., and the two Prolog constants false, true. Non-atomic formulas are generated by the following connectives: ~A | A ^ A | A v A | A -> A | !A | ?A respectively standing for negation, conjunction, disjunction, box and diamond. The usual conventions for parentheses apply. Setup and usage --------------- MOIN runs on SWI Prolog. To use the prover on your machine, first make sure you have SWI Prolog installed (https://www.swi-prolog.org/download/stable). In order to compile the .tex output into a .pdf file, a Latex editor needs to be installed. The .tex output files are compiled using Virginia Lake LaTex Macros by Alessio Guglielmi: http://alessio.guglielmi.name/res/vl/ The .sty file is here: http://alessio.guglielmi.name/res/vl/virginialake.sty or downloadable with the command: wget http://alessio.guglielmi.name/res/vl/virginialake.sty The virginialake.sty file needs to be placed in the same directory as the .tex files directory. To start SWI Prolog, navigate to the MOIN directory and type: $ swipl Then load the MOIN file, with: ?- [moin]. Now MOIN can be queried with goals. Proof search for a formula F is triggered by the predicate: ?- derive(system,Axioms,F). The first argument selects the proof system. Type k to derive F in classical modal logic using nested sequents; i to derive F in intuitionistic modal logic using single-conclusion nested sequents; m to derive F in intuitionistic modal logic using multi-conclusion nested sequents. The second argument is a list, specifying the system of modal logic at which validity of F is to be tested. Write [] to derive F in K or IK [d] to derive F in KD or IKD (*) [t] to derive F in KT or IKT [b] to derive F in KB or IKB [4] to derive F in K4 or IK4 [5] to derive F in K5 or IK5 Combinations of the above are also possible: write [t,b] to derive F in KTB or IKTB, and so on. (*) When asked to derive a formula F in the single-conclusion nested calculus with axiom d, as a default choice MOIN uses the rules for white and black d given in Figure 3 of the article. To use rule d^[] instead (Figure 4 of the article), type [d1] into the list. The use of this rule in combination with axiom 4 and / or 5 might generate non-terminating branches. Example ------- To test derivability of axiom k1 in IK using single-conclusion nested sequents, query MOIN with the goal: ?- derive(i,[],!(a->b)-> ((!a)->(!b)) ). To get a .pdf file showing the derivation, compile the file NIKs+X-result.tex (more details below on the .tex output are given below). Running MOIN with a script --------------------------- On Linux OS, bash version 4.0 or higher, the script moin.sh allows to run MOIN without having to run SWI Prolog and load the moin.pl file in it. It also displays directly the .pdf output, containing the derivation or the countermodel. To run the script, navigate into the Moin directory from the terminal and type: ./moin.sh System 'F' The first argument, System, is the proof system in which the formula (F, the second argument) is to be tested. To specify the system, write: K, IKs, IKm to derive F in classical nested, intuitionistic single-conclusion nested, or intuitionistic multi-conclusion respectively; Add D, T, B, 4, 5 right after K to derive F in the corresponding extension of K or IK. The script prints out in the terminal the time MOIN takes to answer the query. It has been designed for testing the code. Example ------- Write the following line to test the formula in IS5, using multi-conclusion nested calculi. The formula is not derivable in IS5, a countermodel shows up. ./moin.sh IS5m '((?((!a -> !b) -> false) ^ ?(!c -> false)) -> !?!a)' Output files ------------ In case of success of the proof search procedure, MOIN prints out a derivation, accessible in a .tex output file: derivationNK.tex for classical nested sequents; derivationNKs.tex for intuitionistic nested sequents, single-conclusion; derivationNKm.tex for intuitionistic nested sequents, multi-conclustion. In case of proof search failure for classical nested sequents and intuitionistic multi-conclusion sequents, MOIN prints out a countermodel, accessible at: counterNK.tex for classical nested sequents; counterNKm.tex for intuitionistic multi-succedent nested sequents. To generate a readable .pdf file out of the .tex output files for derivations and countermodels, compile with pdflatex the file: NK+X-result.tex for classical nested sequents; NIK+X-result.tex for intuitionistic nested sequents, single-conclusion; NIKs+X-result.tex for intuitionistic nested sequents, multi-conclusion. Axioms of the implemented logics -------------------------------- Classical modal logics: MOIN treats all the 15 logics in the S5-cube. Axioms for K: axioms of classical logic, plus necessitation rule, plus k1 (!(a->b)) -> ((!a)->(!b)) Axioms for extensions of K: d !a -> ?a t !a -> a b ? (!a)-> a 4 !a -> !(!a) 5 ?a -> !(?a) Intuitionistic modal logics: MOIN treats all the decidable modal logics in the IS5-cube. Axioms for IK: axioms for intuitionistic modal logic, plus necessitation rule, plus k1 (!(a->b)) -> ((!a)->(!b)) k2 (!(a->b)) -> ((?a)->(?b)) k3 (?(a v b)) -> ((?a)v(?b)) k4 ((?a)-> (!b)) -> (!(a->b)) k5 (?false)->false Axioms for extensions of IK: id (!a)->(?a) it (a->(?a))^((!a)->a)) ib (a->(!(?a)))^((?(!a)))->a i4 ((?(?a))->(?a))^((!a)->(!(!a))) i5 (?a->(!(?a))) ^ ( (?(!a))->!a ) ***WARNING***: For IK4, ID4 and IS4 (=IKT4), decidability is still not known. Run MOIN for these systems at your own risk, as the program might not terminate, and/or might produce contermodels that do not obey all the necessary conditions. Bibliography ------------ The nested sequents for classical modal logics implemented by MOIN were introduced in: Brünnler, K.: Deep sequent systems for modal logic. Archive for Mathematical Logic 48(6), 551–577 (2009). Single-conclusion nested sequents for intuitionistic modal logics can be found in: Straßburger, L.: Cut elimination in nested sequents for intuitionistic modal logics. In: Pfenning, F. (ed.) FoSSaCS’13. LNCS, vol. 7794, pp. 209–224. Springer (2013) Multi-conclusion nested sequents for intuitionistic modal logics can be found at: Kuznets, R., Straßburger, L.: Maehara-style modal nested calculi. Archive for Mathematical Logic 58(3-4), 359–385 (2019).