FMLtoHOL (version 1.0): Automating First-order Modal Logics with LEO-II and Friends
classification
💻 cs.LO
cs.AI
keywords
logicsmodalfirst-orderordertoolapplicationautomatingclassical
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.