标题： TPTP 世界非经典逻辑基础设施 显示英文标题

标题： TPTP World Infrastructure for Non-classical Logics

摘要： TPTP World 是支持自动定理证明（ATP）系统的研究、开发和部署的已建立的基础架构。 TPTP World 支持一系列经典逻辑，并且自版本 v9.0.0 起支持非经典逻辑。 本文提供了 TPTP World 基础架构在非经典逻辑中的自包含全面概述：非经典语言扩展、问题和解决方案，以及工具支持。 给出了对量化正常多模态逻辑使用该基础架构的详细描述。 显示英文摘要

摘要： 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.