Multimodal and intuitionistic logics in simple type theory1
Multimodal and intuitionistic logics in simple type theory1
复制标题
DOI：
10.1093/jigpal/jzp080
复制
发表时间：
2010-12-01
影响因子：
1
通讯作者：
Paulson, Lawrence C.
中科院分区：
文献类型：
--
作者：
Benzmueller, Christoph;Paulson, Lawrence C.
我们研究了简单类型理论中命题正规多模态逻辑和命题直觉逻辑的直接嵌入。这些嵌入的正确性很容易证明。我们给出的例子表明，这些嵌入提供了一个有效的框架，各种非经典逻辑的计算调查。我们报告了一些实验使用高阶自动定理证明LEO-II。
We study straightforward embeddings of propositional normal multimodal logic and propositional intuitionistic logic in simple type theory. The correctness of these embeddings is easily shown. We give examples to demonstrate that these embeddings provide an effective framework for computational investigations of various non-classical logics. We report some experiments using the higher-order automated theorem prover LEO-II.