%----Version 0.6 (HO TPTP version.internal development number) %----DRAFT VERSION FOR EVALUATION OF HOF FEATURES. Not in sync with TPTP. %----Version 3.1.1.13b (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 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. ::= * ::= | | | %----Formula records ::= | %----Future languages may include ... english | efof | tfof | mathml | ... %----Keyword fof means the same as hof, retained for backward compatibility. ::= hof(,,). | fof(,,). ::= cnf(,,). ::= | , | ,, %----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 | 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. %----HOF formulae. All formulae must be closed. ::= | ::= | | | ::= | | %----Only some binary connectives are associative %----There's no precedence amoung 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)). ::= | () %---- is in the context of . %---- is retained for integrity of . ::= | | ::= $true | $false | = | = | != %---- must have @ at top level. %---- can drop down to immediately. %---- cannot climb back up to , or . %----In this context &, |, ~, $true, $false are "macros" for %----boolean functions that could be denoted with lambda terms. %----E.g., & : o->o->o. ::= @ | @ | @ | @ ::= [] : %----@ (denoting apply) is left-associative and lambda is right-associative. %----lambda [X] : lambda [Y] : f @ g (where f and g are s) %----should be parsed as (lambda [X] : (lambda [Y] : f)) @ g. %----Its Beta reduction is lambda [Y] : f[X:=g], a function of Y, %----in accordance with the usual Currying. %----(Notation follows Stansifer; [Benzmuller, Brown 2005] writes [g/X]f.) %----If X occurs in g, it is outside the scope of the lambda [X] shown %----and the Beta reduction needs to be preceded by a rename of the bound X. %----Of course it is safer and clearer not to overwork bound variables. %----Use parenthese to get lambda [X] : (lambda [Y] : f @ g), or %----lambda [X] : (lambda [Y] : (f @ g)). %----lambda might have a symbol in the future. ::= lambda | ^ ::= | , %----Future variables may have sorts and existential counting %---- is untyped or typed variable declaration. ::= | ::= : ::= ( : ) %---- is disjoint from , but some s can be types. %---- is right-associative: o->o->o means o->(o->o). ::= ( ) | ::= | ::= | ( ) ::= | ::= $o | $i | $type ::= -> | > %----Unary connectives bind more tightly than binary ::= ::= ~ %----CNF formulae (variables implicitly universally quantified) ::= () | ::= * ::= ::= | ~ %----Atoms ( is not used currently) ::= | | ::= %----A looks like a , but really we mean %---- ::= | () %---- ::= %---- ::= %----Using removes a reduce/reduce ambiguity in lex/yacc. ::= | , ::= $true | $false | ::= = | != %----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: != 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 ::= | ::= | | ::= | () ::= | () ::= %----s and s are always interpreted as themselves ::= | ::= | () ::= ::= ::= %----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 | ... ::= | , ::= ::= theory() ::= equality | ac %----More theory names may be added in the future. ::= : | ::= 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(,) ::= ::= | unknown ::= creator() ::= ::= , | %----Useful info fields ::= [] | [] ::= | , ::= | | %----Useful info for formula records ::= | ::= description() ::= iquote() %----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 ::= (,) ::= refutation() %----Useful info for creators is just %----Include directives ::= include(). ::= | ,[] ::= | , %----General purpose ::= | ::= [] | [] ::= | () ::= | , %----The following are reserved s: unknown file inference creator ::= | ::= | ::= %----All numbers are implicitly distinct ::= | ::= | %------------------------------------------------------------------------------ %----Rules from here on down are for building tokens in the lexer. %----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 ), but %----it seems likely that people will put them elsewhere and simply %----strip them before tokenising. %----A string that matches both and should be %----recognized as . ::= %* | /*/ ::= $$

* ::=

* ::= '*' %----\ is used as the escape character for ' and \, i.e., \' is a quote and %----\\ is a backslash. For input and output in TPTP syntax the \ is printed. ::= | ::=