构建支持非经典逻辑的自动定理证明基础设施
TPTP World Infrastructure for Non-classical Logics
- 扩展TPTP语言以支持非经典逻辑形式化
- 提供多模态逻辑问题与求解器工具链
- 适合逻辑研究者与ATP系统开发者使用
TPTP世界是支持自动定理证明（ATP）系统的研究、开发与部署的成熟基础设施。该系统原支持多种经典逻辑，自版本v9.0.0起开始支持非经典逻辑。本文全面概述了TPTP世界在非经典逻辑领域的基础设施：包括非经典逻辑的语言扩展、问题与解决方案集，以及工具支持。文中详细描述了量化正常多模态逻辑的使用方法，为相关研究提供完整技术框架。
原文摘要 · Abstract (English)
The TPTP World is the well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. The TPTP World supports a range of classical logics, and since release v9.0.0 has supported non-classical logics. This paper provides a self-contained comprehensive overview of the TPTP World infrastructure for ATP in non-classical logics: the non-classical language extension, problems and solutions, and tool support. A detailed description of use of the infrastructure for quantified normal multi-modal logic is given.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。