首页> 外文会议>Automated reasoning with analytic tableaux and related methods >Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
【24h】

Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics

机译:特邀演讲:关于(相当)普遍定理证明方法及其在形而上学中的应用

获取原文
获取原文并翻译 | 示例

摘要

Classical higher-order logic is suited as a meta-logic in which a range of other logics can be elegantly embedded. Interactive and automated theorem provers for higher-order logic are therefore readily applicable. By employing this approach, the automation of a variety of ambitious logics has recently been pioneered, including variants of first-order and higher-order quantified multimodal logics and conditional logics. Moreover, the approach supports the automation of meta-level reasoning, and it sheds some new light on meta-theoretical results such as cut-elimination. Most importantly, however, the approach is relevant for practice: it has recently been successfully applied in a series of experiments in metaphysics in which higher-order theorem provers have actually contributed some new knowledge.
机译:经典的高阶逻辑适合作为元逻辑,其中可以优雅地嵌入一系​​列其他逻辑。因此,用于高阶逻辑的交互式和自动定理证明很容易适用。通过采用这种方法,最近开创了各种雄心勃勃的逻辑的自动化,包括一阶和高阶量化多峰逻辑和条件逻辑的变体。此外,该方法支持元级推理的自动化,并且为元理论结果(例如删减)提供了新的思路。但是,最重要的是,该方法与实践有关:最近,它已成功地用于形而上学的一系列实验中,其中高阶定理证明者实际上贡献了一些新知识。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号