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
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
|
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN">
<html>
<head>
<title>Prover9 Manual: Clauses and Formulas</title>
<link rel="stylesheet" href="manual.css">
</head>
<body>
<!-- Site navigation menu -->
<ul class="navbar">
<li><a href="index.html">Introduction</a>
<li><a href="install.html">Installation</a>
<li><a href="running.html">Running Prover9</a>
<li><a href="input.html">Input Files</a>
<li><a href="syntax.html">Clauses & Formulas</a>
<li>Search Prep
<ul class="navbar2">
<li><a href="auto.html">Auto Modes</a>
<li><a href="term-order.html">Term Ordering</a>
<li><a href="more-prep.html">More Prep</a>
<li><a href="limits.html">Search Limits</a>
</ul>
<li>Inference
<ul class="navbar2">
<li><a href="loop.html">The Loop</a>
<li><a href="select.html">Select Given</a>
<li><a href="inf-rules.html">Inference Rules</a>
<li><a href="process-inf.html">Process Inferred</a>
</ul>
<li><a href="output.html">Output Files</a>
<li>More Features
<ul class="navbar2">
<li><a href="weight.html">Weighting</a>
<li><a href="attributes.html">Attributes</a>
<li><a href="actions.html">Actions</a>
<li><a href="fof-reduction.html">FOF Reduction</a>
<li><a href="goals.html">Goals</a>
<li><a href="hints.html">Hints</a>
<li><a href="semantics.html">Semantics</a>
</ul>
<li>Related Programs
<ul class="navbar2">
<li><a href="prooftrans.html">Prooftrans</a>
<li><a href="mace4.html">Mace4</a>
</ul>
<li>Ending
<ul class="navbar2">
<li><a href="options.html">All Options</a>
<li><a href="glossary.html">Glossary</a>
<li><a href="manual-index.html">Index</a>
<li><a href="references.html">References</a>
</ul>
</ul>
<div class="header">Prover9 Manual Version June-2006</div>
<!-- Main content -->
<h1>Clauses and Formulas</h1>
The <a href="glossary.html">Glossary Page</a> contains definitions
of <g>term</g>, <g>atomic formula</g>, <g>literal</g>, <g>clause</g>,
and <g>formula</g> from a logical point of view. This page contains
descriptions of how those kinds of things are parsed and printed,
and we refer to them collectively as <i>objects</i>.
<h2>The Difference Between Clauses and Formulas</h2>
When speaking about <i>formulas</i> in Prover9 input, we mean
a restricted kind of first-order formula in which all variables are
explicitly quantified; that is, <i>closed formulas</i>.
Variables in clauses are not explicitly quantified,
so clauses with variables are not Prover9 formulas.
<p>
The distinction between clauses and formulas is a frequent source
of confusion for Prover9 (and Otter) users. When writing
logical specifications for Prover9, we urge users to be careful,
because clauses go in one kind of list, and formulas go into another.
Here are the important points.
<ul>
<li>
Formulas can have any of the logic connectives, and all variables
are explicitly quantified. Formulas go into lists that
start with <tt>formulas(<font color=#D10000><i>list_name</i></font>)</tt>.
<li>
Clauses are simple disjunctions in which all variables are
implicitly universally quantified.
Clauses go into lists that
start with <tt>clauses(<font color=#D10000><i>list_name</i></font>)</tt>.
<li>
Clauses without variables are also formulas, so they
can go into either kind of list. (An exception: clauses can
have <a href="attributes.html">attributes</a>, and formulas cannot.)
<li>
Because variables in clauses are not explicitly quantified,
a rule is needed for distinguishing variables from constants
in clauses (see <a href="#terms">terms</a> below). No such rule is needed for formulas.
<li>
Prover9's inference rules operate on clauses. If formulas are input,
Prover9 immediately translates them clauses by <g>NNF</g>, <g>Skolemization</g>,
and <g>CNF</g> conversions.
</ul>
<h2>Parsing and Printing Objects</h2>
The <i>prefix standard form</i> of an object with an n-ary symbol, say <tt>f</tt>,
at the root is
<pre class="my_file">
f( <font color="#D10000"><i>argument_1, ..., argument_n</i></font> )
</pre>
Whitespace (spaces, tabs, newline, etc.) is accepted anywhere
except within symbols.
<p>
Prover9 will accept any term, clause, or formula written
prefix standard form. However, clauses, formulas, and
many terms can be written in more convenient ways, for example,
"<tt>a=b | a!=c'</tt>" instead of "<tt>|(=(a,b),-(=(a,'(c))))</tt>".
<p>
Prover9 uses a general mechanism in which binary and unary symbols
can have special parsing properties such as "infix",
"infix-right-associated", "postfix". In addition, each of
those symbols has a precedence so that many parentheses
can be omitted. (The mechanism is similar to those used by
most Prolog systems.)
<p>
Many symbols have built-in parsing properties
(see the <a href="#built_in">table below</a>),
and the user can declare parsing properties for
other symbols with the "op" command.
<p>
Clauses and formulas make extensive use of the built-in
parsing properties for the equality relation and the logic connectives.
Instead of first presenting the general mechanism,
we will present the syntax for clauses and formulas
under the assumption of the built-in parsing properties.
The general mechanism is described below in the
section <a href="#declarations">Infix, Prefix, and Postfix Declarations</a>.
<h3>Symbols</h3>
Symbols include variables, constants, function symbols, predicate symbols,
logic connectives. Symbols do not include parentheses or commas.
<p>
Prover9 recognizes several kinds of symbol.
<ul>
<li>An <i>ordinary symbol</i> is a maximal string made from the
characters a-z, A-Z, 0-9, $, and _.
<li>A <i>special symbol</i> is a maximal string made from
characters in the set
<tt>{+-*/\^<>=`~?@&|!#';}</tt>.
<li>A <i>quoted symbol</i> is any string enclosed in double quotes.
<li>The <i>empty list symbol</i> is <tt>[]</tt>. This is a special case.
</ul>
The reason for separating ordinary and special symbols is so that
objects like <tt>a+b</tt>; that is, <tt>+(a,b)</tt>,
can be written without any whitespace around the <tt>+</tt>.
<p>
Objects (terms, clauses, and formulas) are constructed from
symbols, parentheses, and commas.
<h3>Overloaded Symbols</h3>
In most cases, symbol overloading is not allowed. For example
a symbol cannot be both a function symbol and a predicate symbol,
or both a constant and a binary function symbol. There
are a few exceptions.
<ul>
<li>The logic connectives can also be used as function or
predicate symbols of the same arity. For example,
<tt>-</tt> is typically used as unary arithmetic minus
well as for logical negation.
<li>The symbol <tt>|</tt> is used as a delimiter in the Prolog-style
list notation as well as disjunction in clauses and formulas.
</ul>
<p>
<blockquote class="otter_diff">
Prover9 is much more strict about overloading symbols than Otter is.
</blockquote>
<h3><a name="terms">Terms</h3>
In the context of a clause, a rule is needed for distinguishing
variables from constants, because variables do not have explicit
quantifiers.
The default rule is that a symbol is a variable iff it starts with
(lower case) '<tt>u</tt>' through '<tt>z</tt>'.
(Setting the flag <a href="syntax.html#prolog_style_variables"><tt><b>prolog_style_variables</b></tt></a>
changes the rule so that symbols starting with upper case letters
are variables.)
<p>
As a special case, Prolog-style list notation can be used
to write terms that represent lists.
<table "border" align="center" cellpadding="5">
<tr> <th> Term <th> Internal Representation <th> What it Is
<tr> <td> <tt>[]</tt> <td> <tt>$nil</tt> <td> the empty list
<tr> <td> <tt>[a,b,c]</tt> <td> <tt>$cons(a,$cons(b,$cons(c,$nil)))</tt> <td> list of three objects
<tr> <td> <tt>[a|b]</tt> <td> <tt>$cons(a,b)</tt> <td> first, rest
<tr> <td> <tt>[a,b|c]</tt> <td> <tt>$cons(a,$cons(b,c))</tt> <td> first, second, rest
</table>
Lists are frequently used in Prover9 commands such as the "lex" command,
and they are sometimes also used in clauses and formulas.
<h3>Atomic Formulas</h3>
Equality is a built-in special case.
The binary predicate symbol <tt>=</tt>
is usually written as an infix relation.
The binary symbol <tt>!=</tt> is an abbreviation for "not equal";
that is, the formula <tt>a!=b</tt> stands for </tt>-(a=b)</tt>,
or more precisely, <tt>-(=(a,b))</tt>.
From the semantics point of view,
the binary predicate symbol <tt>=</tt>
is the one and only equality symbol for the inference
rules that use equality.
<h3>Clauses</h3>
The disjunction symbol is <tt>|</tt>, and the negation symbol is <tt>-</tt>.
If the negation symbol follows the disjunction symbol, some whitespace
must separate them; otherwise <tt>|-</tt> would be parsed as one symbol.
The disjunction symbol has higher precedence than the equality symbol,
so equations in clauses do not need parentheses. Every clause ends
with a period.
Examples of clauses with minimum whitespace follow (Prover9 adds some
extra space when printing clauses).
<pre class="my_file">
clauses(sos).
p| -q|r.
a=b|c!=d.
f(x)!=f(y)|x=y.
end_of_list.
</pre>
<h3>Formulas</h3>
<table "border" align="center" cellpadding="5">
<tr><th>Meaning <th> Connective <th> Example
<tr><td>negation <td> <tt>-</tt> <td> <tt>(-p)</tt>
<tr><td>disjunction <td> <tt>|</tt> <td> <tt>(p | q | r)</tt>
<tr><td>conjunction <td> <tt>&</tt> <td> <tt>(p & q & r)</tt>
<tr><td>implication <td> <tt>-></tt> <td> <tt>(p -> q)</tt>
<tr><td>backward implication <td> <tt><-</tt> <td> <tt>(p <- q)</tt>
<tr><td>equivalence <td> <tt><-></tt> <td> <tt>(p <-> q)</tt>
<tr><td>universal quantification <td> <tt>all</tt> <td> <tt>(all x all y p(x,y))</tt>
<tr><td>existential quantification <td> <tt>exists</tt> <td> <tt>(exists x exists y p(x,y))</tt>
</table>
When writing formulas, the <a href="#built_in">built-in parsing declarations</a>
allow many parentheses to be omitted. For example, the following two formulas
are really the same formula.
<pre class="my_file">
formulas(sos).
all x all y (p <-> -q | r & -s) .
(all x (all y (p <-> ((-q) | (r & (-s)))))).
end_of_list.
</pre>
<blockquote class="otter_diff">
For Prover9 formulas, each quantified variable must have its own
quantifier; Otter allows quantifiers to be omitted in a sequence
of quantified variables with the same quantifier. For example,
Otter allows <tt>(all x y z p(x,y,z))</tt>, and Prover9 requires
<tt>(all x all y all z p(x,y,z))</tt>.
</blockquote>
<h2><a name="declarations">Infix, Prefix, and Postfix Declarations</h2>
<p>
Several symbols are understood by Prover9 as having special
parsing properties that determine how terms involving those
symbols can be arranged.
In addition, the user can declare additional symbols to have special
parsing properties.
<h3>Parsing Declarations</h3>
The "op" command is used to declare parse types and precedences.
<pre class="my_file">
op( <font color="#D10000"><i>precedence</i></font>, <font color="#D10000"><i>type</i></font>, <font color="#D10000"><i>symbols(s)</i></font> ). % declare parse type and precedence
</pre>
<ul>
<li>1 ≤ <font color="#D10000"><tt><i>precedence</i></tt></font> ≤ 998.
<li><font color="#D10000"><tt><i>type</i></tt></font> is one of
{ <tt>infix, infix_left, infix_right, prefix, prefix_paren, postfix, postfix_paren, clear</tt> }.
<li><font color="#D10000"><tt><i>symbol(s)</i></tt></font> is either a symbol or a list of symbols.
</ul>
<p>
The following table shows an example of each type of parsing
property (and ignores precedence).
<p>
<table "border" align="center" cellpadding="5">
<tr><th> Type <th> Example <th> Standard Prefix <th> Comment
<tr><td><tt>infix</tt> <td> <tt>a*(b*c) </tt> <td> <tt>*(a,*(b,c))</tt>
<tr><td><tt>infix_left</tt> <td> <tt>a*b*c </tt> <td> <tt>*(*(a,b),c)</tt>
<tr><td><tt>infix_right</tt> <td> <tt>a*b*c </tt> <td> <tt>*(a,*(b,c))</tt>
<tr><td><tt>prefix</tt> <td> <tt>- -p </tt> <td> <tt>-(-(p)) </tt> <td> space required in <tt>- -p</tt>
<tr><td><tt>prefix_paren</tt> <td> <tt>-(-p) </tt> <td> <tt>-(-(p)) </tt>
<tr><td><tt>postfix</tt> <td> <tt>a' ' </tt> <td> <tt>'('(a)) </tt> <td> space required in <tt>a' '</tt>
<tr><td><tt>postfix_paren</tt><td> <tt>(a')' </tt> <td> <tt>'('(a)) </tt>
<tr><td><tt>clear</tt> <td> <tt>*(a,b) </tt> <td> <tt>*(a,b) </tt> <td> takes away parsing properties
</table>
<p>
Higher precedence means closer to the root of the object,
and lower precedence means the the symbol binds more closely.
For example, assume that the following declarations are in effect.
<pre class="my_file">
op(790, infix_right, | ). % disjunction in formulas or clauses
op(780, infix_right, & ). % conjunction in formulas
</pre>
Then the object <tt>a & b | c</tt> is an abbreviation for <tt>(a & b) | c</tt>.
<p>
The built-in parsing declarations are shown in the following box.
The ones with comments have built-in meanings;
the others are for general use as function or predicate symbols.
<a name="built_in">
<pre class="my_file">
op(810, infix_right, # ). % for attaching attributes to clauses
op(800, infix, <-> ). % equivalence in formulas
op(800, infix, -> ). % implication in formulas
op(800, infix, <- ). % backward implication in formulas
op(790, infix_right, | ). % disjunction in formulas or clauses
op(780, infix_right, & ). % conjunction in formulas
op(700, infix, = ). % equal in atomic formulas
op(700, infix, != ). % not equal in atomic formulas
op(700, infix, == ).
op(700, infix, < ).
op(700, infix, <= ).
op(700, infix, > ).
op(700, infix, >= ).
op(500, infix, + ).
op(500, infix, * ).
op(500, infix, @ ).
op(500, infix, / ).
op(500, infix, \ ).
op(500, infix, ^ ).
op(500, infix, v ).
op(400, prefix, - ). % logical negation in formulas or clauses, arithmetic minus in terms
op(300, postfix, ' ).
</pre>
<p>
The built-in parsing declarations can be overridden with ordinary "op" comands.
Be careful, however, when overriding parsing declarations for symbols
with built-in meanings. For example, say you wish to use "#" as an infix function
symbol and give the following the declaration.
<pre class="my_file">
op(500, infix, #).
</pre>
Then clauses with attributes might have be written with more parentheses,
for example, as
<pre class="my_file">
(p(a) | q(a)) # (label(a) # label(b)).
</pre>
<p>
If you wish to use one of the symbols with built-in parsing declarations
as an ordinary prefix symbol, you can undo the declaration by giving
an "op" command with type "clear". The following example clears
the parse types for two symbols.
<pre class="my_file">
op(1, clear, [*,+]). % the precedence is irrelevant for type "clear"
</pre>
<p>
Finally, the following example shows that parsing declarations can
be changed anywhere in the input, with immediate effect. This can be useful
for example, if lists of clauses come from different sources.
<pre class="my_file">
op(400,infix_left,*). % assume left association for following clauses
clauses(sos).
P(a * b * c).
end_of_list.
op(400,infix_right,*). % assume right association for following clauses
clauses(sos).
Q(d * e * f).
end_of_list.
op(400,infix,*). % from here on, include all parentheses (input and output)
</pre>
An excerpt from the output of the preceding example shows how the clauses are
printed after the last "op" command.
<pre class="my_file">
clauses(sos).
1 P((a * b) * c). [input].
2 Q(d * (e * f)). [input].
end_of_list.
</pre>
<h2>Prolog-Style Variables</h2>
<!-- start option prolog_style_variables -->
<a name="prolog_style_variables">
<pre class="my_option">
set(prolog_style_variables).
clear(prolog_style_variables). % default clear
</pre>
<blockquote>
A rule is needed for distinguishing variables from constants in
clauses.
If this flag is clear, variables in clauses start with
(lower case) 'u' through 'z'.
If this flag is set, variables in clauses start with
(upper case) 'A' through 'Z' or '_'.
<p>
No such rule is needed for variables in quantified formulas,
because all variables are explicitly quantified.
<p>
Changing <a href="syntax.html#prolog_style_variables"><tt><b>prolog_style_variables</b></tt></a> after some clauses
have already been read file is allowed, but strongly
discouraged. In such situations, Prover9 can print a clause
<tt>P(A,A)</tt> in which the first <tt>A</tt> is a constant and
the second is a variable. Prover9 will (happily and correctly)
make deductions with clauses like that, but the user will go crazy.
</blockquote>
<!-- end option -->
</body>
</html>
|
