...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Annals of Mathematics and Artificial Intelligence >Combining and automating classical and non-classical logics in classical higher-order logics
【24h】

Combining and automating classical and non-classical logics in classical higher-order logics

机译：在古典高阶逻辑中组合和自动化古典和非古典逻辑

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

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) epis-temic 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.
机译：许多经典和非经典逻辑可以优雅地嵌入到Church的简单类型理论中，也称为经典高阶逻辑。示例包括命题和量化的多峰逻辑，直觉逻辑，安全逻辑和空间推理逻辑。此外，简单类型理论足以表达嵌入式逻辑的组合模型，并且具有很好的语义。存在用于简单类型理论的现成的推理系统，其可以被统一地用于嵌入式逻辑和逻辑组合之内和周围的推理。在本文中，我们将重点放在（量化的）流行的逻辑和十进制逻辑的组合上，并研究它们在建模和自动化有理智能体推理方面的应用。我们展示了示例问题，并提供了有关现成的高阶自动定理证明的实验报告。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号