# TPTP World Infrastructure for Non-classical Logics

arXiv: https://arxiv.org/abs/2508.09318 · HTML: https://mlsanity.com/paper/2508.09318/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 112 references that are in the map.
- First posted on arXiv 12 Aug 2025.

## Builds on (most cited first, 6 of 6)

- [Extensional Higher-Order Paramodulation in Leo-III](https://mlsanity.com/paper/1907.11501/) (2019)
- [Formalization, Mechanization and Automation of G"odel's Proof of God's Existence](https://mlsanity.com/paper/1308.4526/) (2013)
- [Automated Reasoning in Non-classical Logics in the TPTP World](https://mlsanity.com/paper/2202.09836/) (2022)
- [An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning](https://mlsanity.com/paper/2203.12352/) (2022)
- [A First Class Boolean Sort in First-Order Theorem Proving and TPTP](https://mlsanity.com/paper/1505.01682/) (2015)
- [The TPTP Format for Interpretations](https://mlsanity.com/paper/2406.06108/) (2024)

## Built on by (most cited first, 1 of 1)

- [A Reduction of Input/Output Logics to SAT](https://mlsanity.com/paper/2508.16242/) (2025)

## Abstract (arXiv)

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.