The TPTP Language
A Key to Success
- Human-readable, machine-parsable, flexible, extensible
- Same language for input (problems) and output (derivations, models)
Inter-operability between systems and tools
-
Hierarchy of Languages
- CNF and FOF - stable and defacto standards
- TF0 and TH0 - stable and being used, with arithmetic
- TF1 and TH1 - stable, but not much use yet
- TX0 and TX1 - just released
- NX0 and NH0 - coming soon, NX1 and NH1 unclear
Annotated Formulae
Language Definition in BNF
- Extended BNF
-
<source> ::= <general_term>
-
<source> :== <dag_source> | <internal_source>
-
<lower_word> ::- <lower_alpha><alpha_numeric>*
-
<lower_alpha> ::: [a-z]
- LR1 - lex/yacc/flex/bison friendly
- Hyperlinked online