TF0: The Monomorphic Typed First-order Form

Overview

• Extends FOF with types and type declarations
• Functions and predicates are declared with a type signature

Types and Type Signatures

• Types
  • The predefined types $i for ι (individuals) and $o for ο (booleans)
  • The predefined arithmetic types $int for integers, $rat for rationals, $real for reals
  • User-defined types (constants)

• Type Signatures
  • Individual types τ
  • (τ₁ * ... * τ_n) > τ^~ for n > 0

Notes

• Use of functions and predicates must respect the type signature
• When used with Arithmetic, known as "TFA"

TF0 Example