FMLtoHOL (version 1.0): Automating First-order Modal Logics with LEO-II and Friends
Logic in Computer Science
2012-07-31 v1 Artificial Intelligence
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.
Keywords
Cite
@article{arxiv.1207.6685,
title = {FMLtoHOL (version 1.0): Automating First-order Modal Logics with LEO-II and Friends},
author = {Christoph Benzmueller and Thomas Raths},
journal= {arXiv preprint arXiv:1207.6685},
year = {2012}
}
Comments
4 pages