%----Version 3.1.1.13c (TPTP version.internal development number)
%----Intended uses of the various parts of the TPTP syntax are explained
%----in the TPTP technical manual, linked from www.tptp.org.
%----See the <comment> entries regarding text that can be discarded before 
%----tokenizing for this syntax.
%----White space is almost irrelevant, but, for the Prolog people, all tokens
%----consisting of non-alphanumeric characters shuold be followed bya space.

%----Files. Empty file is OK.
<TPTP file>          ::= <TPTP input>*
<TPTP input>         ::= <annotated formula> | <include> |
                         <comment> | <system comment>

%----Formula records
<annotated formula>  ::= <fof annotated> | <cnf annotated> |
                         <TPTP input formula> | <TPTP input clause>
%----Future languages may include ...  english | efof | tfof | mathml | ...
<fof annotated>      ::= fof(<name>,<formula role>,<fof formula><annotations>).
<cnf annotated>      ::= cnf(<name>,<formula role>,<cnf formula><annotations>).
<annotations>        ::= <null> | ,<source> | ,<source>,<useful info>

%----Types for problems.
%----Note: The previous <source type> from ...
%----   <formula role> ::= <user role>-<source> 
%----... is now gone. Parsers may choose to be tolerant of it for backwards 
%----compatibility.
<formula role>       ::= <atomic word>
<formula role>       :== axiom |
                         hypothesis |
                         definition |
                         lemma |
                         theorem |
                         conjecture |
                         lemma_conjecture |
                         negated_conjecture |
                         plain |
                         unknown
%----"axiom"s are accepted, without proof, as a basis for proving "conjecture"s 
%----and "lemma_conjecture"s in FOF problems. In CNF problems "axiom"s are 
%----accepted as part of the set whose satisfiability has to be established.
%----There is no guarantee that the axioms of a problem are consistent.
%----"hypothesis"s are assumed to be true for a particular problem, and are 
%----used like "axiom"s.
%----"definition"s are used to define symbols, and are used like "axiom"s.
%----"lemma"s and "theorem"s have been proven from the "axiom"s, can be used 
%----like "axiom"s, but are redundant wrt the "axiom"s. "lemma" is used as the 
%----role of proven "lemma_conjecture"s, and "theorem" is used as the role of 
%----proven "conjecture"s, in output. A problem containing a "lemma" or 
%----"theorem" that is not redundant wrt the "axiom"s is ill-formed. "theorem"s
%----are more important than "lemma"s from the user perspective.
%----"conjecture"s occur in only FOF problems, and are to all be proven from 
%----the "axiom"(-like) formulae. A problem is solved only when all 
%----"conjecture"s are proven.
%----"lemma_conjecture"s are expected to be provable, and may be useful to 
%----prove, while proving "conjecture"s.
%----"negated_conjecture"s ocuur in only CNF problems, and are formed from
%----negation of a "conjecture" in a FOF to CNF conversion.
%----"plain"s have no special user semantics, and can be used like "axiom"s.
%----"unknown"s have unknown role, and this is an error situation.

%----FOF formulae. All formulae must be closed.
<fof formula>        ::= <binary formula> | <unitary formula>
<binary formula>     ::= <nonassoc binary> | <assoc binary>
%----Only some binary connectives are associative
%----There's no precedence amoung binary connectives
<nonassoc binary>    ::= <unitary formula> <binary connective> <unitary formula>
<binary connective>  ::= <=> | => | <= | <~> | ~<vline> | ~&
%----Associative connectives & and | are in <assoc binary>
<assoc binary>       ::= <or formula> | <and formula>
<or formula>         ::= <unitary formula> <vline> <unitary formula>
                         <more or formula>*
<more or formula>    ::= <vline> <unitary formula>
<and formula>        ::= <unitary formula> & <unitary formula>
                         <more and formula>*
<more and formula>   ::= & <unitary formula>
%----<unitary formula> are in ()s or do not have a <binary connective> at the 
%----top level.
<unitary formula>    ::= <quantified formula> | <unary formula> |
                         (<fof formula>) | <atomic formula>
<quantified formula> ::= <quantifier> [<variable list>] : <unitary formula>
<quantifier>         ::= ! | ?
%----! is universal quantification and ? is existential. Syntactically, the 
%----quantification is the left operand of :, and the <unitary formula> is 
%----the right operand. Although : is a binary operator syntactically, it is 
%----not a <binary connective>, and thus a <quantified formula> is a 
%----<unitary formula>.
%----Universal   example: ! [X,Y] : ((p(X) & p(Y)) => q(X,Y)).
%----Existential example: ? [X,Y] : (p(X) & p(Y)) & ~ q(X,Y).
%----Quantifiers have higher precedence than binary connectives, so in
%----the existential example the quantifier applies to only (p(X) & p(Y)).
<variable list>      ::= <variable> | <variable>,<variable list>
%----Future variables may have sorts and existential counting
%----Unary connectives bind more tightly than binary
<unary formula>      ::= <unary connective> <unitary formula>
<unary connective>   ::= ~

%----CNF formulae (variables implicitly universally quantified)
<cnf formula>        ::= (<disjunction>) | <disjunction>
<disjunction>        ::= <literal> <more disjunction>*
<more disjunction>   ::= <vline> <literal>
<literal>            ::= <atomic formula> | ~ <atomic formula>

%----Atoms (<predicate> is not used currently)
<atomic formula>     ::= <plain atom> | <defined atom> | <system atom>
<plain atom>         ::= <plain term>
%----A <plain atom> looks like a <plain term>, but really we mean
%----  <plain atom>         ::= <proposition> | <predicate>(<arguments>)
%----  <proposition>        ::= <atomic word>
%----  <predicate>          ::= <atomic word>
%----Using <plain term> removes a reduce/reduce ambiguity in lex/yacc.
<arguments>          ::= <term> | <term>,<arguments>
<defined atom>       ::= $true | $false |
                         <term> = <term> | <term> != <term>
%----Some systems still interprete equal/2 as equality. The use of equal/2
%----for other purposes is therefore discouraged. Please refrain from either 
%----use. Use infix '=' for equality. Note: <term> != <term> is equivalent
%----to ~ <term> = <term>
%----More defined atoms may be added in the future.
<system atom>        ::= <system term>
%----<system atom>s are used for evaluable predicates that are available
%----in particular tools. The predicate names are not controlled by the
%----TPTP syntax, so use with due care. The same is true for <system term>s.

%----Terms
<term>               ::= <function term> | <variable>
<function term>      ::= <plain term> | <defined term> | <system term>
<plain term>         ::= <constant> | <functor>(<arguments>)
<constant>           ::= <atomic word>
<functor>            ::= <atomic word>
%----<numbers>s and <distinct object>s are always interpreted as themselves
<defined term>       ::= <number> | <distinct object>
<system term>        ::= <system constant> | <system functor>(<arguments>)
<system functor>     ::= <atomic system word>
<system constant>    ::= <atomic system word>
<variable>           ::= <upper word>

%----Formula sources
<source>             ::= <general function>
<source>             :== <dag source> | <internal source> | <external source> |
                         unknown
%----Only a <dag source> can be a <name>, i.e., derived formulae can be
%----identified by a <name> or an <inference record> 
<dag source>         :== <name> | <inference record>
<inference record>   :== inference(<inference rule>,<useful info>,
                         [<parent info list>])
<inference rule>     :== <atomic word>
%----Examples are        deduction | modus_tollens | modus_ponens | rewrite | 
%                        resolution | paramodulation | factorization | 
%                        cnf_conversion | cnf_refutation | ...
<parent info list>   :== <parent info> | <parent info>,<parent info list>
<parent info>        :== <source><parent details>
<theory>             :== theory(<theory name>)
<theory name>        :== equality | ac
%----More theory names may be added in the future.
<parent details>     :== :<atomic word> | <null>
<internal source>    :== introduced(<intro type><intro info>)
<intro type>         :== definition | axiom_of_choice | tautology
%----This should be used to record the symbol being defined, or the function
%----for the axiom of choice
<intro info>         :== ,<useful info> | <null>
<external source>    :== <file source> | <creator source> | <theory>
<file source>        :== file(<file name>,<file node name>)
<file node name>     :== <name> | unknown
<creator source>     :== creator(<creator name><creator info>)
<creator name>       :== <atomic word>
<creator info>       :== ,<useful info> | <null>

%----File name and Useful Info fields
<file name>          ::= <atomic word>
<useful info>        ::= <general list>
<useful info>        :== [] | [<info items>]
<info items>         :== <info item> | <info item>,<info items>
<info item>          :== <formula item> | <inference item> | <general function>
%----Useful info for formula records
<formula item>       :== <description item> | <iquote item> 
<description item>   :== description(<atomic word>)
<iquote item>        :== iquote(<atomic word>)
%----Useful info for inference records
<inference item>     :== <inference status> | <refutation>
<inference status>   :== status(<status value>)
%----These are the status values from the SZS ontology
<status value>       :== tau | tac | eqv | thm | sat | cax | noc | csa | cth |
                         ceq | unc | uns | sab | sam | sar | sap | csp | csr |
                         csm | csb
<inference info>     :== <inference rule>(<atomic word>,<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 list>]
<name list>          ::= <name> | <name>,<name list>

%----General purpose
<general term>       ::= <general function> | <general list>
<general list>       ::= [] | [<general arguments>]
<general function>   ::= <name> | <functor>(<general arguments>)
<general arguments>  ::= <general term> | <general term>,<general arguments>
%----The following are reserved <name>s: unknown file inference creator
<name>               ::= <atomic word> | <unsigned integer>
<atomic word>        ::= <lower word> | <single quoted>
<null>               ::=

%----All numbers are implicitly distinct
<number>             ::= <real> | <integer>
<integer>            ::= <signed integer> | <unsigned integer>


%------------------------------------------------------------------------------
%----Rules from here on down are for defining tokens (terminal symbols)
%----of the grammar, assuming they will be recognized by a lexical scanner.

%----Usual regexp notation is used mostly, as in grep, lex, awk, sed, etc.
%----[ ] denotes a selection of ONE of the enclosed characters; e.g.
%----[0-9] means one digit.  Inside [ ], special meanings are disabled;
%----e.g., [.] is a period whereas . is any character except a newline.
%----[^abc] means any character EXCEPT a, b, or c.  [\^] matches a caret.
%----[\\] matches a backslash.  See lex/flex documentation for details.
%----For uniformity and safety, [ ] is placed around single characters even
%----when not necessary.

%----A ::- rule defines a token.
%----A ::: rule defines a macro that is not a token.
%----"..." means the definition is imprecise and manual coding is needed.
%----"% $$" provides semantic information, and explains "...".
<digit>                ::: [0-9]
<lower>                ::: [a-z]
<upper>                ::: [A-Z]
<alphanum>             ::: (<lower>|<upper>|<digit>|[_])
<any char>             ::: (.|\n)
<ddollar>              ::: [$][$]

<vline>                ::- [|] ...
% $$ token for <vline> is VLINE, conflicts with meta-symbol, hard-coded.

<real>                 ::- (<signed integer>|<unsigned integer>)<decimal part>
<signed integer>       ::- [+-]<unsigned integer>
<unsigned integer>     ::- <digit><digit>*
<decimal part>         ::- [.]<digit><digit>*

<upper word>           ::- <upper><alphanum>*
<lower word>           ::- <lower><alphanum>*
<atomic system word>   ::- <ddollar><lower><alphanum>*

%----System Comments are used for system specific annotation of anything.
%----They look like comments (see next), 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 begin $$, then identify the system,
%----followed by a :, e.g., /* $$ Otter 3.3: Demodulator */

%----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.

% $$ A string that matches both <system comment> and <comment> should be
% $$ recognized as <system comment>.
<system comment>       ::- <system comment one>|<system comment multi>
<comment>              ::- <comment one>|<comment multi>
<system comment one>   ::: [%][ ]*<ddollar>.*
<system comment multi> ::: [/][*][ ]*<ddollar>([^*]*[*][*]*[^/*])*[^*]*[*][*]*[/]
% $$ Approximately, [/][*][ ]*<ddollar><any char>*[*][/]
% $$ Correct regexp ends at FIRST [*][/]
% $$ See comment for <comment multi> below.
<comment one>          ::: [%].*
<comment multi>        ::: [/][*]([^*]*[*][*]*[^/*])*[^*]*[*][*]*[/]
% $$ Approximately, [/][*]<any char>*[*][/]
% $$ Correct regexp ends at FIRST [*][/]
% $$ BEWARE: lex will end at the LAST [*][/] in the whole file if you let it.

% $$ <single quoted> and <distinct object> must contain only "printing ASCII",
% $$ which includes space, and consists of ASCII codes 40-126 decimal.

<single quoted>        ::- [']([^\\']|[\\][']|[\\][\\])*[']
% $$ ['].*['] would be OK except for escape sequences.
% $$ \ is used as the escape character for ' and \ in <single quoted>;
% $$ i.e., \' is  backslash-quote and \\ is backslash-backslash.
% $$ For input and output in TPTP syntax the \ is present.

%----All <distinct object>s are implicitly unequal; ~("a" = "b"). 
<distinct object>      ::- ["]([^\\"]|[\\]["]|[\\][\\])*["]
% $$ ["].*["] would be OK except for escape sequences.
% $$ \ is used as the escape character for " and \ in <distinct object>;
% $$ i.e., \" is  backslash-quote and \\ is backslash-backslash.
% $$ For input and output in TPTP syntax the \ is present.

%------------------------------------------------------------------------------
%----If you are writing a new TPTP parser, you do not need to parse the old
%----style TPTP formulae, i.e., ignore from here on down.
%----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>,<formula role>,<fof formula>).
<TPTP CNF file>      ::= <TPTP CNF input>*
<TPTP CNF input>     ::= <TPTP input clause> | <include> | <comment>
<TPTP input clause>  ::= input_clause(<name>,<formula role>,<TPTP literals>).

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