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

TL;DR

This paper explores the use of existing higher-order theorem provers and model generators to automate reasoning in quantified multimodal logics, leveraging the TPTP infrastructure for classical higher-order logic.

Contribution

It demonstrates the feasibility of applying off-the-shelf higher-order tools to automate reasoning in complex multimodal logics through a detailed case study.

Findings

Successful automation of reasoning tasks in quantified multimodal logics

Effective use of TPTP infrastructure for higher-order logic

Potential for broader application of existing theorem provers

Abstract

In a case study we investigate whether off the shelf higher-order theorem provers and model generators can be employed to automate reasoning in and about quantified multimodal logics. In our experiments we exploit the new TPTP infrastructure for classical higher-order logic.