%----v3.2.0.5 (TPTP version.internal development number) %------------------------------------------------------------------------------ %----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 should be readable with %----read/1. %---- %----The syntax of comments is defined by the 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). %------------------------------------------------------------------------------ %----Files. Empty file is OK. ::= * ::= | %----Formula records ::= | | | %----Future languages may include ... english | efof | tfof | mathml | ... ::= fof(,,). ::= cnf(,,). ::= thf(,,). ::= tff(,,). ::= | , %----In derivations the annotated formulae names must be unique, so that %----parent references (see ) are unambiguous. %----Types for problems. %----Note: The previous from ... %---- ::= - %----... is now gone. Parsers may choose to be tolerant of it for backwards %----compatibility. ::= :== axiom | hypothesis | definition | lemma | theorem | conjecture | lemma_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 %----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. %----See for details of thf usage. %----"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 all are to 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 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. %----START FOF --------------------------------------------------------------- %----FOF formulae. All formulae must be closed. ::= | ::= | %----Only some binary connectives are associative %----There's no precedence among binary connectives ::= ::= <=> | => | <= | <~> | ~ | ~& %----Associative connectives & and | are in ::= | ::= * ::= ::= & * ::= & ::= | & %---- are in ()s or do not have a at the %----top level. ::= | | | () ::= [] : ::= ! | ? %----! is universal quantification and ? is existential. Syntactically, the %----quantification is the left operand of :, and the is %----the right operand. Although : is a binary operator syntactically, it is %----not a , and thus a is a %----. %----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)). ::= | , %----Future variables may have sorts and existential counting %----Unary connectives bind more tightly than binary ::= ::= ~ %---- END FOF --------------------------------- %----CNF formulae (variables implicitly universally quantified) ::= () | ::= * ::= ::= | ~ %---- END CNF --------------------------------- %---- START THF --------------------------------------------------------------- %----THF formulae. All formulae must be closed. ::= | | ::= | | | | %----Only some binary connectives are associative %----There's no precedence among binary connectives ::= ::= = %----Associative connectives & and | are in . %----For thf, these are left-associative to simplify the translation to %----their corresponding lambda expressions. %----E.g., (U & W & Y) becomes ^ [U,W,Y]: (U @ W @ $false @ Y @ $false). %----and (U | W | Y) becomes ^ [U,W,Y]: (U @ $true @ W @ $true @ Y). ::= | ::= | ::= & | & %---- are in ()s or do not have a %----at the top level. Essentially, a is any %----lambda expression that "has enough parentheses" to be used inside %----a larger lambda expression. However, lambda notation might not be used. ::= | | | | | ( ) | ( ) | ( ) ::= [] : ::= ! | ? ::= | , %----Unary connectives bind more tightly than binary ::= %----@ (denoting apply) is left-associative and lambda is right-associative. %----lambda [X] : lambda [Y] : f @ g (where f is a %----and g is a ) should be parsed as: %----(lambda [X] : (lambda [Y] : f)) @ g. %----That is, g is not in the scope of either lambda. ::= [] : ::= lambda | ^ ::= @ | @ %----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 := lambda [E]: (E @ lambda [F, R]: F)" and %----"rest := lambda [E]: (E @ lambda [F, R]: R)". %----Then "(first @ (U, V)) = U" and "(rest @ (U, V)) = V" are valid. %----thf_tuple is not a because it would confuse Prolog %----if it appeared at top level without parentheses. ::= , | , ::= | ::= | ::= | ::= | ::= : ::= %----If the entire formula is a , it should be treated %----as an assertion that the constant is in this type, globally. %----If a appears inside a larger expression, %----it is presently unspecified what the scope of this type declaration is. %----Users producing such formulas should be sure to clarify their intent; %----ad-hoc polymorphism and subtyping are two of several possibilities. %----Note: "defined" means a word starting with one $ and "system" means $$. ::= : ::= | | | | | ( ) ::= | ::= | | | | = %---- appears after ":", where a type is being specified %----for a constant or variable (or other expression, in the future), %----or within a larger . %----However, this is just for "readability", and %----expands simply to , so the syntax allows %----just about any lambda expression with "enough" parentheses to serve %----as a type. HOWEVER, 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)]: letrec [sum := ^ [L1]: ...] : . %----If a that "looks like" a type appears in the %----"function position" of an apply formula, it is %----considered to be a function into bool that is true exactly when its %----parameter is of the type denoted by the . %----E.g., ((nat -> nat) @ fibonacci) might evaluate to $true. %---- is right-associative: o->o->o means o->(o->o). %---- is left-associative: o * o * o means (o * o) * o. %---- is left-associative: o + o + o means (o + o) + o. %----We cannot use for union because of conflict with "or formula". ::= | | ::= | ::= | ::= | ::= ::= -> | > %---- and . %----As a formula, a evaluates to true. %----If "name := expr" is the entire formula, it has global scope, i.e., the %----entire input (to be consistent with the principle that the order of %----formulas within the input is immaterial). %----The symbol := is considered punctuation, so parentheses are not required %----(colon (:) also is considered punctuation). %----Primary expected use is as a , such as %----"letrec [name1 := expr1, name2 := expr2, ...] : formula", %----where the symbols "name1", "name2", ... normally appear in "formula", %----and might appear in "expr1", "expr2", ... . %----In ML, this would be "let rec name = expr in formula" or %----"let name = expr in formula". (thf has only one syntax for both cases.) %----It is expected that each occurrence of "name_i" should be replaced %----by "expr_i" within "formula", BUT NOT ELSEWHERE. %----That is, "formula" is the scope of the definition. %----For "cascading" definitions use "letrec [a := b]: letrec [c := d]: e". ::= letrec [] : ::= | , ::= := | ( ) %---- END THF ----------------------------------------------------------------- %---- START TFF --------------------------------- %----TFF formulae. All formulae must be closed. %----TFF is like FOF except that predicate and function symbols may be typed %----at top level (normally with formula role "type"), and variables may be %----typed when they are bound in quantifier lists. %----s are just like FOF. %----The following conventions allow a fof_formula to be treated as %----a tff_formula. %----If a type is not explicitly declared for a predicate, it defaults to %---- ( * * ...) -> . %----If a type is not explicitly declared for a function, it defaults to %---- ( * * ...) -> . %----If a type is not explicitly declared for a variable, it defaults to %---- . ::= | | ::= | %----Only some binary connectives are associative %----There's no precedence among binary connectives ::= %----Associative connectives & and | are in ::= | ::= * ::= ::= & * ::= & %---- are in ()s or do not have a %----at the top level. ::= | | | ( ) | ( ) ::= [] : ::= | , %----Unary connectives bind more tightly than binary ::= %----tff_typed_atom can appear ONLY at top level, unlike thf. ::= : | ( ) %----tff_untyped_atom can be a predicate symbol or a function symbol. %----Unlike thf, tff_untyped_atom cannot be a variable. ::= | | ::= | ::= : ::= %---- can only appear after ":", where a type is being specified %----for a function or predicate or variable. %---- is right-associative: o->o->o means o->(o->o). %---- is left-associative: o * o * o means (o * o) * o. %---- is left-associative: o + o + o means (o + o) + o. %----We cannot use for union because of conflict with "or formula". ::= | | | ( ) ::= ( ) ::= | | ::= | ::= | ::= | ::= | | %---- END TFF --------------------------------- %----Atoms ( is not used currently) ::= | | ::= %----A looks like a , but really we mean %---- ::= | () %---- ::= %---- ::= ::= | , %----Using removes a reduce/reduce ambiguity in lex/yacc. ::= | () | ::= = | != ::= | ::= :== ::= | | %----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: != is equivalent %----to ~ = %----More defined atoms may be added in the future. ::= %----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 s. %----Terms ::= | ::= | | ::= | () ::= ::= ::= | %----A more general formulation, which syntactically admits more defined terms, %----is as follows. Developers may prefer to adopt this. %---- ::= | | %---- | %---- () | %---- %---- ::= %---- :== %---- ::= %---- :== %---- ::= %----System terms have system specific interpretations ::= | () ::= ::= ::= %----Formula sources ::= :== | | | unknown %----Only a can be a , i.e., derived formulae can be %----identified by a or an :== | :== inference(,, []) :== %----Examples are deduction | modus_tollens | modus_ponens | rewrite | % resolution | paramodulation | factorization | % cnf_conversion | cnf_refutation | ... :== | , :== :== : | :== introduced() :== definition | axiom_of_choice | tautology %----This should be used to record the symbol being defined, or the function %----for the axiom of choice :== | | :== file() :== , | :== theory() :== equality | ac %----More theory names may be added in the future. The 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() :== %----Useful info fields ::= , | ::= :== [] | [] :== | , :== | | %----Useful info for formula records :== | :== description() :== iquote() %----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 in each . %----Useful info for inference records :== | :== status() | %----These are the status values from the SZS ontology :== tau | tac | eqv | thm | sat | cax | noc | csa | cth | ceq | unc | uns | sab | sam | sar | sap | csp | csr | csm | csb %----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. :== (,) :== refutation() %----Useful info for creators is just %----Include directives ::= include(). ::= ,[] | ::= | , %----Non-logical data ::= | : | ::= | () | | ::= | , ::= [] | [] ::= | , %----General purpose. SOME ARE USED BY thf and tff, as well as fof, cnf! ::= | ::= | ::= ::= ::= | | %----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. ::= ::= %------------------------------------------------------------------------------ %----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 , , denote "|", "*", "+", respectively. %----Keywords: fof cnf thf tff include %----Punctuation: ( ) , . [ ] : %----Operators: ! ? ~ & | <=> => <= <~> ~| ~& * + %----Predicates: = != $true $false %----For lex/yacc there cannot be spaces on eiither side of the | here ::: | ::: [%]* ::: [/][*][*][*]*[/] ::: ([^*]*[*][*]*[^/*])*[^*]* %----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: %---- ::- | %---- ::: [%]* %---- ::: [/][*][*][*]*[/] %----A string that matches both and should be %----recognized as , so put these before regular comments. ::- [']([^\\']|[\\][']|[\\][\\])*['] %---- ::- '*', but ' and \ are escaped. %----\ is used as the escape character for ' and \, i.e., if \' is encountered %----the ' is not the end of the , 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- is encountered. If the contents of a constitute a , then the ''s should be stripped to %----produce a . ::- ["]([^\\"]|[\\]["]|[\\][\\])*["] %---- ::- "*", but " and \ are escaped. The %----comments for 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. ::- [$](oType|o) ::- [$](iType|i) ::- [$](tType|t) ::- [$]true ::- [$]false ::- [$] ::- ::- * ::- * ::- [+] %----Numbers ::- (|) ::- ::- ::: ::: [+-] ::: ([0]|*) ::: [.]* %----Character classes ::: [0-9] ::: [1-9] ::: [a-z] ::: [A-Z] ::: (|||[_]) ::: [$][$] ::: . %---- ::: any printable ASCII character, codes 32-126 %---- thus includes spaces, but not tabs, newlines, bells, etc. %----This definition does not capture that. %----The following macros have no effect and are for documentation only. ::: [|] ::: [*] %------------------------------------------------------------------------------