%----v3.2.0.3 (TPTP version.internal development number)
% Includes TFF
% <variable> and (<fof_formula>) as <general_data>
% Added letrecs to tff
% Added $distinct as a defined pred - needed for SMT
% Added $vector_int, $vector_real, $matrix_int, $matrix_real as defined types.
% Disallowed extra ()s around <tff_unitary_type>
% Removed $lambda and ->
%------------------------------------------------------------------------------
%----README ... this header provides important meta- and usage information
%----
%----Intended uses of the various parts of the TPTP syntax are explained
%----in the TPTP technical manual, linked from www.tptp.org.
%----
%----Four kinds of separators are used, to indicate different types of rules:
%---- ::= is used for regular grammar rules, for syntactic parsing.
%---- :== is used for semantic grammar rules. These define specific values
%---- that make semantic sense when more general syntactic rules apply.
%---- ::- is used for rules that produce tokens.
%---- ::: is used for rules that define character classes used in the
%---- construction of tokens.
%----
%----White space may occur between any two tokens. White space is not specified
%----in the grammar, but there are some restrictions to ensure that the grammar
%----is compatible with standard Prolog: a <TPTP_file> should be readable with
%----read/1.
%----
%----The syntax of comments is defined by the <comment> rule. Comments may
%----occur between any two tokens, but do not act as white space. Comments
%----will normally be discarded at the lexical level, but may be processed
%----by systems that understand them (e.g., if the system comment convention
%----is followed).
%----
%----Four languages are defined first - THF, TFF, FOF, and CNF. Depending on
%----your need, you can implement just the one(s) you need. The common rules
%----for atoms, terms, etc, come after the definitions of the languages, and
%----they are all needed for all four languages (except for the core THF0,
%----which is a defined subset of THF).
%----Top of Page---------------------------------------------------------------
%----Files. Empty file is OK.
<TPTP_file> ::= <TPTP_input>*
<TPTP_input> ::= <annotated_formula> | <include>
%----Formula records
<annotated_formula> ::= <thf_annotated> | <tff_annotated> | <fof_annotated> |
<cnf_annotated>
%----Future languages may include ... english | efof | tfof | mathml | ...
<thf_annotated> ::= thf(<name>,<formula_role>,<thf_formula><annotations>).
<tff_annotated> ::= tff(<name>,<formula_role>,<tff_formula><annotations>).
<fof_annotated> ::= fof(<name>,<formula_role>,<fof_formula><annotations>).
<cnf_annotated> ::= cnf(<name>,<formula_role>,<cnf_formula><annotations>).
<annotations> ::= <null> | ,<source><optional_info>
%----In derivations the annotated formulae names must be unique, so that
%----parent references (see <inference_record>) are unambiguous.
%----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> ::= <lower_word>
<formula_role> :== axiom | hypothesis | definition | assumption |
lemma | theorem | conjecture | negated_conjecture |
plain | fi_domain | fi_functors | fi_predicates |
type | unknown
%----"axiom"s are accepted, without proof, as a basis for proving "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.
%----See <thf_definition> for details of thf usage.
%----"assumption"s can be used like axioms, but must be discharged before a
%----derivation is complete.
%----"lemma"s and "theorem"s have been proven from the "axiom"s. They can be
%----used like "axiom"s in problems, and a problem containing a non-redundant
%----"lemma" or theorem" is ill-formed. They can also appear in derications.
%----"theorem"s are more important than "lemma"s from the user perspective.
%----"conjecture"s occur in only FOF problems, and all are to be proven from
%----the "axiom"(-like) formulae. A problem is solved only when all
%----"conjecture"s are proven.
%----"negated_conjecture"s occur 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.
%----"fi_domain", "fi_functors", and "fi_predicates" are used to record the
%----domain, interpretation of functors, and interpretation of predicates, for
%----a finite interpretation.
%----"type" defines the type globally for one symbol; treat as $true.
%----"unknown"s have unknown role, and this is an error situation.
%----Top of Page---------------------------------------------------------------
%----THF formulae. All formulae must be closed.
<thf_formula> ::= <thf_logic_formula> | <thf_typed_const> |
<thf_defined_const>
<thf_logic_formula> ::= <thf_binary_formula> | <thf_unitary_formula>
<thf_binary_formula> ::= <thf_pair_binary> | <thf_tuple_binary>
%----Only some binary connectives can be written without ()s.
%----There's no precedence among binary connectives
<thf_pair_binary> ::= <thf_unitary_formula> <thf_pair_connective>
<thf_unitary_formula>
%----Associative connectives & and | are in <assoc_formula>.
<thf_tuple_binary> ::= <thf_or_formula> | <thf_and_formula> |
<thf_apply_formula>
<thf_or_formula> ::= <thf_unitary_formula> <vline> <thf_unitary_formula> |
<thf_or_formula> <vline> <thf_unitary_formula>
<thf_and_formula> ::= <thf_unitary_formula> & <thf_unitary_formula> |
<thf_and_formula> & <thf_unitary_formula>
<thf_apply_formula> ::= <thf_unitary_formula> @ <thf_unitary_formula> |
<thf_apply_formula> @ <thf_unitary_formula>
%----<thf_unitary_formula> are in ()s or do not have a <binary_connective>
%----at the top level. Essentially, a <thf_unitary_formula> is any
%----lambda expression that "has enough parentheses" to be used inside
%----a larger lambda expression. However, lambda notation might not be used.
<thf_unitary_formula> ::= <thf_quantified_formula> | <thf_abstraction> |
<thf_unary_formula> | <thf_atom> | <thf_tuple> |
<thf_letrec> | (<thf_logic_formula>)
<thf_quantified_formula> ::= <thf_quantified_var> | <thf_quantified_novar>
<thf_quantified_var> ::= <quantifier> [<thf_variable_list>] :
<thf_unitary_formula>
<thf_quantified_novar> ::= <thf_quantifier> (<thf_unitary_formula>)
%----@ (denoting apply) is left-associative and lambda is right-associative.
%----^ [X] : ^ [Y] : f @ g (where f is a <thf_apply_formula> and g is a
%----<thf_unitary_formula>) should be parsed as: (^ [X] : (^ [Y] : f)) @ g.
%----That is, g is not in the scope of either lambda.
<thf_abstraction> ::= <thf_lambda> [<thf_variable_list>] :
<thf_unitary_formula>
<thf_variable_list> ::= <thf_variable> | <thf_variable>,<thf_variable_list>
<thf_variable> ::= <variable> | <thf_typed_variable>
<thf_typed_variable> ::= <variable> : <thf_top_level_type>
%----Unary connectives bind more tightly than binary. The negated formula
%----must be ()ed because a ~ is also a term.
<thf_unary_formula> ::= <thf_unary_connective> (<thf_logic_formula>)
%----An <thf_typed_const> is a global assertion that the atom is in this type.
<thf_typed_const> ::= <constant> : <thf_top_level_type> | (<thf_typed_const>)
%----THF atoms
<thf_atom> ::= <term> | <thf_conn_term>
%----<thf_atom> can also be <defined_type> | <defined_plain_formula> |
%----<system_type> | <system_atomic_formula>, but they are syntactically
%----captured by <term>.
%----thf_tuple is really the "pair" function of lambda calculus, so it
%----should be right-associative. It is also "cons" in Lisp.
%----So "(U, V)" is "syntactic sugar" for "lambda [X]: (X @ U @ V)".
%----Some useful functions to work with tuples might be:
%----"first := ^ [E]: (E @ ^ [F, R]: F)" and
%----"rest := ^ [E]: (E @ ^ [F, R]: R)".
%----Then "(first @ (U, V)) = U" and "(rest @ (U, V)) = V" are valid.
%----<thf_tuple> is not a <binary_formula> because it would confuse Prolog
%----if it appeared at top level without parentheses.
<thf_tuple> ::= (<thf_tuple_list>)
<thf_tuple_list> ::= <thf_unitary_formula>,<thf_unitary_formula> |
<thf_unitary_formula>,<thf_tuple_list>
%----If "name := expr" is the entire formula, it has global scope, i.e., the
%----entire input. In this case the <plain_term> must not be a variable. If
%----"name := expr" is in a :=, e.g., ":= [n1 := e1, n2 := e2, ...] : formula"
%----(where the ni normally appear in the formula, and might appear in the ei,
%----each occurrence of ni should be replaced by ei in the formula, i.e., the
%----formula is the scope of the definition. As a formula a <thf_definition>
%----evaluates to true.
<thf_letrec> ::= := [<thf_letrec_list>] : <thf_unitary_formula>
<thf_letrec_list> ::= <thf_defined_var> |
<thf_defined_var>,<thf_letrec_list>
<thf_defined_var> ::= <variable> := <thf_top_level_type> |
(<thf_defined_var>)
<thf_defined_const> ::= <constant> := <thf_top_level_type> |
(<thf_defined_const>)
%----Note that <thf_top_level_type> includes <thf_unitary_formula>
%----<thf_top_level_type> appears after ":", where a type is being specified
%----for a term or variable. <thf_unitary_type> includes <thf_unitary_formula>,
%----so the syntax allows just about any lambda expression with "enough"
%----parentheses to serve as a type. The expected use of this flexibility is
%----parametric polymorphism in types, expressed with lambda abstraction:
%---- list := ^ [T]: ((T * (list @ T)) + (emptylist @ T))
%---- ! [L : (list @ int)]: $let [sum := ^ [L1]: ...] : <expr in L and sum>.
%----Mapping is right-associative: o > o > o means o > (o > o).
%----Xproduct is left-associative: o * o * o means (o * o) * o.
%----Union is left-associative: o + o + o means (o + o) + o.
<thf_top_level_type> ::= <thf_unitary_formula> | <thf_binary_type>
<thf_unitary_type> ::= <thf_unitary_formula> | (<thf_binary_type>)
<thf_binary_type> ::= <thf_mapping_type> | <thf_xprod_type> |
<thf_union_type> | (<thf_binary_type>)
<thf_mapping_type> ::= <thf_unitary_type> <arrow> <thf_unitary_type> |
<thf_unitary_type> <arrow> <thf_mapping_type>
<thf_xprod_type> ::= <thf_unitary_type> <star> <thf_unitary_type> |
<thf_xprod_type> <star> <thf_unitary_type>
<thf_union_type> ::= <thf_unitary_type> <plus> <thf_unitary_type> |
<thf_union_type> <plus> <thf_unitary_type>
%----Top of Page---------------------------------------------------------------
%----TFF formulae. All formulae must be closed.
%----TFF is like FOF except that predicate and function symbols must be typed
%----exactly once at top level (with formula role "type"), and variables must
%----be typed when they are bound in quantifier lists. atomic_formula>s are
%----just like FOF. See the porposal linked from the TPTP web page for details
%----of the semantics.
<tff_formula> ::= <tff_logic_formula> | <tff_defined_const> |
<tff_typed_atom>
<tff_logic_formula> ::= <tff_binary_formula> | <tff_unitary_formula>
<tff_binary_formula> ::= <tff_nonassoc_binary> | <tff_assoc_binary>
<tff_nonassoc_binary> ::= <tff_unitary_formula> <binary_connective>
<tff_unitary_formula>
<tff_assoc_binary> ::= <tff_or_formula> | <tff_and_formula>
<tff_or_formula> ::= <tff_unitary_formula> <vline> <tff_unitary_formula>
<tff_more_or_formula>*
<tff_more_or_formula> ::= <vline> <tff_unitary_formula>
<tff_and_formula> ::= <tff_unitary_formula> & <tff_unitary_formula>
<tff_more_and_formula>*
<tff_more_and_formula> ::= & <tff_unitary_formula>
<tff_unitary_formula> ::= <tff_quantified_formula> | <tff_unary_formula> |
<atomic_formula> | (<tff_logic_formula>) |
<tff_letrec> | <variable>
%----<variable>s make sense only when they are the <term> of a <tff_letrec>
<tff_quantified_formula> ::= <quantifier> [<tff_variable_list>] :
<tff_unitary_formula>
<tff_variable_list> ::= <tff_variable> | <tff_variable>,<tff_variable_list>
<tff_variable> ::= <variable> : <tff_atomic_type>
<tff_unary_formula> ::= <unary_connective> <tff_unitary_formula>
%----<tff_typed_atom> can appear only at top level, unlike in THF.
<tff_typed_atom> ::= <tff_untyped_atom> : <tff_top_level_type> |
(<tff_typed_atom>)
<tff_untyped_atom> ::= <functor> | <system_functor>
%----The types of the <defined_atom>s and <defined_prop>s are:
%---- <real> : $real
%---- <signed_integer> : $int
%---- <unsigned_integer> : $int
%---- <distinct_object> : $iType
%---- $true : $oType
%---- $false : $oType
%----See <thf_letrec> for commentary
<tff_letrec> ::= := [<tff_letrec_list>] : <tff_unitary_formula>
<tff_letrec_list> ::= <tff_defined_var> |
<tff_defined_var>,<tff_letrec_list>
<tff_defined_var> ::= <variable> := <tff_unitary_formula> |
(<tff_defined_var>)
<tff_defined_const> ::= <constant> := <tff_unitary_formula> |
(<tff_defined_const>)
%----See <thf_top_level_type> for commentary
<tff_top_level_type> ::= <tff_atomic_type> | <tff_mapping_type>
<tff_unitary_type> ::= <tff_atomic_type> | (<tff_xprod_type>)
<tff_atomic_type> ::= <atomic_word> | <defined_type>
%----For consistency with <thf_unitary_formula> (the analogue in thf),
%----<tff_atomic_type> should also allow (<tff_atomic_type>)
%----For Josef Urban, change <atomic_word> to <unitary_formula>, and leave
%----out <defined_type> (to avoid conflict on <atomic_defined_word>. Also,
%----<unitary_formula> can be ()ed, so leave out (<tff_unitary_type>), but
%----that means <tff_xprod_type> doesn't have (()) option.
<tff_mapping_type> ::= <tff_unitary_type> <arrow> <tff_atomic_type> |
(<tff_mapping_type>)
<tff_xprod_type> ::= <tff_atomic_type> <star> <tff_atomic_type> |
<tff_xprod_type> <star> <tff_atomic_type>
%----Top of Page---------------------------------------------------------------
%----FOF formulae. All formulae must be closed.
<fof_formula> ::= <binary_formula> | <unitary_formula>
%----Future answer variable ideas | <answer_formula>
%----Answer variable <answer_formula> ::= ?? <general_list> : <fof_formula>
<binary_formula> ::= <nonassoc_binary> | <assoc_binary>
%----Only some binary connectives are associative
%----There's no precedence among binary connectives
<nonassoc_binary> ::= <unitary_formula> <binary_connective> <unitary_formula>
%----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> |
<atomic_formula> | (<fof_formula>)
<quantified_formula> ::= <quantifier> [<variable_list>] : <unitary_formula>
%----! 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 existential counting
%----Unary connectives bind more tightly than binary
<unary_formula> ::= <unary_connective> <unitary_formula>
%----Top of Page---------------------------------------------------------------
%----CNF formulae (variables implicitly universally quantified)
<cnf_formula> ::= (<disjunction>) | <disjunction>
<disjunction> ::= <literal> <more_disjunction>*
<more_disjunction> ::= <vline> <literal>
<literal> ::= <atomic_formula> | ~ <atomic_formula>
%----Top of Page---------------------------------------------------------------
%----Special higher order terms
<thf_conn_term> ::= <thf_quantifier> | <thf_pair_connective> |
<assoc_connective> | <thf_unary_connective>
%----Connectives - THF
<thf_lambda> ::= ^
<thf_quantifier> ::= !! | ??
%---Pi and Sigma
<thf_pair_connective> ::= = | <binary_connective>
<thf_unary_connective> ::= <unary_connective>
%----Connectives - FOF
<quantifier> ::= ! | ?
<binary_connective> ::= <=> | => | <= | <~> | ~<vline> | ~&
<assoc_connective> ::= <vline> | &
<unary_connective> ::= ~
%----Types for THF and TFF
<defined_type> ::= <atomic_defined_word>
<defined_type> :== $oType | $o | $iType | $i | $tType |
$real | $int |
$vector_int | $vector_real |
$matrix_int | $matrix_real
%----$oType/$o is the Boolean type, i.e., the type of $true and $false.
%----$iType/$i is type of individuals. $tType is the type of all types.
%----$real is the type of <real>s. $int is the type of <signed_integer>s and
%----<unsigned_integer>s.
%----There are no constants for the vector and matrix types.
<system_type> :== <atomic_system_word>
%----First order atoms
<atomic_formula> ::= <plain_atomic_formula> | <defined_atomic_formula> |
<system_atomic_formula>
<plain_atomic_formula> ::= <plain_term>
%----A <plain_atomic_formula> looks like a <plain_term>, but really we mean
%---- <plain_atomic_formula> ::= <proposition> | <predicate>(<arguments>)
%---- <proposition> ::= <predicate>
%---- <predicate> ::= <atomic_word>
%----Using <plain_term> removes a reduce/reduce ambiguity in lex/yacc.
%----Note: "defined" means a word starting with one $ and "system" means $$.
<defined_atomic_formula> ::= <defined_plain_formula> | <defined_infix_formula>
%----Some systems still interpret 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>
<defined_plain_formula> ::= <defined_plain_term>
<defined_plain_formula> :== <defined_prop> | <defined_pred>(<arguments>)
<defined_prop> :== <atomic_defined_word>
<defined_prop> :== $true | $false
%----Pure CNF should not use these in problems, an use $false only as the root
%----of a refutation.
<defined_pred> :== <atomic_defined_word>
<defined_pred> :== $equal | $distinct
%----$distinct is for SMT
<defined_infix_formula> ::= <term> <defined_infix_pred> <term>
<defined_infix_pred> ::= = | !=
%----System terms have system specific interpretations
<system_atomic_formula> ::= <system_term>
%----<system_atomic_formula>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.
%----First order terms
<term> ::= <function_term> | <variable>
<function_term> ::= <plain_term> | <defined_term> | <system_term>
<plain_term> ::= <constant> | <functor>(<arguments>)
<constant> ::= <functor>
<functor> ::= <atomic_word>
%----Defined terms have TPTP specific interpretations
<defined_term> ::= <defined_atom> | <defined_atomic_term>
<defined_atom> ::= <number> | <distinct_object>
<defined_atomic_term> ::= <defined_plain_term>
%----None yet | <defined_infix_term>
%----None yet <defined_infix_term> ::= <term> <defined_infix_func> <term>
%----None yet <defined_infix_func> ::=
<defined_plain_term> ::= <defined_constant> | <defined_functor>(<arguments>)
<defined_constant> ::= <defined_functor>
<defined_constant> :==
<defined_functor> ::= <atomic_defined_word>
<defined_functor> :== $vector_int_update | $vector_int_select |
$vector_real_update | $vector_real_select |
$matrix_int_update | $matrix_int_select |
$matrix_real_update | $matrix_real_select
%----System terms have system specific interpretations
<system_term> ::= <system_constant> | <system_functor>(<arguments>)
<system_constant> ::= <system_functor>
<system_functor> ::= <atomic_system_word>
%----Variables, and only variables, start with uppercase
<variable> ::= <upper_word>
%----Arguments recurse back up to terms (this is the FOF world here)
<arguments> ::= <term> | <term>,<arguments>
%----Top of Page---------------------------------------------------------------
%----Formula sources
<source> ::= <general_term>
<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_list>])
<inference_rule> :== <atomic_word>
%----Examples are deduction | modus_tollens | modus_ponens | rewrite |
% resolution | paramodulation | factorization |
% cnf_conversion | cnf_refutation | ...
%----<parent_list> cannot be empty. Formulae introduced without parents must
%----use an <internal_source>
<parent_list> :== <parent_info> | <parent_info>,<parent_ items>
<parent_info> :== <source><parent_details>
<parent_details> :== :<atomic_word> | <null>
<internal_source> :== introduced(<intro_type><optional_info>)
<intro_type> :== definition | axiom_of_choice | tautology | assumption
%----This should be used to record the symbol being defined, or the function
%----for the axiom of choice
<external_source> :== <file_source> | <theory> | <creator_source>
<file_source> :== file(<file_name><file_info>)
<file_info> :== ,<name> | <null>
<theory> :== theory(<theory_name><optional_info>)
<theory_name> :== equality | ac
%----More theory names may be added in the future. The <optional_info> is
%----used to store, e.g., which axioms of equality have been implicitly used,
%----e.g., theory(equality,[rst]). Standard format still to be decided.
<creator_source> :== creator(<creator_name><optional_info>)
<creator_name> :== <atomic_word>
%----Useful info fields
<optional_info> ::= ,<useful_info> | <null>
<useful_info> ::= <general_term_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>)
%----<iquote_item>s are used for recording exactly what the system output about
%----the inference step. In the future it is planned to encode this information
%----in standardized forms as <parent_details> in each <inference_record>.
%----Useful info for inference records
<inference_item> :== <inference_status> | <assumptions_record> |
<refutation>
<inference_status> :== status(<status_value>) | <inference_info>
%----These are the status values from the SZS ontology. The most commonly used
%----status values are:
%---- thm - Every model (and there are some) of the parent formulae is a
%---- model of the inferred formula. Regular logical consequences.
%---- cth - Every model (and there are some) of the parent formulae is a
%---- model of the negation of the inferred formula. Used for negation
%---- of conjectures in FOF to CNF conversion.
%---- sab - There is a bijection between the models (and there are some) of
%---- the parent formulae and models of the inferred formula. Used for
%---- Skolemization steps.
%----For the full hierarchy see the SZSOntology file distributed with the TPTP.
<status_value> :== tau | tac | eqv | thm | sat | cax | noc | csa | cth |
ceq | unc | uns | sab | sam | sar | sap | csp | csr |
csm | csb
%----<inference_info> is used to record standard information associated with an
%----arbitrary inference rule. The <inference_rule> is the same as the
%----<inference_rule> of the <inference_record>. The <atomic_word> indicates
%----the information being recorded in the <general_list>. The <atomic_word>
%----are (loosely) set by TPTP conventions, and include esplit, sr_split, and
%----discharge.
<inference_info> :== <inference_rule>(<atomic_word>,<general_list>)
%----An <assumptions_record> lists the names of assumptions upon which this
%----inferred formula depends. These must be discharged in a completed proof.
<assumptions_record> :== assumptions([<name_list>])
%----A <refutation> record names a file in which the inference recorded here
%----is recorded as a proof by refutation.
<refutation> :== refutation(<file_source>)
%----Useful info for creators and introduced is just <general_function>
%----Include directives
<include> ::= include(<file_name><formula_selection>).
<formula_selection> ::= ,[<name_list>] | <null>
<name_list> ::= <name> | <name>,<name_list>
%----Non-logical data
<general_term> ::= <general_data> | <general_data>:<general_term> |
<general_list>
<general_data> ::= <atomic_word> | <atomic_word>(<general_arguments>) |
<variable> | <number> | <distinct_object> |
(<formula_data>)
<formula_data> ::= <fof_formula>
%----In the future, for other cases, <formula_data> will also have to
%----accept <thf_formula>, etc. It introduced a parsing ambiguity, which
%----can be resolved by having separate <useful_info> rules for each
%----language (or is <thf_formula> strong enough - hey, I think so!).
%----Note that this allows terms because atomic formulae are parsed as terms.
<general_arguments> ::= <general_term> | <general_term>,<general_arguments>
<general_list> ::= [] | [<general_term_list>]
<general_term_list> ::= <general_term> | <general_term>,<general_term_list>
%----General purpose
<name> ::= <atomic_word> | <unsigned_integer>
<atomic_word> ::= <lower_word> | <single_quoted>
<atomic_defined_word> ::= <dollar_word>
<atomic_system_word> ::= <dollar_dollar_word>
<number> ::= <real> | <signed_integer> | <unsigned_integer>
%----Numbers are always interpreted as themselves, and are thus implicitly
%----distinct if they have different values, e.g., 1 != 2 is an implicit axiom.
%----All numbers are base 10 at the moment.
<file_name> ::= <atomic_word>
<null> ::=
%----Top of Page---------------------------------------------------------------
%----Rules from here on down are for defining tokens (terminal symbols) of the
%----grammar, assuming they will be recognized by a lexical scanner.
%----A ::- rule defines a token, a ::: rule defines a macro that is not a
%----token. Usual regexp notation is used. Single characters are always placed
%----in []s to disable any special meanings (for uniformity this is done to
%----all characters, not only those with special meanings).
%----These are tokens that appear in the syntax rules above. No rules
%----defined here because they appear explicitly in the syntax rules,
%----except that <vline>, <star>, <plus> denote "|", "*", "+", respectively.
%----Keywords: fof cnf thf tff include
%----Punctuation: ( ) , . [ ] :
%----Operators: ! ? ~ & | <=> => <= <~> ~| ~& * +
%----Predicates: = != $true $false
%----For lex/yacc there cannot be spaces on either side of the | here
<comment> ::: <comment_line>|<comment_block>
<comment_line> ::: [%]<printable_char>*
<comment_block> ::: [/][*]<not_star_slash>[*][*]*[/]
<not_star_slash> ::: ([^*]*[*][*]*[^/*])*[^*]*
%----Defined comments are a convention used for annotations that are used as
%----additional input for systems. They look like comments, but start with %$
%----or /*$. A wily user of the syntax can notice the $ and extract information
%----from the "comment" and pass that on as input to the system. They are
%----analogous to pragmas in programming languages. To extract these separately
%----from regular comments, the rules are:
%---- <defined_comment> ::- <def_comment_line>|<def_comment_block>
%---- <def_comment_line> ::: [%]<dollar><printable_char>*
%---- <def_comment_block> ::: [/][*]<dollar><not_star_slash>[*][*]*[/]
%----A string that matches both <defined_comment> and <comment> should be
%----recognized as <defined_comment>, so put these before <comment>.
%----Defined comments that are in use include:
%---- TO BE ANNOUNCED
%----System comments are a convention used for annotations that may used as
%----additional input to a specific system. They look like comments, but start
%----with %$$ or /*$$. A wily user of the syntax can notice the $$ and extract
%----information from the "comment" and pass that on as input to the system.
%----The specific system for which the information is intended should be
%----identified after the $$, e.g., /*$$Otter 3.3: Demodulator */
%----To extract these separately from regular comments, the rules are:
%---- <system_comment> ::- <sys_comment_line>|<sys_comment_block>
%---- <sys_comment_line> ::: [%]<dollar><dollar><printable_char>*
%---- <sys_comment_block> ::: [/][*]<dollar><dollar><not_star_slash>[*][*]*[/]
%----A string that matches both <system_comment> and <defined_comment> should
%----be recognized as <system_comment>, so put these before <defined_comment>.
<single_quoted> ::- [']([^\\']|[\\][']|[\\][\\])([^\\']|[\\][']|[\\][\\])*[']
%----<single_quoted> ::- '<printable_char>*', but ' and \ are escaped.
%----\ is used as the escape character for ' and \, i.e., if \' is encountered
%----the ' is not the end of the <single_quoted>, and if \\ is encountered the
%----second \ is not an escape. Both characters (the escape \ and the following
%----' or \) are retained and printed on output. Behaviour is undefined if the
%----escape \ is followed by anything other than ' or \. Behaviour is undefined
%----if a non-<printable_char> is encountered. If the contents of a <single
%----quoted> constitute a <lower_word>, then the ''s should be stripped to
%----produce a <lower_word>.
<distinct_object> ::- ["]([^\\"]|[\\]["]|[\\][\\])([^\\"]|[\\]["]|[\\][\\])*["]
%----<distinct_object> ::- "<viewable_char>*", but " and \ are escaped. The
%----comments for <single_quoted> apply, with ' replaced by ".
%----Distinct objects are always interpreted as themselves, and are thus
%----implicitly distinct if they look different, e.g., "Apple" != "Microsoft"
%----is an implicit axiom.
<dollar_word> ::- <dollar><lower_word>
<dollar_dollar_word> ::- <dollar><dollar><lower_word>
<upper_word> ::- <upper_alpha><alpha_numeric>*
<lower_word> ::- <lower_alpha><alpha_numeric>*
<vline> ::- [|]
<star> ::- [*]
<plus> ::- [+]
<arrow> ::- [>]
%----Numbers
<real> ::- (<decimal_fraction>|<decimal_exponent>)
<signed_integer> ::- <sign><unsigned_integer>
<unsigned_integer> ::- <decimal_natural>
%----<signed_integer>s and <unsigned_integer>s have to be different tokens
%----because <unsigned_integer>s are allowed as annotated formula names.
<decimal_exponent> ::: (<decimal>|<decimal_fraction>)<exponent><decimal>
<decimal_fraction> ::: <decimal><dot_decimal>
<decimal> ::: (<signed_decimal>|<decimal_natural>)
<signed_decimal> ::: <sign><decimal_natural>
<decimal_natural> ::: ([0]|<non_zero_numeric><numeric>*)
<dot_decimal> ::: [.]<numeric><numeric>*
<sign> ::: [+-]
<exponent> ::: [Ee]
%----Character classes
<numeric> ::: [0-9]
<non_zero_numeric> ::: [1-9]
<lower_alpha> ::: [a-z]
<upper_alpha> ::: [A-Z]
<alpha_numeric> ::: (<lower_alpha>|<upper_alpha>|<numeric>|[_])
<dollar> ::: [$]
<printable_char> ::: .
%----<printable_char> is any printable ASCII character, codes 32 (space) to 126
%----(tilde). printable_char> does not include tabs, newlines, bells, etc. The
%----use of . does not not exclude tab, so this is a bit loose.
<viewable_char> ::: [.\n]
%----Top of Page---------------------------------------------------------------