TPTP Language Summary

A Key to Success

• Same language for input (problems) and output (derivations, models)
• Prolog like with a simple concrete syntax
• BNF is lex/yacc/flex/bison friendly

Extended BNF

• <source>      ::= <general_term>
• <source>      :== <dag_source> | <internal_source>
• <lower_word>  ::- <lower_alpha><alpha_numeric>*
• <lower_alpha> ::: [a-z]

Languages

• CNF and FOF - stable
• TFF and TFA - released and being used (maybe some changes coming)
• THF - THF0 core released, THF and THFX defined

Hyperlinked BNF available online at www.tptp.org/TPTP/SyntaxBNF.html

• Local copy