The TMTP Idea

What

• TPTP axiomatization problems
  • Contain only include directives for axiom files
  • Axiomatize some established theory
• Library of models for TPTP axiomatization problems
  • Written in the TPTP language
• Infrastructure for collecting models from the TSTP
• Functions for efficiently interpreting wrt an interpretation
• Tools for examining and manipulating interpretations

Why

• ATP semantically guided by fixed interpretation(s)
  • Semantic Resolution (Slagle, 1967, no implementations)
  • SRASS, SCOTT, SLM, etc.
  • 
• Semantic axiom selection in large theories
• Insights into semantic structure of axiomatizations