FMLtoHOL (version 1.0): Automating First-order Modal Logics with LEO-II and Friends
This tool addresses the challenge of automated theorem proving for modal logicians and AI researchers, but it is incremental as it builds on existing higher-order logic tools.
The paper tackled the problem of automating reasoning in first-order modal logics by developing a converter tool that translates these logics into classical higher-order logic, enabling the use of existing theorem provers and model finders for logics like K, S4, and S5 with various domain semantics.
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.