About

MOIN is a SWI Prolog theorem prover for classical and intuitionstic modal logics. It implements three kinds of nested calculi:

Nested sequents for classical modal logics, presented in Brünnler, 2009, available here.
Nested sequents (Gentzen-style, or single-conclusion) for intuitionistic modal logics, from Straßburger, FoSSaCS 2013, available here, Marin and Straßburger, AiML 2014, and Chaudhuri, Marin and Straßburger, FSCD 2016.
Nested sequents (Maehara-style, or multi-conclusion) for intuitionistic modal logics, from Kuznets and Straßburger, Archive for Mathematical Logic, 2019.

The modal and intuitionistic modal logics considered are all the 15 systems occurring in the modal S5-cube, and all the decidable intuitionistic modal logics in the IS5-cube. MOIN also provides a protptype implementation for the intuitionistic logics for which decidability is not known (IK4,ID5 and IS4).
MOIN is consists of a set of Prolog clauses, each clause representing a rule in one of the three proof systems. The clauses are recursively applied to a given formula, constructing a proof-search tree. The user selects the nested proof system, the logic, and the formula to be tested. In the case of classic nested sequent and Maehara-style nested sequents, MOIN yields a derivation, in case of success of the proof search, or a countermodel, in case of proof search failure. The countermodel for classical modal logics is a Kripke model, while for intuitionistic modal logic is a bi-relational model. In case of Gentzen-style nested sequents, the prover does not perform a countermodel extraction.

A system description of MOIN is available here.

Download

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.