Progress in the Development of
Automated Theorem Proving for
Higher-order Logic

The First-order TPTP World: TPTP, TSTP, Infrastructure, CASC

Higher-order ATP needs a TPTP World

The Higher-order TPTP World

• The THF Language
• TPTP Problems
• TSTP Solutions
• THF Tools

Higher-order ATP Systems

• LEO II
• TPS-GOOD1
• IsabelleP and IsabelleM and IsabelleN
• TSTP Solutions

Conclusion

• Cunning Plans for the Future
• Current Status

The End - Any Questions?