Quantified Multimodal Logics in Simple Type Theory
Quantified Multimodal Logics in Simple Type Theory
复制标题
DOI：
10.1007/s11787-012-0052-y
复制
发表时间：
2013-03-01
影响因子：
0.8
通讯作者：
Paulson, Lawrence C.
中科院分区：
文献类型：
--
作者：
Benzmueller, Christoph;Paulson, Lawrence C.
我们提出了一种将量化多模态逻辑嵌入到简单类型理论中的方法，并证明了它的完备性。建立并利用了量化多模态逻辑的QKp模型与Henkin模型之间的对应关系。我们的嵌入支持应用现成的高阶定理证明，用于量化多模态逻辑内部和有关的推理。此外，它还为简单类型理论中进一步的逻辑嵌入及其组合提供了一个起点。
We present an embedding of quantified multimodal logics into simple type theory and prove its soundness and completeness. A correspondence between QKp models for quantified multimodal logics and Henkin models is established and exploited. Our embedding supports the application of off-the-shelf higher-order theorem provers for reasoning within and about quantified multimodal logics. Moreover, it provides a starting point for further logic embeddings and their combinations in simple type theory.