The TPTP Typed First-order Form with Arithmetic

Introduction

• Andrzej Trybulec (Andjray Triboolets) and Arithmetic
• Motivation and History

The TFF and TFA Languages

• TFF Type System and Syntax
• TFF Type Checking and Semantics
• TFF + Arithmetic = TFA
• TFA Semantics, Solvability, and Decidability

TPTP Problems

• TFA Problems in the TPTP
• Data Structure Example
• Number Theory Example
• Software Verification Example

TPTP Solutions

• TPTP World Tools
• ATP Systems with Arithmetic
• SystemOnTPTP

How Useful is That!?

The End - Any Questions?

---