Type System and Syntax
Requirements for the Type System
- Acceptable, with a low entry barrier
- Implementable, so existing tools can be adapted
- Beneficial, so that ATP performance improves
- Expressive enough, at least for arithmetic
A Simple Many-sorted Logic
- Sorts are atomic, inhabited, disjoint
- Equality is ad hoc polymorphic
- Uninterpreted symbols were monomorphic (TF0)
- Uninterpreted symbols are polymorphic (TF1)
- No subsorts (yet)
The TPTP Syntax
- $tType, $i, $o (plus numeric types)
- Declarations of sorts and signatures, defaults
- Typing of variables
- = stands for equality over all sorts
- Let expressions and conditional expressions
- $distinct