Copyright 2020 Marianna Girlando, Marianela Morales.

This file is part of MOILab. MOILab 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. 

MOILab 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 MOILab. If not, see 
<http://www.gnu.org/licenses/>.

----------------------------------------
MOILab theorem prover
MOdal and Intuitionistic Labelled sequents
----------------------------------------
----------------------------------------


MOILab is a Prolog prototype theorem prover for intuitionistic modal logic IK, implementing a labelled sequent calculus for the logic.

The user selects the formula to be tested, and MOILab implements a backwards proof search yielding a derivation or a bi-relational countermodel.
The axioms of IK 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
---------------

MOILab 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 accessible 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.


To start SWI Prolog, navigate to the MOILab directory and type:

$  swipl

Then load the MOIN file, with:

?-  [moi_lab].

Now MOILab can be queried with goals. Proof search for a formula F is triggered
by the predicate:

?-  derive(F).



Output files
------------

In case of success of the proof search procedure, MOILab prints out a derivation,
accessible in the output file: derivationLab.tex

In case of proof search failure, MOILab prints out a countermodel, accessible in the output file: countermodelLab.tex

To generate a readable .pdf file out of the .tex output files for derivations and
countermodels, compile with pdflatex the file: result_IKlab.tex



Example
-------

To test derivability of axiom k1, query MOILab with the goal:

?- derive(!(a->b)-> ((!a)->(!b)) ).

To get a .pdf file showing the derivation, compile the file result_IKlab.tex.



Axioms of IK
------------

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



Bibliography
------------

The labelled sequent calculus for intuitionistic modal logics implemented by MOILab are
introduced in:

    Marin, S., Morales, M., Straßburger, L.:  A fully labelled proof system for intuitionistic
    modal logics. 2019. hal-02390454
    
    available at: https://hal.inria.fr/hal-02390454

MOILab is modelled on MOIN, a theorem prover, whose system description is available here:
    
    Girlando, M., Straßburger, L.: MOIN: A Nested Sequent Theorem Prover for Intuitionistic
    Modal Logics (System Description). Accepted for publication at IJCAR 2020.

    MOIN webpage is here: 
    http://www.lix.polytechnique.fr/Labo/Lutz.Strassburger/Software/Moin/MoinProver.html