Introduction

The TPTP World

• TPTP problem library, TSTP solution library
• TPTP language standards, SZS status standards
• Services and tools
• The CADE ATP System Competition (CASC)
• De facto platform for ATP research and development

The Logic Languages

• First-order ... CNF and FOF
• Typed first-order ... TFF and TXF (0 & 1)
• Typed higher-order ... THF (0 & 1)
• Non-classical ... NXF and NHF (0 & 1?)

Logic "Languages"

• I don't like Greek letters
• I'm scared of logicians