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).