Interpreted Predicates and Functors

Interpreted Symbols

• Start with $ or are non-alphanumeric
• Truth values, $true and $false
• Predicates, e.g., =, !=, $distinct
• Types, e.g., $tType, $i, $o, $int
• Arithmetic, e.g., $greater, $sum

Interpreted Functors

• Distinct objects
  • Written in "double quotes"
  • Interpreted as the domain elements in the "double quotes"s
• Numbers
  • Interpreted as themselves (as domain elements)
• Known to be unequal, e.g., "Apple" != "Microsoft" and 1 != 2

System predicates and functors

• Start with $$
• For predicates and functors interpreted by specific systems
• Not controlled by TPTP language