MOILab: towards a labelled theorem prover for intuitionistic modal logics

We present MOILab, a prototype Prolog theorem prover implementing a labelled sequent calculus for IK, the basic system in the intuitionistic modal logics family. MOILab builds upon MOIN, a theorem prover implementing nested sequent calculi (both single-conclusion and multi-conclusion) for all the logics in the modal intuitionistic cube. With respect to the nested implementations, MOILab offers a straightforward countermodel construction in case of proof search failure