TPTP World Infrastructure for Non-classical Logics

2025/08/12 by Steen, Alexander, Sutcliffe, Geoff · 1 citation
#68T27 #Artificial Intelligence (cs.AI) #F.4.1 #FOS: Computer and information sciences #I.2.3 #I.2.4 #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2508.09318

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.

Citations

• The TPTP Format for Interpretations
• An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning
• Automated Reasoning in Non-classical Logics in the TPTP World
• Dynamic term-modal logics for first-order epistemic planning
• Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support
• Formalization, Mechanization and Automation of G"odel's Proof of God's Existence
• Reasoning in the OWL 2 Full Ontology Language using First-Order Automated Theorem Proving
• Quantified Multimodal Logics in Simple Type Theory
• A methodology for hardware verification based on logic simulation

Cited by

• A Reduction of Input/Output Logics to SAT

Related

• Automated Reasoning in Non-classical Logics in the TPTP World
• Solving Quantified Modal Logic Problems by Translation to Classical Logics
• Automating Quantified Multimodal Logics in Simple Type Theory -- A Case Study
• An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning
• Learning to Reason