Combining and automating classical and non-classical logics in classical higher-order logics
Combining and automating classical and non-classical logics in classical higher-order logics
复制标题
DOI：
10.1007/s10472-011-9249-7
复制
发表时间：
2011-06-01
影响因子：
1.2
通讯作者：
Benzmueller, Christoph
中科院分区：
文献类型：
--
作者：
Benzmueller, Christoph
许多经典和非经典逻辑可以优雅地嵌入丘奇的简单类型理论，也被称为经典高阶逻辑。例子包括命题和量化的多模态逻辑，直觉逻辑，安全逻辑和空间推理逻辑。此外，简单类型理论对于嵌入式逻辑的组合建模具有足够的表达能力，并且具有很好的语义理解。现成的简单类型理论的推理系统存在，可以统一用于推理内和有关嵌入式逻辑和逻辑组合。在这篇文章中，我们专注于（量化）认知和doxastic逻辑的组合，并研究其应用建模和自动推理的理性代理。我们提出说明示例问题和报告的实验与现成的高阶自动定理证明。
Numerous classical and non-classical logics can be elegantly embedded in Church's simple type theory, also known as classical higher-order logic. Examples include propositional and quantified multimodal logics, intuitionistic logics, logics for security, and logics for spatial reasoning. Furthermore, simple type theory is sufficiently expressive to model combinations of embedded logics and it has a well understood semantics. Off-the-shelf reasoning systems for simple type theory exist that can be uniformly employed for reasoning within and about embedded logics and logics combinations. In this article we focus on combinations of (quantified) epistemic and doxastic logics and study their application for modeling and automating the reasoning of rational agents. We present illustrating example problems and report on experiments with off-the-shelf higher-order automated theorem provers.