Hanna Lachnitt

Systematic Verification of the Intuitionistic Modal Logic Cube in Isabelle/HOL

Betreuer: Christoph Benzmüller , Raúl Rojas , Maximilian Claus
Abschluss: Bachelor of Science (B.Sc.)
Abgabedatum: 30.01.2017


Due to its computational interpretation, there has been a lot of interest in intuitinistic logic in computer science. Adding combinations of the intuitionistic modal axioms to intuitionistic modal logic IK results in different systems. Together they constitute the  intuitionistic modal logic cube. We use an embedding of intuitionistic model logic in higher order logic to verify this cube.  Automatic reasoning tools, such as Sledgehammer and Nitpick, were used to prove the inclusion relations between the cube's logics and the equality of some logics.