Automating Quantified Multimodal Logics in Simple Type Theory -- A Case Study

This paper presents a case study in quantified multimodal logics. An interesting aspect of this case study is that off the shelf theorem provers and model generators for simple type theory, that is, classical higher-order logic, are employed to automate problems in quantified multimodal logics, that is, nonclassical logics. This is enabled by our recent embedding of normal quantified multimodal logics in simple type theory [8, 10], which is sound and complete [10]. Interestingly, not only reasoning within various nonclassical logics can be automated this way but also reasoning about them. For example, the equivalence between different properties of accessibility relations and their associated multimodal axioms can be proved automatically.