TPTP World Infrastructure for Non-classical Logics
Alexander Steen, Geoff Sutcliffe
TL;DR
This paper presents a comprehensive overview of the TPTP World infrastructure's support for non-classical logics, including language extensions, problem handling, and tool support, with a detailed case study on multi-modal logic.
Contribution
It introduces the non-classical logic support in TPTP World, detailing language extensions, problem formats, and tool integration, enhancing ATP research in diverse logical systems.
Findings
Supports a range of non-classical logics since v9.0.0
Provides detailed infrastructure description and tool support
Includes a case study on multi-modal logic
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.