FMLtoHOL (version 1.0): Automating First-order Modal Logics with LEO-II and Friends

TL;DR

This paper introduces FMLtoHOL, a converter that translates first-order modal logics into classical higher-order logic, enabling the use of existing higher-order theorem provers for modal reasoning across various logics.

Contribution

The paper presents a novel converter tool that automates the translation of multiple first-order modal logics into higher-order logic, facilitating reasoning with existing theorem provers.

Findings

Supports multiple modal logics including K, K4, D, D4, T, S4, S5

Enables reasoning with off-the-shelf higher-order theorem provers

Facilitates modal logic reasoning using classical higher-order logic tools

Abstract

A converter from first-order modal logics to classical higher- order logic is presented. This tool enables the application of off-the-shelf higher-order theorem provers and model finders for reasoning within first- order modal logics. The tool supports logics K, K4, D, D4, T, S4, and S5 with respect to constant, varying and cumulative domain semantics.