/usr/share/doc/prover9-doc/html/semantics.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 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN">
<html>
<head>
<title>Prover9 Manual: Semantic Guidance</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>Semantic Guidance</h1>
<p>
Prover9 has a method of using finite interpretations
to guide the search for a proof; in particular, to
help select the <a href="glossary.html#given-clause">given clause</a>.
<p>
To use semantic guidance the user gives one
or more interpretations along with the ordinary
Prover9 input. All clauses (input and derived) that are eligible to be
selected as given clauses are evaluated in the interpretations.
If a clause is false in all of the interpretations, it is
marked as "false" and given the attribute <tt>label(false)</tt>;
if it is true in any of the interpretations, it is marked as "true".
(There is an exception: see the parameter
<a href="semantics.html#eval_limit"><tt><b>eval_limit</b></tt></a>
below.)
<p>
If a clause being evaluated contains a symbol that is
not in an interpretation, a warning message is given, and
the clause receives the value "true".
<p>
When selecting the given clause,
Prover9 may use the parameters
<a href="select.html#true_part"><tt><b>true_part</b></tt></a>,and
<a href="select.html#false_part"><tt><b>false_part</b></tt></a>,
as described on the page
<a href="select.html">Selecting the Given Clause</a>.
With semantic guidance (explicit interpretations), the
"true_part" and "false_part" refer simply to clauses marked as
"true" and "false" with respect to the interpretations.
<h2>Format of Interpretations for Semantic Guidance</h2>
<p>
The interpretations are finite and must be in the format
produced by <a href="mace4.html">Mace4</a>. They must
appear in a list that starts with <tt>list(interpretations).</tt>
and ends with <tt>and_of_list.</tt> The following example
is a lattice in terms of the meet and join operations.
<pre class="my_file">
list(interpretations).
interpretation(6, [], [
function(^(_,_), [
0,0,0,0,0,0,
0,1,2,3,4,5,
0,2,2,0,0,0,
0,3,0,3,5,5,
0,4,0,5,4,5,
0,5,0,5,5,5]),
function(v(_,_), [
0,1,2,3,4,5,
1,1,1,1,1,1,
2,1,2,1,1,1,
3,1,1,3,1,3,
4,1,1,1,4,4,
5,1,1,3,4,5])]).
end_of_list.
</pre>
<h2>An Example of Semantic Guidance</h2>
<p>
Here a job that uses the preceding interpretation for semantic guidance.
<pre class="my_job">
prover9 -f <a href="../examples/LT-82-2.in">LT-82-2.in</a> > <a href="../examples/LT-82-2.out">LT-82-2.out</a>
</pre>
Notes about the preceding job.
<ul>
<li>
The interpretation is the only additional input needed to give
semantic guidance.
The default values of the parameters
<a href="select.html#age_part"><tt><b>age_part</b></tt></a>,
<a href="select.html#true_part"><tt><b>true_part</b></tt></a>,
<a href="select.html#false_part"><tt><b>false_part</b></tt></a>, and
<a href="select.html#eval_limit"><tt><b>eval_limit</b></tt></a>,
work well for this job (and many others).
<li>The interpretation does not contain Skolem constants that appear in
the denial, and warning messages are given when Prover9 attempts
to evaluate clauses containing those Skolem constants.
(They receive the value "true".)
<li>One of the input clauses is assigned the attribute
<tt>label(false)</tt>, because it is false in the interpretation.
<li>The "false" given clauses (#12, #13, #17, #18, #22, #23, ...)
are mostly heavier than the "true" given clauses, showing that they
would likely not enter the search at such an early stage without
semantic guidance.
<li>At given clause #138, there are no more false clauses to select;
and then several more are inferred and given near the end of the search,
leading to a proof.
<li>This job takes about 11 seconds. A similar job without
semantic guidance takes about 25 minutes to find a proof.
</ul>
<h2>Advice on Selecting Interpretations</h2>
If the conjecture formulates naturally as
<blockquote><i>
theory, hypotheses -> conclusion,
</i></blockquote>
a good first step is to try the smallest model of the theory
in which the conclusion is false.
The preceding example has that form, and
the interpretation used in the that example
can be easily found with the following Mace4 job.
<pre class="my_job">
mace4 -N10 -f <a href="../examples/LT-82-2-interp.in">LT-82-2-interp.in</a> > <a href="../examples/LT-82-2-interp.out">LT-82-2-interp.out</a>
</pre>
If the conjecture formulates naturally as
<blockquote><i>
theory -> conclusion,
</i></blockquote>
with no obvious hypothesis, one can try to slightly weaken the theory
in some way that relates to the conclusion,
and use a model of the weakened theory in which the conclusion is
false.
<h2>Options for Semantic Guidance</h2>
Aside from the parameters
<a href="select.html#true_part"><tt><b>true_part</b></tt></a>,and
<a href="select.html#false_part"><tt><b>false_part</b></tt></a>,
which may be used regardless of whether semantic guidance is in effect,
there are just two options to control semantic guidance.
<!-- start option order -->
<a name="multiple_interps">
<pre class="my_option">
assign(multiple_interps, <i>string</i>). % default <i>string</i>=false_in_all, range [false_in_all, false_in_some]
</pre>
<blockquote>
This parameter is used when there are multiple interpretations.
It determines the method for marking clauses as "false": false
in all interpretations, or false in some interpretations.
</blockquote>
<!-- end option -->
<!-- start option eval_limit -->
<a name="eval_limit">
<pre class="my_option">
assign(eval_limit, <i>n</i>). % default <i>n</i>=1024, range [-1 .. <tt>INT_MAX</tt>]
</pre>
<blockquote>
If an interpretation is large, or if a clause being
evaluated has many variables, evaluation can take too long,
because it must consider each instance of the clause over
the domain of the interpretation. That is if an interpretation
has size <i>d</i>, and a clause has <i>v</i> variables, evaluation
has to consider <i>d<sup>v</sup></i> instances of the clause to
determine that it is true.
This parameter causes large evaluations to be skipped.
<p>
This parameter applies when explicit interpretations are being used to
select the given clause.
When a clause is being evaluated in an interpretation, if
the number of ground instances that would be considered is greater than
<i>n</i>, the evaluation is skipped and the clause is assigned the
value <i>true</i>.
<p>
The default value of 1024 allows
<ul>
<li>
clauses with up to 3 variables to be evaluated in
interpretations up to size 10,
<li>
clauses with up to 4 variables to be evaluated in
interpretations up to size 5,
<li>
clauses with up to 5 variables to be evaluated in
interpretations up to size 4,
<li>
clauses with up to 6 variables to be evaluated in
interpretations up to size 3, and
<li>
clauses with up to 10 variables to be evaluated in
interpretations of size 2.
</ul>
</blockquote>
<!-- end option -->
<!-- start option eval_limit -->
<a name="eval_var_limit">
<pre class="my_option">
assign(eval_var_limit, <i>n</i>). % default <i>n</i>=-1, range [-1 .. <tt>INT_MAX</tt>]
</pre>
<blockquote>
This parameter is another (more convenient) way to limit the evaluation
of clauses. It overrides the parameter <tt>eval_limit</tt>.
Clauses with more than <i>n</i> variables will not be evaluated
in the largest interpretation(s).
<p>
In particular, if the value <i>n</i> is set to some value other than -1, the
parameter <tt>eval_limit</tt> will be reset to
<i>d<sup>n</sup></i>, where <i>d</i> is the size of the largest
interpretation in the input.
<p>
Note that if there are multiple interpretations of different sizes,
and if <tt>multiple_interps</tt> is set to "false_in_some", then
clauses with more than <i>n</i> variables may be evaluated in the
smaller interpretations.
</blockquote>
<!-- end option -->
<hr>
Next Section:
<a href="mace4.html">Mace4</a>
</body>
</html>
|