TPTP World Infrastructure for Non-classical Logics
By: Alexander Steen, Geoff Sutcliffe
Potential Business Impact:
Helps computers prove math problems in new ways.
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.
Similar Papers
The Dependently Typed Higher-Order Form for the TPTP World
Logic in Computer Science
Lets computers understand more complex math problems.
SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus
Logic in Computer Science
Lets computers share and check math proofs.
Automated Theorem Proving for Prolog Verification
Logic in Computer Science
Proves computer programs are correct and won't crash.