Conclusion

In the Short Term

• I did this to clarify my big picture
• The TSTP is not a result in itself, but ...
  • It has required some non-trivial software development and organization
  • It will immediately contribute to the development of ATP systems

In the Long Term

• Wil provide a basis for understanding and comparing proof structures
• Will be used for certification of ATP systems
• Will form a framework within which problems will be formulated and solved using ATP tools and techniques.

Immediate Plans

• Mechanism for incremental conversion of human proofs to (verified) machine proofs
• Mining the TSTP for proof abstractions and lemmas
• TSTP format for models
• Proofs in homological algebra