MOILab is a SWI Prolog prototype theorem prover for intuitionstic modal logic IK. It implements a labelled sequent calculus for IK presented in an article by Sonia Marin, Marianela Morales and Lutz Straßburger, available here.

MOILab is modelled on MOIN, a Prolog theorem prover implementing single-conclusion and multi-conclusion nested sequents for the 15 logics in the intuitionistic modal logics cube.

MOILab consists of a set of Prolog clauses, each clause representing a rule in the labelled proof systems. The clauses are recursively applied to a given formula, constructing a proof-search tree. MOILab yields a derivation in case of proof search success, and a countermodel in case of proof search failure. The countermodel is a bi-relational model, and it is extracted from the upper sequent occurring a failed branch. MOILab is a prototype, meaning that, as to now, proof search does not terminate on all IK formulas.

A short presentation of MOILab is available here.

MOIN runs on SWI Prolog. To use the prover, first make sure to have SWI Prolog installed (download page here). Then, download and unpack this file and follow the instructions in the readme.

LaTex is needed to generate a .pdf file from of the .tex files containing derivations or countermodels produced in output by MOIN. The .tex output files are compiled using Virginia Lake LaTex Macros by Alessio Guglielmi, available here.