%----See the <comment> entries regarding text that can be discarded before 
%----tokenizing for this syntax.

%----Formulae
<TPTP file>          ::= <TPTP input>+
<TPTP input>         ::= <annotated formula> | <include> | <comment>

%----Formula records
<annotated formula>  ::= <language>(<name>,<type>,<fol formula><extra annotations>).
<extra annotations>  ::= <null> | ,<source> | ,<source>,<useful info>
<language>           ::= cnf | fof 
%----Future languages may include ...  english | efof | tfof | mathml | ...

%----Types for problems
<type>               ::= <user type>-<source type> | <user type> | <source type>
<user type>          ::= axiom | hypothesis | conjecture | negated_conjecture |
                         lemma | theorem | plain | unknown
%----Future user types may include ... definition | knowledge | 
<source type>        ::= derived
%----A formula whose <type> formed from just a <user type> is an initial
%----formula provided as input, e.g., "axiom" means an initial axiom.

%----FOL formulae
<fol formula>        ::= <literal formula> | <binary formula>
<literal formula>    ::= <atomic formula> | <unary formula>
<atomic formula>     ::= <quantified formula> | <bracketed formula> | <atom>
<bracketed formula>  ::= (<fol formula>)
%----Quantifers have higher precedence than binary connectives
<quantified formula> ::= <quantifier> <variables> : <literal formula>
<quantifier>         ::= ! | ?
<variables>          ::= [<variable><rest of variables>*]
<rest of variables>  ::= ,<variable>
%----Future variables may have sorts and existential counting
%----Binary formulae are right associative
<binary formula>     ::= <literal formula> <binary connective> <logic formula>
%----Unary connectives bind more tightly than binary
<unary formula>      ::= <unary connective> <literal formula>
<binary connective>  ::= & | <=> | => | <= | vline | <~> | ~vline | ~&
<unary connective>   ::= ~

%----Terms
<atom>               ::= <theory atom> | <user atom>
<theory atom>        ::= <term> = <term> | <term> != <term> | 
                         equal(<term>,<term>) |
                         $true | $false 
<user atom>          ::= <proposition> | <predicate>(<arguments>)
<proposition>        ::= <lower word>
<predicate>          ::= <lower word>
<arguments>          ::= <term><rest of terms>*
<rest of terms>      ::= ,<term>
<term>               ::= <function> | <variable>
<function>           ::= <theory function> | <user function>
<theory function>    ::= <number> | <string>
<user function>      ::= <constant> | <functor>(<arguments>)
<functor>            ::= <lower word>
<constant>           ::= <lower word> | <quoted string>
<variable>           ::= <upper word>
<variable type>      ::= <lower word>

%----Formula sources
<source>             ::= <dag source> | <external source> | unknown
<dag source>         ::= <name> | <inference record>
<inference record>   ::= inference(<inference rule>,<useful info>,
                             [<parent info><rest parent info>*])
<inference rule>     ::= <lower word>
%----Others may be       deduction | modus_tollens | modus_ponens | rewrite | 
%                        resolution | paramodulation | factorization | 
%                        cnf_conversion | cnf_refutation | ...
<rest parent info>   ::= ,<parent info>
<parent info>        ::= <parent source><parent details>
<parent source>      ::= <source> | <theory>
<theory>             ::= theory(<theory name>)
<theory name>        ::= equality | ac | ...
<parent details>     ::= -<quoted string> | <null>
<external source>    ::= <file source> | <creator source> | <theory>
<file source>        ::= file(<file name>,<file node name>)
<file name>          ::= <quoted string>
<file node name>     ::= <name> | unknown
<creator source>     ::= creator(<creator name>,<useful info>)
<creator name>       ::= <quoted string>

%----Useful info fields
<useful info>        ::= [] | [<info items>]
<info items>         ::= <info item><rest of info items>*
<rest of info items> ::= ,<info item>
<info item>          ::= <formula item> | <inference item> | <general function>
%----Useful info for formula records
<formula item>       ::= <description item> | <iquote item> 
<description item>   ::= description(<quoted string>)
<iquote item>        ::= iquote(<quoted string>)
%----Useful info for inference records
<inference item>     ::= <inference status> | <refutation>
<inference status>   ::= status(<status value>) | <inference info>
<status value>       ::= thm | sat | ... 
<inference info>     ::= <inference rule>(<constant>,<general list>)
<refutation>         ::= refutation(<file source>)
%----Useful info for creators is just <general function>

%----Include directives
<include>            ::= include(<file name><formula selection>).
<formula selection>  ::= <null> | <name> | [<name><rest names>*]
<rest names>         ::= ,<name>

%----Comments. These may be retained for non-logical purposes. Comments
%----can occur only between annotated formulae (see <TPTP input>), but
%----it seems likely that people will put them elsewhere and simply
%----strip them before tokenising.
<comment>            ::= %<char until eoln>* | /<star><char>*<star>/
%----Annotations are used for system specific annotation of anything. Notice
%----that they look like comments, so by default they are discarded. However,
%----a wily user of the syntax can notice the @ and store/extract information 
%----from the "comment". System specific annotations should identify the 
%----system, followed by a :, after the @, e.g., /*@Otter 3.3: Demodulator */
<annotation>         ::= %@<char until eoln>* | /<star>@char>*<star>/ 

%----General purpose
<general term>       ::= <general function> | <quoted string> | <general list>
<general list>       ::= [] | [<general arguments>]
<general function>   ::= <constant> | <functor>(<general arguments>)
<general arguments>  ::= <general term><rest of gterms>*
<rest of gterms>     ::= ,<general term>
<name>               ::= <lower word>
<upper word>         ::= <A-Z><a-z0-9A-Z_>*
<lower word>         ::= <a-z><a-z0-9A-Z_>*
<quoted string>      ::= '<char>*'
<number>             ::= <sign><unsigned integer><decimal part>
<sign>               ::= + | - | <null>
<unsigned integer>   ::= <0-9>+
<decimal part>       ::= .<0-9>+ | <null>
<string>             ::= "<char>*"
<char>               ::= ... any printable ASCII character
<star>               ::= ... a star character
<plus>               ::= ... a plus character
<null>               ::=

%----Old style TPTP clauses and formulae
<TPTP FOF file>      ::= <TPTP FOF input>+
<TPTP FOF input>     ::= <TPTP input formula> | <include> | <comment>
<TPTP input formula> ::= input_formula(<name>,<type>,<logic formula>).
<TPTP CNF file>      ::= <TPTP CNF input>+
<TPTP CNF input>     ::= <TPTP input clause> | <include> | <comment>
<TPTP input clause>  ::= input_clause(<name>,<type>,<TPTP literals>).

%----Old TPTP style CNF
<TPTP literals>      ::= [] | [<TPTP literal><rest of TPTP literals>*]
<rest of TPTP literals> ::= ,<TPTP literal>
<TPTP literal>       ::= <TPTP sign><atom>
<TPTP sign>          ::= ++ | --

