# Automated Reasoning in Non-classical Logics in the TPTP World

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 3 of its 60 references that are in the map.
- First posted on arXiv 20 Feb 2022.

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

- [Extensional Higher-Order Paramodulation in Leo-III](https://mlsanity.com/paper/1907.11501/) (2019)
- [Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy](https://mlsanity.com/paper/2111.01654/) (2021)
- [A First Class Boolean Sort in First-Order Theorem Proving and TPTP](https://mlsanity.com/paper/1505.01682/) (2015)

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

- [An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning](https://mlsanity.com/paper/2203.12352/) (2022)
- [Bridging between LegalRuleML and TPTP for Automated Normative Reasoning (extended version)](https://mlsanity.com/paper/2209.05090/) (2022)
- [TPTP World Infrastructure for Non-classical Logics](https://mlsanity.com/paper/2508.09318/) (2025)
- [A Reduction of Input/Output Logics to SAT](https://mlsanity.com/paper/2508.16242/) (2025)

## Abstract (arXiv)

Non-classical logics are used in a wide spectrum of disciplines, including artificial intelligence, computer science, mathematics, and philosophy. The de-facto standard infrastructure for automated theorem proving, the TPTP World, currently supports only classical logics. Similar standards for non-classical logic reasoning do not exist (yet). This hampers practical development of reasoning systems, and limits their interoperability and application. This paper describes the latest extension of the TPTP World, which provides languages and infrastructure for reasoning in non-classical logics. The extensions integrate seamlessly with the existing TPTP World.