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

2012/07/28 by Benzmueller, Christoph, Raths, Thomas
#03B15 #03B60 #68T15 #68T27 #68T30 #Artificial Intelligence (cs.AI) #F.4.1 #FOS: Computer and information sciences #I.2.3 #I.2.4 #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1207.6685

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.

Related

• Solving Quantified Modal Logic Problems by Translation to Classical Logics
• Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
• First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)
• First-Order Modal Logic: Frame Definability and Lindström Theorems
• Growing a Modular Framework for Modal Systems- HOLMS: a HOL Light Library