TPTP Logical Formulae

Active Formulae

• Logical formulae are initially active
• They can be deactivated and (re)activated
• Inactive formulae are not used

Groups

• Logical formulae belong to one or more groups
• All belong to the tpi group
• axioms, hypothesiss, lemmas, etc. belong to the tpi_premises group
• conjectures and negated_conjectures beloing to the tpi_conjectures group
• Can belong to multiple other groups

Defined Terms

• $getargv gets interpreter's command line arguments
• $getenv gets environment variable values
• $getgroups gets logical formulae into a file