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. In a nutshell, 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 two proof systems for the logic: a fully labelled sequent calculus, explicitly incorporating semantic elements in the syntax, and a bi-nested calculus, using additional structural connectives. After introducing the proof systems, we will discuss and compare the corresponding decision algorithms, defined by implementing terminating proof search in the two calculi.
This talk is based on joint work with Han Gao, Roman Kuznets, Sonia Marin, Marianela Morales, Nicola Olivetti, and Lutz Straßburger.