Motivation and Aims

Existing ATP Languages

• Most (including TPTP) are for logical formulae
• Minimal support for process control
• ITP systems provide rich command languages
• Some previous work for ATP
  • System specific control in input
  • APIs for external control
  • Generic command languages

Aims

• A generic TPTP command language
• Store, manipulate, reason about logical formulae
• Command formulae syntax same as logical formulae
• Command formulae at the same level as logical formulae
• Understood by ATP system or interpreter - TPI systems