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
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
|
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN">
<html>
<head>
<title>Prover9 Manual: Inference Rules</title>
<link rel="stylesheet" href="manual.css">
</head>
<body>
<hr>
<table width="100%">
<tr>
<colgroup>
<col width="33%">
<col width="34%">
<col width="33%">
</colgroup>
<td align="left"><i>Prover9 Manual</i>
<td align="center"><img src="prover9-5a-256t.gif">
<td align="right"><i>Version 2008-05A</i>
</table>
<hr>
<!-- Main content -->
<h1>Inference Rules</h1>
When a given clause is selected, all of the enabled inference rules
are applied to it. For each inference, one of
the parents is the given clause, and all other parents
must be in the <tt>usable</tt> list.
<p>
Most inference rules distinguish the parents by the roles
they play in the inference, e.g., positive or negative literal for
binary resolution, nucleus or satellite for hyper rules,
and from and into for paramodulation. The given clause can
play any role in the inference.
<p>
After an inference rule generates a new clause,
the clause is <a href="process-inf.html">processed</a>,
which includes simplification operations such
as demodulation and <a href="process-inf.html#unit_deletion"><tt><b>unit_deletion</b></tt></a>,
and retention tests, such as <a href="process-inf.html#max_weight"><tt><b>max_weight</b></tt></a>.
Processing also includes several operations
that might be considered inference rules, such as
<a href="process-inf.html#factor"><tt><b>factor</b></tt></a> and
<a href="process-inf.html#new_constants"><tt><b>new_constants</b></tt></a>.
<p>
Prover9 uses ordered resolution and paramodulation with
literal selection. These methods restrict the literals that
are eligible for inference.
The resolution and paramodulation inference rules are
intended to be
<g>complete<g>
(exceptions are given in the descriptions
of the options below), but we have not done a rigorous
analysis of the algorithms, so users should not make any
assumptions about completeness.
For an overview of ordered inference with literal selection,
see the section
<a href="inf-rules.html#ordered_inference">Ordered Inference</a> below.
<h2>Binary Resolution Rules and Options</h2>
<!-- start option binary_resolution -->
<a name="binary_resolution">
<pre class="my_option">
set(binary_resolution).
clear(binary_resolution). % default clear
</pre>
<blockquote>
If this flag is set,
<a href="glossary.html#Binary Resolution">binary resolution</a>
will be applied to the given clause.
The options
<a href="inf-rules.html#literal_selection"><tt><b>literal_selection</b></tt></a>,
<a href="inf-rules.html#ordered_res"><tt><b>ordered_res</b></tt></a>, and
<a href="inf-rules.html#check_res_instances"><tt><b>check_res_instances</b></tt></a>
determine eligible literals.
</blockquote>
<!-- end option -->
<!-- start option neg_binary_resolution -->
<a name="neg_binary_resolution">
<pre class="my_option">
set(neg_binary_resolution).
clear(neg_binary_resolution). % default clear
</pre>
<blockquote>
If this flag is set, <a href="glossary.html#Binary Resolution">negative binary resolution</a> is
applied to the given clause. That is, the negative resolved literal must be in
a clause in which all literals are negative.
The options
<a href="inf-rules.html#ordered_res"><tt><b>ordered_res</b></tt></a>, and
<a href="inf-rules.html#check_res_instances"><tt><b>check_res_instances</b></tt></a>
are also used to determine eligible literals.
<p>
Note that there is no inference rule "pos_binary_resolution".
Positive binary resolution can be achieved by using the parameter
<a href="inf-rules.html#literal_selection"><tt><b>literal_selection</b></tt></a>
so that at least one negative literal is always selected.
Positive binary resolution is not the dual of
<a href="inf-rules.html#neg_binary_resolution"><tt><b>neg_binary_resolution</b></tt></a>,
because the
<a href="inf-rules.html#literal_selection"><tt><b>literal_selection</b></tt></a>
technique is not symmetric between positive and negative literals;
in particular, selected literals are always negative.
The <a href="inf-rules.html#literal_selection"><tt><b>literal_selection</b></tt></a>
parameter is always ignored for negative binary resolution.
</blockquote>
<!-- end option -->
<!-- start option ordered_res -->
<a name="ordered_res">
<pre class="my_option">
set(ordered_res). % default set
clear(ordered_res).
</pre>
<blockquote>
This option puts restrictions on the binary and hyperresolution
inference rules (but not on UR-resolution).
It says that resolved literals in one or more of the parents must be
<a href="glossary.html#maximal">maximal</a> in the clause.
<p>
See the section <a href="inf-rules.html#ordered_inference">Ordered Inference</a> below.
</blockquote>
<!-- end option -->
<!-- start option check_res_instances -->
<a name="check_res_instances">
<pre class="my_option">
set(check_res_instances).
clear(check_res_instances). % default clear
</pre>
<blockquote>
This flag applies to the binary and hyperresolution inference rules
if the flag <a href="inf-rules.html#ordered_res"><tt><b>ordered_res</b></tt></a> is also set. If
<a href="inf-rules.html#check_res_instances"><tt><b>check_res_instances</b></tt></a> is set,
the <a href="inf-rules.html#ordered_res"><tt><b>ordered_res</b></tt></a> test is is applied after the
substitution for the inference has been applied to the parents.
</blockquote>
<!-- end option -->
<!-- start option literal_selection -->
<a name="literal_selection">
<pre class="my_option">
assign(literal_selection, <i>string</i>). % default <i>string</i>=max_negative, range [max_negative, all_negative, none]
</pre>
<blockquote>
This parameter affects to the inference rules
<a href="inf-rules.html#binary_res"><tt><b>binary_res</b></tt></a> and
<a href="inf-rules.html#paramodulation"><tt><b>paramodulation</b></tt></a>.
It determines which literals are eligible for inference.
Here are the accepted values.
<ul>
<li><tt>max_negative</tt>: negative literals that are maximal w.r.t.
the negative literals of the clause are marked;
<li><tt>all_negative</tt>: all negative literals are marked;
<li><tt>none</tt>: no literals are marked;
</ul>
If at least one negative literal is always selected (e.g.,
<tt>max_negative</tt> or <tt>all_negative</tt>),
binary resolution will be
<a href="glossary.html#Binary Resolution">positive binary resolution</a>,
and paramodulation will be
<a href="glossary.html#positive-paramodulation">positive paramodulation</a>.
<p>
Literal selection is ordinarily used with
<a href="#ordered_inference">ordered inference</a>
(flags <a href="inf-rules.html#ordered_res"><tt><b>ordered_res</b></tt></a> and
<a href="inf-rules.html#ordered_para"><tt><b>ordered_para</b></tt></a>),
but it can be used without ordered inference.
</blockquote>
<!-- end option -->
<h2>Hyper and UR Resolution Rules and Options</h2>
The Hyper and UR resultion rules can resolve more than one literal
of one of the parent clauses (the <a href="glossary.html#hyperresolution">nucleus</a>) with other
parent clauses (the <g>satellites</g>), all in one step. An
application of one of these inference rules can be viewed as
a sequence of binary resolution steps.
<!-- start option pos_hyper_resolution -->
<a name="pos_hyper_resolution">
<pre class="my_option">
set(pos_hyper_resolution).
clear(pos_hyper_resolution). % default clear
</pre>
<blockquote>
If this flag is set, positive
<a href="glossary.html#">hyperresolution</a>
(usually called simply hyperresolution) is applied to the given clause.
If the flag <a href="inf-rules.html#ordered_res"><tt><b>ordered_res</b></tt></a> is set, the
resolved literals in the satellites (positive parents) must be
</g>maximal</g>.
If the flags
<a href="inf-rules.html#ordered_res"><tt><b>ordered_res</b></tt></a> and
<a href="inf-rules.html#check_res_instances"><tt><b>check_res_instances</b></tt></a>
are both set, the maximality check is done after the substitution
for the inference has been applied to the parents.
Literal selection is not applied to hyperresolution.
</blockquote>
<!-- end option -->
<!-- start option hyper_resolution -->
<a name="hyper_resolution">
<pre class="my_option">
set(hyper_resolution).
clear(hyper_resolution). % default clear
</pre>
<blockquote>
This flag is a synonym for
<a href="inf-rules.html#pos_hyper_resolution"><tt><b>pos_hyper_resolution</b></tt></a>.
The only effect of changing this flag is to make the corresponding
change to the flag
<a href="inf-rules.html#pos_hyper_resolution"><tt><b>pos_hyper_resolution</b></tt></a>.
</blockquote>
<!-- end option -->
<!-- start option neg_hyper_resolution -->
<a name="neg_hyper_resolution">
<pre class="my_option">
set(neg_hyper_resolution).
clear(neg_hyper_resolution). % default clear
</pre>
<blockquote>
If this flag is set,
<a href="glossary.html#hyperresolution">negative hyperresolution</a>
is applied to the given clause.
If the flag
<a href="inf-rules.html#ordered_res"><tt><b>ordered_res</b></tt></a>
is set, the resolved literals in the satellites (negative parents)
must be </g>maximal</g>.
If the flags
<a href="inf-rules.html#ordered_res"><tt><b>ordered_res</b></tt></a> and
<a href="inf-rules.html#check_res_instances"><tt><b>check_res_instances</b></tt></a>
are both set, the maximality check is done after the substitution
for the inference has been applied to the parents.
Literal selection is not applied to hyperresolution.
</blockquote>
<!-- end option -->
<!-- start option ur_resolution -->
<a name="ur_resolution">
<pre class="my_option">
set(ur_resolution).
clear(ur_resolution). % default clear
</pre>
<blockquote>
If this flag is set, <a href="glossary.html#">UR resolution</a> (unit-resulting
resolution) is applied to the given clause. In fact, the
only effect of this flag is that it automatically sets
the flags <a href="inf-rules.html#pos_ur_resolution"><tt><b>pos_ur_resolution</b></tt></a> and
<a href="inf-rules.html#neg_ur_resolution"><tt><b>neg_ur_resolution</b></tt></a>
<p>
UR resolution may be
<g>incomplete</g> when there are
<a href="glossary.html#horn">non-Horn</a> clauses.
</blockquote>
<!-- end option -->
<!-- start option pos_ur_resolution -->
<a name="pos_ur_resolution">
<pre class="my_option">
set(pos_ur_resolution).
clear(pos_ur_resolution). % default clear
</pre>
<blockquote>
If this flag is set, positive <a href="glossary.html#">UR resolution</a> is applied
to the given clause. That is, the resulting unit clause is
a positive clause.
Neither ordering constraints nor literal selection
is applied to UR resolution.
</blockquote>
<!-- end option -->
<!-- start option neg_ur_resolution -->
<a name="neg_ur_resolution">
<pre class="my_option">
set(neg_ur_resolution).
clear(neg_ur_resolution). % default clear
</pre>
<blockquote>
If this flag is set, negative <a href="glossary.html#">UR resolution</a> is applied
to the given clause. That is, the resulting unit clause is
a negative clause.
Neither ordering constraints nor literal selection
is applied to UR resolution.
</blockquote>
<!-- end option -->
<!-- start option initial_nuclei -->
<a name="initial_nuclei">
<pre class="my_option">
set(initial_nuclei).
clear(initial_nuclei). % default clear
</pre>
<blockquote>
This flag puts a restriction on the <a href="glossary.html#">nucleus</a> for the
hyperresolution and UR-resolution inference rules. It says
that each nucleus must be an input clause (more precisely,
an <a href="glossary.html#">initial clause</a>).
<p>
Setting this flag may cause
<g>incompleteness</g>
of the inference system.
</blockquote>
<!-- end option -->
<!-- start option nucleus_limit -->
<a name="nucleus_limit">
<pre class="my_option">
assign(ur_nucleus_limit, <i>n</i>). % default <i>n</i>=-1, range [-1 .. <tt>INT_MAX</tt>]
</pre>
<blockquote>
If <i>n</i> != -1, then the <a href="glossary.html#">nucleus</a> for each UR-resolution
inference can have at most <i>n</i> literals.
<p>
This option may cause
<g>incompleteness</g>
of the inference system.
</blockquote>
<!-- end option -->
<h2>Paramodulation Rules and Options</h2>
<!-- start option paramodulation -->
<a name="paramodulation">
<pre class="my_option">
set(paramodulation).
clear(paramodulation). % default clear
</pre>
<blockquote>
If this flag is set, paramodulation is applied to the given clause.
If the
<a href="glossary.html#from-into">from literal</a>
is oriented (oriented equalities are always <i>heavy=light</i>),
the paramodulation is applied left-to-right. If the
<a href="glossary.html#from-into">from literal</a>
cannot be oriented Prover9 attempts
to paramodulate from both sides of it.
Unlike the inference rule <a href="glossary.html#">superposition</a>,
this inference rule goes into "light" sides of equations.
<p>
If the flag <a href="inf-rules.html#ordered_para"><tt><b>ordered_para</b></tt></a> is also set,
ordered paramodulation is used.
<p>
If paramodulation involves non-unit clauses,
<a href="inf-rules.html#literal_selection"><tt><b>literal_selection</b></tt></a>
is used to determine eligible literals.
<p>
Note that the flag
<a href="process-inf.html#back_demod"><tt><b>back_demod</b></tt></a>
set set by default, so that derived equations can be used to
rewrite older clauses.
</blockquote>
<!-- end option -->
<!-- start option ordered_para -->
<a name="ordered_para">
<pre class="my_option">
set(ordered_para). % default set
clear(ordered_para).
</pre>
<blockquote>
This flag places a restrictions on the
<a href="inf-rules.html#paramodulation"><tt><b>paramodulation</b></tt></a>
inference rule, based on
<a href="glossary.html#maximal">maximal</a> literals.
See the section
<a href="inf-rules.html#ordered_inference">Ordered Inference</a>.
</blockquote>
<!-- end option -->
<!-- start option check_para_instances -->
<a name="check_para_instances">
<pre class="my_option">
set(check_para_instances).
clear(check_para_instances). % default clear
</pre>
<blockquote>
This flag applies to the
<a href="inf-rules.html#paramodulation"><tt><b>paramodulation</b></tt></a>
inference rule and is analogous to the flag
<a href="inf-rules.html#check_res_instances"><tt><b>check_res_instances</b></tt></a> for
<a href="inf-rules.html#binary_resolution"><tt><b>binary_resolution</b></tt></a>.
It says to apply the ordering tests <i>after</i> the substitution for the
inference has been applied to the parent claues.
</blockquote>
<!-- end option -->
<!-- start option para_from_vars -->
<a name="para_from_vars">
<pre class="my_option">
set(para_from_vars). % default set
clear(para_from_vars).
</pre>
<blockquote>
This flag says that paramodulation may occur from variables. That is,
a literal <i>x=t</i>, in which <i>x</i> does not ocur in <i>t</i>,
may be used as the
<a href="glossary.html#from-into">from literal</a>, unifying
arbitrary terms with <i>x</i>, and replacing them with
<i>t</i>.
<p>
For (unit) equational problems, this flag is nearly always irrelevant.
<p>
Clearing this flag may cause
<g>incompleteness</g>
of the inference system.
</blockquote>
<!-- end option -->
<!-- start option para_lit_limit -->
<a name="para_lit_limit">
<pre class="my_option">
assign(para_lit_limit, <i>n</i>). % default <i>n</i>=-1, range [-1 .. <tt>INT_MAX</tt>]
</pre>
<blockquote>
If <i>n</i> ≠ -1, each parent in paramodulation can have at most
<i>n</i> literals.
This option may cause
<g>incompleteness</g>
of the inference system.
</blockquote>
<!-- end option -->
<!-- start option para_units_only -->
<a name="para_units_only">
<pre class="my_option">
set(para_units_only).
clear(para_units_only). % default clear
</pre>
<blockquote>
This flag says that both parents for paramodulation must be
unit clauses. The only effect of this flag is to assign 1 to
the parameter <a href="inf-rules.html#para_lit_limit"><tt><b>para_lit_limit</b></tt></a>.
<p>
Setting this flag may cause
<g>incompleteness</g>
of the inference system.
</blockquote>
<!-- end option -->
<!-- start option basic_paramodulation -->
<a name="basic_paramodulation">
<pre class="my_option">
set(basic_paramodulation).
clear(basic_paramodulation). % default clear
</pre>
<blockquote>
This option hasn't been implemented yet.
</blockquote>
<!-- end option -->
<a name="ordered_inference">
<h2>Ordered Inference</h2>
This section contains a practical overview of ordered inference
as implemented in Prover9.
For theoretical presentations, see
[<a href="references.html#Bachmair-Ganzinger-res">Bachmair-Ganzinger-res</a>]
and
[<a href="references.html#Nieuwenhuis-Rubio-para">Nieuwenhuis-Rubio-para</a>].
<p>
Prover9 uses ordered inference with literal selection.
<ul>
<li> <i>Ordered inference.</i>Within a clause, there is a partial
order on literals, determined by the
<a href="term-order.html">term ordering</a>.
A subset of the literals is marked as <i>maximal</i>.
(If the clause is ground, the order is total, and the greatest
literal is marked as maximal.) The inference rules may be
restricted in some cases so that they apply only to maximal literals.
<li> <i>Literal selection.</i> In each clause, a subset of the
<i>negative</i> literals of a clause is marked as <i>selected</i>.
(Different clauses may have the subset chosen by different methods.)
The inference rules may be restricted in some cases so that they
apply only to selected literals.
</ul>
Ordered inference and literal selection are typically used
together, but each can be used without the other, by changing
the options
<a href="inf-rules.html#ordered_res"><tt><b>ordered_res</b></tt></a>
and
<a href="inf-rules.html#literal_selection"><tt><b>literal_selection</b></tt></a>. In the following,
if <a href="inf-rules.html#ordered_res"><tt><b>ordered_res</b></tt></a> is disabled,
simply assume all literals are maximal.
The setting <tt>assign(literal_selection, none)</tt> has the
effect of disabling literal selection.
<h3>Ordered Binary Resolution with Literal Selection</h3>
<pre class="my_code">
A positive literal <i>PL</i> in a clause <i>C</i> is eligible for resolution if
no literal is selected in <i>C</i>, and <i>PL</i> is maximal in <i>C</i>.
A negative literal <i>NL</i> in a clause <i>C</i> is eligible for resolution if
(1) <i>NL</i> is selected in <i>C</i>, or
(2) no literal is selected in <i>C</i>, and <i>NL</i> is maximal in <i>C</i>.
</pre>
Note that if at least one negative literals is selected in every clause,
we have a version of positive binary resolution, because no literal may
be selected in the clause containing the positive resolved literal.
<h3>Ordered Factoring</h3>
Prover9 does not do ordered factoring. Instead, if factoring is enabled
(see flag <a href="process-inf.html#factor"><tt><b>factor</b></tt></a>),
factoring is applied as much as possible to all newly kept clauses.
In theory, factoring can be restricted to maximal literals without
losing completeness, but we believe applying it eagerly is more
practical.
<h3>Ordered Paramodulation with Selection</h3>
For ordered paramodulation with selection, literal eligibility
for the "from" literal is that same as eligibilty of the
positive literal for ordered resolution with selection.
<p>
Literal eligibility for <i>positive</i> "into" literals
is that same as eligibilty of the
positive literal for ordered resolution with selection.
<p>
Literal eligibility for <i>negative</i> "into" literals
is the same as eligibilty of the negative literal for
ordered resolution with selection.
<p>
In other words,
<pre class="my_code">
A positive literal <i>PL</i> in a clause <i>C</i> is eligible for paramodularion
(as the "from" or the "into" parent) if no literal is selected in <i>C</i>,
and <i>PL</i> is maximal in <i>C</i>.
A negative literal <i>NL</i> in a clause <i>C</i> is eligible for paramodulation if
(1) <i>NL</i> is selected in <i>C</i>, or
(2) no literal is selected in <i>C</i>, and <i>NL</i> is maximal in <i>C</i>.
</pre>
<h3>Negative Ordered Binary Resolution</h3>
<pre class="my_code">
A positive literal <i>NL</i> in a clause <i>C</i> is eligible for resolution if
<i>NL</i> is maximal among the positive literals of <i>C</i>.
A negative literal <i>NL</i> in a clause <i>C</i> is eligible for resolution if
<i>C</i> has no positive literals, and <i>NL</i> is maximal in <i>C</i>.
</pre>
Note that negative ordered binary resolution is not the dual
of positive ordered binary resolution, because the negative version
ignores literal selection.
<hr>
Next Section:
<a href="process-inf.html">Process Inferred</a>
</body>
</html>
|