HOL Based First-Order Modal Logic Provers
HOL Based First-Order Modal Logic Provers
复制标题
基于 HOL 的一阶模态逻辑证明器
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Thomas Raths
中科院分区：
文献类型：
--
作者：
Christoph Benzmüller;Thomas Raths
一阶模态逻辑（FML）可以被建模为经典高阶逻辑（HOL）的自然片段。FMLtoHOL工具利用了这一事实，它支持应用现成的HOL证明器和模型查找器在FML中进行推理。该工具在FML的qmf语法和HOL的TPTP thf0语法之间建立了桥梁。它目前支持逻辑K、K4、D、D4、T、S4和S5，涉及恒定、变化和累积域语义。结合HOL的元证明器，顺序调度各种HOL推理机的方法进行评估。由此产生的系统非常有竞争力。
First-order modal logics (FMLs) can be modeled as natural fragments of classical higher-order logic (HOL). The FMLtoHOL tool exploits this fact and it enables the application of off-the-shelf HOL provers and model finders for reasoning within FMLs. The tool bridges between the qmf-syntax for FML and the TPTP thf0-syntax for HOL. It currently supports logics K, K4, D, D4, T, S4, and S5 with respect to constant, varying and cumulative domain semantics. The approach is evaluated in combination with a meta-prover for HOL, which sequentially schedules various HOL reasoners. The resulting system is very competitive.
使用分析表和相关方法进行自动推理
DOI：
10.1007/978-3-642-40537-2_17
发表时间：
2013
期刊：
--
影响因子：
--
作者：
Khodadadi M
通讯作者：
Khodadadi M