A decision algorithm is an automated procedure establishing validity or invalidity of a formula in a given logical system. Proof systems, and in particular sequent calculus, can be fruitfully employed to define such algorithms. A proof theoretic decision procedure implements exhaustive and terminating root-first proof search for the formula in the calculus. If a proof is found the formula is valid. Otherwise, one can usually construct a countermodel for the formula at the root from a finite branch of a failed proof search tree. In the literature, proof-theoretic decision procedures have been defined for a number of systems, there including intuitionistic and modal logics.

In this talk we consider intuitionistic modal logic IK. This logic is the intuitionistic variant of modal logic K proposed by Fisher Servi, Plotkin and Stirling, and studied by Simpson. We shall present a fully labelled sequent calculus for the logic, explicitly incorporating semantic elements in the syntax, and discuss the corresponding decision algorithms, defined by implementing terminating proof search.

This talk is based on joint work with Han Gao, Roman Kuznets, Sonia Marin, Marianela Morales, Nicola Olivetti, and Lutz Straßburger.