The TPTP World -
Infrastructure for Automated Reasoning
http://tptp.org

Introduction ^0:05

• ATP, What is it?
  • A Motivating Example
• ATP, What is it Good For?
• ATP, What Systems are Successful?
• TPTP Infrastructure
  • Another Motivating Example
• Tutorial on Logic and the TPTP World (++)

TPTP World Core Infrastructure ^0:10

• The TPTP Problem Library
• The TPTP Language (++)
• The SZS Ontologies
• The TSTP Solution Library
• Problem and System Ratings (++)
• The TPTP Process Instruction Language (++)

TPTP World Services ^0:25

• System*T*TP
  • Online - ATP in your Web Browser
  • Desktop - ATP on your Computer (++)
  • Remote - ATP in your Software (++)
• Derivation Tools
  • IDV - Interactive Derivation Viewer
  • AGInTRater - Derivation Nodes' Interestingness
  • GDV - Semantic Derivation Verification
• Interpretation Tools
  • IIV - Interactive Interpretation Viewer
  • AGMV - Semantic Model Verification

Using the TPTP World (--) ^1:00

• The TPTP Quick Guide
• SystemOnTPTP demonstration using PUZ001+1 and PUZ131_1
  • Start at the TPTP : http://tptp.org
  • Browse TPTP problems to PUZ001+1
  • Note language, SPC, Rating
  • Browse TSTP solutions to E solution, note language
  • Could rush forward to "Solve problem", but first ...
  • Copy formulae, open SystemB4TPTP : http://tptp.org/cgi-bin/SystemB4TPTP, and explain interface. Then check syntax using BNFParserDrill.
  • Open SystemOnTPTP : http://tptp.org/cgi-bin/SystemOnTPTP, and explain interface. Then check axioms using Paradox.
  • Add conjecture and prove with E. Note yacko proof, then redo with "TPTP format". Note language.
  • Could shortcut using SoTSTP, but first ... Copy formulae, open SystemOnTSTP : http://tptp.org/cgi-bin/SystemOnTSTP, and explain interface. Then check proof using GDV.
  • Run IDV on solution. Explain IDV interface. Show interestingness. Show "good/bad cat lemmas". Show verification.
  • Return to SystemB4TPTP : http://tptp.org/cgi-bin/SystemB4TPTP, and do PUZ131_1. Type check with TwHelFTC. Prove using Beagle. Translate to FOF by Isabelle, then Monotonox as an option. Prove FOF with E, look at IDV image and verify with GDV.
• Tutorial on Logic and the TPTP World
• The ATP Process

TPTP World Applications ^0:40

• Mathematics in Many Forms
• Certifiable program sythesis at NASA
• The Sledgehammer in Isabelle
• The Ontological Argument
• Some Internal Projects
  • SSCPA - Competitive Parallelism
  • AGInT - Generating Interesting Theorems
  • SRASS - Semantic Selection of Axioms
  • MANSEX - Multiple Answer Extraction
  • SPASS-XDB - External Data Access for ATP
• The CADE ATP System Competition

Conclusion ^{0:50 or 1:20}

• Work in Progress
• Why Does it Work?

The End - Any Questions?