TPTP World Infrastructure for Non-classical Logics
Logic in Computer Science
2025-08-14 v1 Artificial Intelligence
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.
Keywords
Cite
@article{arxiv.2508.09318,
title = {TPTP World Infrastructure for Non-classical Logics},
author = {Alexander Steen and Geoff Sutcliffe},
journal= {arXiv preprint arXiv:2508.09318},
year = {2025}
}
Comments
35 pages