Implementing and Evaluating Provers for First-order Modal Logics
Implementing and Evaluating Provers for First-order Modal Logics
复制标题
一阶模态逻辑证明器的实现和评估
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Thomas Raths
中科院分区：
文献类型：
--
作者：
Christoph Benzmüller;J. Otten;Thomas Raths
虽然一阶模态逻辑的理论有大量的文献，但对它们的实际推理系统知之甚少。本文介绍了几种基于不同证明演算的一阶模态逻辑全自动定理证明器的实现。在这些演算中有标准的递归演算、前缀tableau演算、嵌入到简单类型理论、基于实例的方法和前缀连接演算。所有实现都在新的QMLTP问题库上进行了测试和评估，用于一阶模态逻辑。
While there is a broad literature on the theory of first-order modal logics, little is known about practical reasoning systems for them. This paper presents several implementations of fully automated theorem provers for first-order modal logics based on different proof calculi. Among these calculi are the standard sequent calculus, a prefixed tableau calculus, an embedding into simple type theory, an instance-based method, and a prefixed connection calculus. All implementations are tested and evaluated on the new QMLTP problem library for first-order modal logic.