Mario Piazza

A Kruskal Decision Procedure for Intuitionistic Modal Logic IK4

We prove decidability of Simpson's intuitionistic modal logic IK$ by working directly with cut-free nested proofs. Once the end formula is fixed, only finitely many combinations of input and output formulae can occur at a node, although the modal tree itself remains unbounded. We order these nested sequents by rooted h...