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
|
<!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>
<!-- 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>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 <g>given clause</g>.
<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 any of the interpretations, it is
marked as "false" and given the attribute <tt>label(false)</tt>;
if it is true in all 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 always uses 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>,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>terms(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">
terms(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="LT-82-2.in">LT-82-2.in</a> > <a href="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 hypothesis and conclusion are both 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="LT-82-2-interp.in">LT-82-2-interp.in</a> > <a href="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#age_part"><tt><b>age_part</b></tt></a>,
<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 used regardless of whether semantic guidance is in effect,
there is just one option,
<a href="semantics.html#eval_limit"><tt><b>eval_limit</b></tt></a>,
to control semantic guidance.
<p>
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.
The following parameter
causes large evaluations to be skipped.
<!-- 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 .. INT_MAX]
</pre>
<blockquote>
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 the 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 -->
</body>
</html>
|
