How Useful is That!?

New(ish) Capability for ATP

• Arithmetic in full first-order logic (no constraints)
• Three numeric types (more than other frameworks)
• A bunch of ATP problems
• A bunch of ATP systems

TPTP World

• Standardized in the TPTP infrastructure
• Parsers
• TPTP2X and TPTP4X
• Type checker for TFF

What are the New(ish) Applications?

• Mathematics
• Hardware and Software Verification
• Science and engineering
• Finance and business
• Quantitative spatial and temporal reasoning
• Commonsense reasoning
• ... and many more I'm sure

Future Work for Them and You and Me

• Type checker for TFA (him)
• Proof output (them)
• New ATP systems (him and him)
• GDV and IDV (me)
• Contribute to SMT (me, them)
• More applications (you)