Logic for Programming, Artificial Intelligence, and Reasoning

Logic for Programming, Artificial Intelligence, and Reasoning
复制标题

编程逻辑、人工智能和推理

DOI：
10.1007/978-3-642-45221-5_9
复制
发表时间：
2013
期刊：
--
影响因子：
--
通讯作者：
Benzmüller C
Benzmüller C
中科院分区：
--
文献类型：
--
作者：
Benzmüller C

文献摘要

被引文献

相似文献

一阶模态逻辑（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). TheFMLtoHOLtool 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.