1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
|
%----Version 3.1.0.23 (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.
%----Files. At least something, and at least one <annotated formula> expected
<TPTP file> ::= <TPTP input>+
<TPTP input> ::= <annotated formula> | <include> | <comment>
%----Formula records
<annotated formula> ::= <fof annotated> | <cnf annotated>
%----Future languages may include ... english | efof | tfof | mathml | ...
<fof annotated> ::= fof(<name>,<type>,<fof formula><annotations>).
<cnf annotated> ::= cnf(<name>,<type>,<cnf formula><annotations>).
<annotations> ::= <null> | ,<source> | ,<source>,<useful info>
%----Types for problems.
%----Note: The previous <source type> from ...
%---- <type> ::= <user type>-<source type>
%----... is now gone. Parsers may choose to be tolerant of it for backwards
%----compatibility.
<type> ::= axiom |
%----Axioms are accepted without proof as a basis for proving conjectures and
%----lemma_conjectures. There is no guarentee that the axioms of a problem are
%----consistent.
hypothesis |
%----Hypotheses are assumed to be true for a particular problem. Like axioms.
definition |
%----Definitions used to define symbols. Used like axioms.
lemma |
%----Lemmas have been proved from the axiom formulae. Can be used like axioms,
%----but are redundant wrt the axioms. Used as the type of proved
%----lemma_conjectures in output. A problem containing a lemma that is not
%----redundant wrt the axioms is ill-formed.
theorem |
%----Theorems have been proved from the axiom formulae. Can be used like
%----axioms, but are redundant wrt the axioms. Used as the type of proved
%----conjectures in output. Theorems are more important than lemmas from the
%----user perspective.
conjecture |
%----Conjectures are all to be proved from the axiom(-like) formulae. A problem
%----is solved only when all conjectures are proved.
lemma_conjecture |
%----Lemma conjectures are expected to be provable, and may be useful to prove,
%----while proving conjectures.
negated_conjecture |
%----Negated conjectures are derived from negation of a conjecture. CNF
%----specific.
plain |
%----Plain formulae have no special user semantics. Can be used like axioms.
unknown
%----Unknown formulae have unknown type. This is an error situation.
%----Future user types may include ... knowledge |
%----FOF formulae. All formulae must be closed.
<fof formula> ::= <literal formula> | <binary formula>
<literal formula> ::= <atomic formula> | <unary formula>
<atomic formula> ::= <quantified formula> | <atom> | (<fof formula>)
%----Quantifers have higher precedence than binary connectives.
<quantified formula> ::= <quantifier> <variables> : <literal formula>
%----! is universal quantification and ? is existential
<quantifier> ::= ! | ?
<variables> ::= [<variable><rest of variables>*]
%----Future variables may have sorts and existential counting
<rest of variables> ::= ,<variable>
%----Only some binary connectives are associative, and there's no precedence
<binary formula> ::= <non-assoc binary> | <assoc binary>
<non-assoc binary> ::= <literal formula> <binary connective> <literal formula>
%----Associative connectives & and vline are in <assoc binary>
<binary connective> ::= <=> | => | <= | <~> | ~vline | ~&
<assoc binary> ::= <or formula> | <and formula>
<or formula> ::= <literal formula> vline <literal formula>
<rest or formula>*
<rest or formula> ::= vline <literal formula>
<and formula> ::= <literal formula> & <literal formula>
<rest and formula>*
<rest and formula> ::= & <literal formula>
%----Unary connectives bind more tightly than binary
<unary formula> ::= <unary connective> <literal formula>
<unary connective> ::= ~
%----CNF formulae (variables implicitly universally quantified)
<cnf formula> ::= (<disjunction>) | <disjunction>
<disjunction> ::= <literal> | <literal> vline <disjunction>
<literal> ::= <atom> | ~ <atom>
%----Atoms
<atom> ::= <plain atom> | <defined atom> | <system atom>
<plain atom> ::= <proposition> | <predicate>(<arguments>)
<proposition> ::= <atomic word>
<predicate> ::= <atomic word>
<arguments> ::= <term><rest of args>*
<rest of args> ::= ,<term>
<defined atom> ::= $true | $false |
<term> = <term> | <term> != <term> |
equal(<term>,<term>)
%----More defined atoms may be added in the future
%----Note: <term> != <term> should be parsed as ~ <term> = <term>
<system atom> ::= $$<predicate> | $$<predicate>(<arguments>)
%----Terms
<term> ::= <function term> | <variable>
<function term> ::= <plain term> | <defined term> | <system term>
<plain term> ::= <constant> | <functor>(<arguments>)
<constant> ::= <atomic word>
<functor> ::= <atomic word>
<defined term> ::= <number> | <double quoted>
<system term> ::= $$<functor> | $$<functor>(<arguments>)
<variable> ::= <upper word>
%----Formula sources
<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><rest parent info>*])
<inference rule> ::= <atomic word>
%----Examples are deduction | modus_tollens | modus_ponens | rewrite |
% resolution | paramodulation | factorization |
% cnf_conversion | cnf_refutation | ...
<rest parent info> ::= ,<parent info>
<parent info> ::= <source><parent details>
<theory> ::= theory(<theory name>)
<theory name> ::= equality | ac | ...
<parent details> ::= -<single quoted> | <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> ::= ,<atomic word> | ,<null>
<external source> ::= <file source> | <creator source> | <theory>
<file source> ::= file(<file name>,<file node name>)
<file name> ::= <single quoted>
<file node name> ::= <name> | unknown
<creator source> ::= creator(<creator name><creator info>)
<creator name> ::= <single quoted>
<creator info> ::= ,<useful info> | <null>
%----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(<single quoted>)
<iquote item> ::= iquote(<single quoted>)
%----Useful info for inference records
<inference item> ::= <inference status> | <refutation>
<inference status> ::= status(<status value>) | <inference info>
%----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><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 */
<system comment> ::= %$$<char until eoln>* | /<star>$$<char>*<star>/
%----General purpose
<general term> ::= <general function> | <general list>
<general list> ::= [] | [<general arguments>]
<general function> ::= <constant> | <functor>(<general arguments>)
<general arguments> ::= <general term><rest of gargs>*
<rest of gargs> ::= ,<general term>
%----The following are reserved <name>s: unknown file inference creator
<name> ::= <atomic word> | <unsigned integer>
<atomic word> ::= <lower word> | <single quoted>
<upper word> ::= <A-Z><a-z0-9A-Z_>*
<lower word> ::= <a-z><a-z0-9A-Z_>*
<single quoted> ::= '<char>*'
%----All numbers are implicitly distinct
<number> ::= <integer> | <real>
<integer> ::= <sign><unsigned integer>
<real> ::= <integer><decimal part>
<sign> ::= + | - | <null>
<unsigned integer> ::= <0-9>+
<decimal part> ::= .<0-9>+ | <null>
%----All strings are implicitly distinct
<double quoted> ::= "<char>*"
<char> ::= ... any printable ASCII character
<star> ::= ... a star character
<plus> ::= ... a plus character
<null> ::=
|
