This file is indexed.

/usr/share/doc/prover9-doc/html/process-inf.html is in prover9-doc 0.0.200902a-2.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below.

  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
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN">
<html>
<head>
  <title>Prover9 Manual: Processing Inferred Clauses</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 2009-02A</i>
</table>
<hr>

<!-- Main content -->

<h1>Processing Inferred Clauses</h1>

Processing of inferred clauses is separated into two
stages: (1) simplifying the clause and deciding whether
to keep it, and if it is kept, (2) using the clause to
operate on other clauses.

<h2>Processing Initial Clauses</h2>

Initial clauses in the <tt>sos</tt> list are processed,
for the most part, as if they were derived by some inference
rule.  This process helps to ensure that Prover9's working set
of clauses starts out in a good state, in particular, that
no clause subsumes another, and that all clauses are simplified
according to the working set of demodulators.
Note the following exceptions.

<ul>
<li>
The main exceptions to processing initial clauses is that
the parameters
<a href="process-inf.html#max_literals"><tt><b>max_literals</b></tt></a>,
<a href="process-inf.html#max_vars"><tt><b>max_vars</b></tt></a>,
<a href="process-inf.html#max_weight"><tt><b>max_weight</b></tt></a>, and 
<a href="process-inf.html#max_depth"><tt><b>max_depth</b></tt></a>
are not applied.
<li>
All processing of initial <tt>sos</tt> clauses can be disabled
by clearing the flag
<a href="more-prep.html#process_initial_sos"><tt><b>process_initial_sos</b></tt></a>.
<li>
Clauses in the initial <tt>usable</tt> list are never processed.
<li>
If there is an initial <tt>demodulators</tt> list,
the clauses therein will be checked.
If an equation is orientable but backward,
it will be flipped, and a warning message will be printed.
Otherwise, it must satisfy all of the ordinary constraints
on demodulators.
Having an initial <tt>demodulators</tt> list is useful,
along with clearing the flag
<a href="process-inf.html#back_demod"><tt><b>back_demod</b></tt></a>,
if the user wishes to have a set of demodulators that is fixed throughout
the search.
</ul>

<h2>Algorithm for Processing Clauses</h2>

Processing initial and inferred clauses.

<pre class="my_code">
Start with clause c:
    1.  Simplify c:
        1a.  demodulate
	1b.  orient equalities
	1c.  simplify literals
        1d.  merge identical literals
	1e.  <a href="process-inf.html#unit_deletion"><tt><b>unit_deletion</b></tt></a>
	1f.  <a href="process-inf.html#cac_redundancy"><tt><b>cac_redundancy</b></tt></a>
    2.  <a href="process-inf.html#safe_unit_conflict"><tt><b>safe_unit_conflict</b></tt></a> check
    3.  <a href="process-inf.html#max_literals"><tt><b>max_literals</b></tt></a>, <a href="process-inf.html#max_depth"><tt><b>max_depth</b></tt></a>, <a href="process-inf.html#max_vars"><tt><b>max_vars</b></tt></a>, <a href="process-inf.html#max_weight"><tt><b>max_weight</b></tt></a> checks
    4.  evaluate for <a href="semantics.html">semantic selection</a>
    5.  <a href="limits.html#sos_limit"><tt><b>sos_limit</b></tt></a></a> check
    6.  subsumption check (forward)
    7.  assign an ID and keep the clause
    8.  unsafe unit conflict check
    9.  check if the clause should be a demodulator
    ---- (the following steps are delayed until finished with the given clause) ---
    10. <a href="process-inf.html#factor"><tt><b>factor</b></tt></a> c
    11. apply <a href="process-inf.html#new_constants"><tt><b>new_constants</b></tt></a> to c
    12. apply <a href="process-inf.html#back_subsume"><tt><b>back_subsume</b></tt></a> with c
    13. apply <a href="process-inf.html#back_demod"><tt><b>back_demod</b></tt></a> with c
    14. apply <a href="process-inf.html#back_unit_deletion"><tt><b>back_unit_deletion</b></tt></a> with c
    15. move c to the sos list
</pre>
Restricted denials (see flag
<a href="goals.html#restrict_denials"><tt><b>restrict_denials</b></tt></a>)
are not subject to the
<a href="process-inf.html#max_weight"><tt><b>max_weight</b></tt></a> test.

<h2>Options for Processing Inferred Clauses</h2>

<a name="demod-options"</a>
<h3>Demodulation Options</h3>

Dedmodulation is the process of using equations (demodulators)
to rewrite terms.  If a demodulator is oriented by the
term ordering in effect (KBO, LPO, or RPO),
it is applied unconditionally, heavy-to-light.
If a demodulator is not oriented,
it is applied only if the instance that would be used
is oriented.

<!-- start option lex_order_vars -->
<a name="lex_order_vars">
<pre class="my_option">
set(lex_order_vars).
clear(lex_order_vars).    % default clear
</pre>

<blockquote>
This flag allows an exception to the rule for applying nonorientable
demodulators.   If the flag is set, variables are treated as
constants when comparing terms, with the precedence
<p>
<tt>function_order([x,y,z,u,v,w,v6,v7,v8, ...]).</tt>
<p>
That is, variables are smaller than any other symbols.
<p>
For example, with the (nonorientable) demodulator <tt>x*y = y*x</tt>,
the term <tt>v7*v6</tt> can be rewritten to <tt>v6*v7</tt>.
Setting this flag can easily block proofs, but it can also drastically
reduce the search space and still allow some proofs to be found.
<p>
If you have a difficult problem that involves a commutative,
associative-commutative, or some other permutative operation,
we recommend trying this option.
</blockquote>
<!-- end option -->

<!-- start option demod_step_limit -->
<a name="demod_step_limit">
<pre class="my_option">
assign(demod_step_limit, <i>n</i>).  % default <i>n</i>=1000, range [-1 .. <tt>INT_MAX</tt>]
</pre>

<blockquote>
This parameter limits the number of rewrite steps that are applied
to a clause during demodulation.  If <i>n</i>=-1, there is no limit.
</blockquote>
<!-- end option -->

<!-- start option demod_increase_limit -->
<a name="demod_increase_limit">
<pre class="my_option">
assign(demod_increase_limit, <i>n</i>).  % default <i>n</i>=1000, range [-1 .. <tt>INT_MAX</tt>]
</pre>

<blockquote>
This parameter limits the amount (measured as symbol count) that
demodulation can increase the size of a clause.
If <i>n</i>=-1, there is no limit.
</blockquote>
<!-- end option -->

<!-- start option back_demod -->
<a name="back_demod">
<pre class="my_option">
set(back_demod).      % default set
clear(back_demod).
</pre>

<blockquote>
If this flag is set,
<a href="glossary.html#demodulation">back demodulation</a> is applied.
If an orientable equation is derived, it is
appended to the <tt>demodulators</tt> list.
Non-orientable equations are appended based
on the settings of the flags
<a href="process-inf.html#lex_dep_demod"><tt><b>lex_dep_demod</b></tt></a> and
<a href="process-inf.html#lex_dep_demod_sane"><tt><b>lex_dep_demod_sane</b></tt></a>
and the parameter
<a href="process-inf.html#lex_dep_demod_lim"><tt><b>lex_dep_demod_lim</b></tt></a>.

<p>
If an equation is added to <tt>demodulators</tt>,
Then each clause in <tt>usable</tt> or <tt>sos</tt>
that can be rewritten with the equation is copied
and deleted, then the copy is treated as if it were
generated by an inference rule.  In particular,
it will be processed, including demodulation, which
will apply the new demodulator.

</blockquote>
<!-- end option -->

<!-- start option lex_dep_demod -->
<a name="lex_dep_demod">
<pre class="my_option">
set(lex_dep_demod).    % default set
clear(lex_dep_demod).
</pre>

<blockquote>
If this flag is set, then non-orientable equations can
become demodulators (via the flag <a href="process-inf.html#back_demod"><tt><b>back_demod</b></tt></a>).
</blockquote>
<!-- end option -->

<!-- start option lex_dep_demod_lim -->
<a name="lex_dep_demod_lim">
<pre class="my_option">
assign(lex_dep_demod_lim, <i>n</i>).  % default <i>n</i>=11, range [-1 .. <tt>INT_MAX</tt>]
</pre>

<blockquote>
This parameter is a limit on the flag <a href="process-inf.html#lex_dep_demod"><tt><b>lex_dep_demod</b></tt></a>.
A non-orientable equation cannot become a demodulator
if it has more than <i>n</i> symbols.  (The equation <tt>(x*y)*z=x*(y*z)</tt> has 11 symbols.)
If <i>n</i> = -1, there is no limit.
</blockquote>
<!-- end option -->

<!-- start option lex_dep_demod_sane -->
<a name="lex_dep_demod_sane">
<pre class="my_option">
set(lex_dep_demod_sane).    % default set
clear(lex_dep_demod_sane).
</pre>

<blockquote>
This flag is a restriction on the flag <a href="process-inf.html#lex_dep_demod"><tt><b>lex_dep_demod</b></tt></a>.
If set, a non-orientable equation can become a demodulator
only if its two sides have the same number of symbols.
</blockquote>
<!-- end option -->

<!-- start option unit_deletion -->
<a name="unit_deletion">
<pre class="my_option">
set(unit_deletion).
clear(unit_deletion).    % default clear
</pre>

<blockquote>
This flag extends demodulation to include rewriting
of literals with unit clauses.  For example, if
we have the unit clause <tt>p(x,a)</tt>, then
we can use it to remove instances of <tt>-p(x,a)</tt>
from generated clauses.  This process is like using
the unit clause as the demodulator <tt>p(x,a) = TRUE</tt>.
(Unit deletion is not actually implemented as demodulation.)

This flag also causes <i>back unit deletion</i> to occur,
that is, new unit clauses are used to remove literals
from older clauses.
</blockquote>
<!-- end option -->

<!-- end option -->

<h3>Simplifying and Deciding Whether to Keep Clauses</h3>

The options in this section appear in the order in which they are applied.

<!-- start option cac_redundancy -->
<a name="cac_redundancy">
<pre class="my_option">
set(cac_redundancy).    % default set
clear(cac_redundancy).
</pre>

<blockquote>
If this flag is set, then an equational redundancy criterion is applied.
If Prover9 finds that a binary operation is commutative or
associative-commutative, it makes a note and uses that information to simplify
clauses that are derived later in the search.
<p>
If a derived clause contains an equality <i>alpha=beta</i>,
in which <i>alpha</i> and <i>beta</i> are equal with respect to
commutativity or associativity-commutativity of the previously
noted operations, the equality is simplified to <tt>TRUE</tt>.
<p>
For example, if Prover9 notes that <tt>x*y=y*x</tt>, and then some
time later a clause containing the literal <tt>g(u*v)=g(v*u)</tt> is
derived, that literal will be simplified to TRUE and the clause
will be deleted.  (Demodulation will not rewrite the two sides
to the same term unless the flag <a href="process-inf.html#lex_dep_demod"><tt><b>lex_dep_demod</b></tt></a> is set.)
</blockquote>
<!-- end option -->

<!-- start option max_literals -->
<a name="max_literals">
<pre class="my_option">
assign(max_literals, <i>n</i>).  % default <i>n</i>=-1, range [-1 .. <tt>INT_MAX</tt>]
</pre>

<blockquote>
Clauses containing more than <i>n</i> literals will be deleted.
If <n> = -1, there is no limit.
This parameter is never applied to <a href="glossary.html#">initial clause</a>s
or to clauses that <a href="hints.html">match hints</a>.
</blockquote>
<!-- end option -->

<!-- start option max_literals -->
<a name="max_depth">
<pre class="my_option">
assign(max_depth, <i>n</i>).  % default <i>n</i>=-1, range [-1 .. <tt>INT_MAX</tt>]
</pre>

<blockquote>
If the <a href="glossary.html#depth-C">depth of the clause</a> is more than <i>n</i>, it will be deleted.
If <n> = -1, there is no limit.
This parameter is never applied to <a href="glossary.html#">initial clause</a>s
or to clauses that <a href="hints.html">match hints</a>.
</blockquote>
<!-- end option -->

<!-- start option max_vars -->
<a name="max_vars">
<pre class="my_option">
assign(max_vars, <i>n</i>).  % default <i>n</i>=-1, range [-1 .. <tt>INT_MAX</tt>]
</pre>

<blockquote>
Clauses containing more than <i>n</i> (distinct) variables will be deleted.
If <n> = -1, there is no limit.
This parameter is never applied to <a href="glossary.html#">initial clause</a>s
or to clauses that <a href="hints.html">match hints</a>.
</blockquote>
<!-- end option -->

<!-- start option max_weight -->
<a name="max_weight">
<pre class="my_option">
assign(max_weight, <i>n</i>).  % default <i>n</i>=100, range [<tt>INT_MIN</tt> .. <tt>INT_MAX</tt>]
</pre>

<blockquote>
Derived clauses with weight greater then <i>n</i> will be discarded.
For this parameter, -1 does not mean infinity, because -1 is a reasonable
value (clauses can have negative weights).
This parameter is never applied to
<a href="glossary.html#">initial clause</a>s,
and it is not applied to
clauses that <a href="hints.html">match hints</a>
unless the flag <tt>limit_hint_matchers</tt> is set.
</blockquote>
<!-- end option -->

<!-- start option safe_unit_conflict -->
<a name="safe_unit_conflict">
<pre class="my_option">
set(safe_unit_conflict).
clear(safe_unit_conflict).    % default clear
</pre>

<blockquote>
This flag provides for a safe, but more expensive,
<a href="glossary.html#">unit conflict</a> test.
If set, the unit conflict test will be done
<i>before</i> the <a href="process-inf.html#max_weight"><tt><b>max_weight</b></tt></a> test is applied.
If the flag is clear, the test will be done <i>after</i>
the <a href="process-inf.html#max_weight"><tt><b>max_weight</b></tt></a> test is applied, allowing the possibility that
a proof will be missed, because the final step was deleted
by the <a href="process-inf.html#max_weight"><tt><b>max_weight</b></tt></a> parameter.
</blockquote>
<!-- end option -->

<h3>Performing Operations with the New Clause</h3>

The options in this section appear in the order in which they are applied.

<!-- start option factor -->
<a name="factor">
<pre class="my_option">
set(factor).
clear(factor).    % default clear
</pre>

<blockquote>
If this flag is set, <a href="glossary.html#">binary factoring</a> is applied to
newly-kept clauses.  Note that factoring is an inference rule
rather than a simplification rule, because a child is generated
and the parent is retained.  (If the child happens to subsume
the parent, the parent will be deleted by the <a href="glossary.html#subsumption">back subsumption</a>
process).  Unlike other inference rules such as resolution,
factoring is applied to a clause when it is <i>kept</i>,
not when it is <i>given</i>.
</blockquote>
<!-- end option -->

<!-- start option new_constants -->
<a name="new_constants">
<pre class="my_option">
assign(new_constants, <i>n</i>).  % default <i>n</i>=0, range [-1 .. <tt>INT_MAX</tt>]
</pre>

<blockquote>
If this parameter is greater than 0, Prover9 will apply a
rule that introduces a new constant when it derives an equation
that shows the existence of a constant.  In particular, if
a derived equation has the property that each side has
exactly one variable and those two variables are different,
a new constant
will be introduced and set equal to one side of the equation.
(Back demodulation will derive that the constant is equal to
the other side.)
<p>
For example, if <tt>x' * x = y * y'</tt> is derived, the
equation <tt>x' * x = c</tt> is produced, where the constant <tt>c</tt>
does not occur anywhere else.
<p>
The value of the parameter limits the number of new constants
that can be introduced by this rule.
<p>
(There is a more general rule allowing multiple variables.
Also, there is an extension to the rule that introduces (non-constant)
function symbols based on the intersection of the variables
of the two sides.  We have not found these extensions to be useful
in practice, so we have not included them in Prover9.)
<p>
Unlike other inference rules such as resolution, the
<a href="process-inf.html#new_constants"><tt><b>new_constants</b></tt></a>
rule is applied to a clause when it is <i>kept</i>,
not when it is <i>given</i>.
</blockquote>
<!-- end option -->

<!-- start option back_subsume -->
<a name="back_subsume">
<pre class="my_option">
set(back_subsume).    % default set
clear(back_subsume).
</pre>

<blockquote>
If this flag is set, then <a href="glossary.html#subsumption">back subsumption</a> is applied
with all new clauses.  That is, when a new clause is kept,
each clause subsumed by the new clause is deleted.
</blockquote>
<!-- end option -->

<!-- start option backsub_check -->
<a name="backsub_check">
<pre class="my_option">
assign(backsub_check, <i>n</i>).  % default <i>n</i>=500, range [-1 .. <tt>INT_MAX</tt>]
</pre>

<blockquote>
Back subsumption can be an expensive operation.  This
parameter tells Prover9 to check (once during the search)
whether back subsmption is removing enough clauses to justify
its use.
<p>
When the number of given clauses reaches this parameter,
Prover9 will calculate the percentage of kept clauses that
have been back subsumed;  if it is less than 5%, back
subsumption will be disabled.
</blockquote>
<!-- end option -->

<hr>
Next Section:
<a href="output.html">Output Files</a>

</body>
</html>