← Back to branch summary

~ubuntu-branches/ubuntu/trusty/spass/trusty

« back to all changes in this revision

Viewing changes to doc/html/script_1.html

  • Committer: Bazaar Package Importer
  • Author(s): Roland Stigge
  • Date: 2010-06-27 18:59:28 UTC
  • mfrom: (1.1.1 upstream)
  • Revision ID: james.westby@ubuntu.com-20100627185928-kdjuqghv04rxyqmc
Tags: 3.7-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
doc/html/script_1.html
 
1
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html401/loose.dtd">
 
2
<html>
 
3
<!-- Created on February, 23 2010 by texi2html 1.78 -->
 
4
<!--
 
5
Written by: Lionel Cons <Lionel.Cons@cern.ch> (original author)
 
6
            Karl Berry  <karl@freefriends.org>
 
7
            Olaf Bachmann <obachman@mathematik.uni-kl.de>
 
8
            and many others.
 
9
Maintained by: Many creative people.
 
10
Send bugs and suggestions to <texi2html-bug@nongnu.org>
 
11
 
 
12
-->
 
13
<head>
 
14
<title>frequently asked questions about SPASS: 1. SPASS</title>
 
15
 
 
16
<meta name="description" content="frequently asked questions about SPASS: 1. SPASS">
 
17
<meta name="keywords" content="frequently asked questions about SPASS: 1. SPASS">
 
18
<meta name="resource-type" content="document">
 
19
<meta name="distribution" content="global">
 
20
<meta name="Generator" content="texi2html 1.78">
 
21
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
 
22
<style type="text/css">
 
23
<!--
 
24
a.summary-letter {text-decoration: none}
 
25
pre.display {font-family: serif}
 
26
pre.format {font-family: serif}
 
27
pre.menu-comment {font-family: serif}
 
28
pre.menu-preformatted {font-family: serif}
 
29
pre.smalldisplay {font-family: serif; font-size: smaller}
 
30
pre.smallexample {font-size: smaller}
 
31
pre.smallformat {font-family: serif; font-size: smaller}
 
32
pre.smalllisp {font-size: smaller}
 
33
span.roman {font-family:serif; font-weight:normal;}
 
34
span.sansserif {font-family:sans-serif; font-weight:normal;}
 
35
ul.toc {list-style: none}
 
36
-->
 
37
</style>
 
38
 
 
39
 
 
40
</head>
 
41
 
 
42
<body lang="en" bgcolor="#FFFFFF" text="#000000" link="#0000FF" vlink="#800080" alink="#FF0000">
 
43
 
 
44
<table cellpadding="1" cellspacing="1" border="0">
 
45
<tr><td valign="middle" align="left">[ &lt;&lt; ]</td>
 
46
<td valign="middle" align="left">[<a href="script_2.html#SEC10" title="Next chapter"> &gt;&gt; </a>]</td>
 
47
<td valign="middle" align="left"> &nbsp; </td>
 
48
<td valign="middle" align="left"> &nbsp; </td>
 
49
<td valign="middle" align="left"> &nbsp; </td>
 
50
<td valign="middle" align="left"> &nbsp; </td>
 
51
<td valign="middle" align="left"> &nbsp; </td>
 
52
<td valign="middle" align="left">[<a href="script.html#Top" title="Cover (top) of document">Top</a>]</td>
 
53
<td valign="middle" align="left">[Contents]</td>
 
54
<td valign="middle" align="left">[Index]</td>
 
55
<td valign="middle" align="left">[<a href="script_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
 
56
</tr></table>
 
57
 
 
58
<hr size="2">
 
59
<a name="SPASS"></a>
 
60
<a name="SEC1"></a>
 
61
<h1 class="chapter"> 1. SPASS </h1>
 
62
 
 
63
<hr size="6">
 
64
<a name="SEC2"></a>
 
65
<h2 class="section"> 1.1 NAME </h2>
 
66
<p>SPASS - an automated theorem prover for full first-order logic with equality
 
67
</p>
 
68
<hr size="6">
 
69
<a name="SEC3"></a>
 
70
<h2 class="section"> 1.2 SYNOPSIS </h2>
 
71
<p>SPASS [&lsquo;<samp>options</samp>&rsquo;] [<var>inputfile</var>]
 
72
</p>
 
73
<hr size="6">
 
74
<a name="SEC4"></a>
 
75
<h2 class="section"> 1.3 DESCRIPTION </h2>
 
76
<p>SPASS is an automated theorem prover for full sorted first-order logic with equality
 
77
that extends superposition by sorts and a splitting rule for case analysis.
 
78
SPASS can also be used as a modal logic and description logic theorem prover.
 
79
</p>
 
80
<hr size="6">
 
81
<a name="SEC5"></a>
 
82
<h2 class="section"> 1.4 OPTIONS </h2>
 
83
<p>Command line options in SPASS are implemented via modifications to the GNU command
 
84
line option package for C. Just giving the option sets its value to 1 and means enabling
 
85
the option. In order to disable
 
86
an option the value has to be set to 0 by declaring -<i>Option</i>=0.
 
87
The following options are currently supported by SPASS:
 
88
</p>
 
89
<dl compact="compact">
 
90
<dt> <kbd>-Auto</kbd></dt>
 
91
<dd><br><p>Enables/disables the auto mode where SPASS configures itself automatically.
 
92
The inference/reduction rules, the sort technology, the ordering and precedence
 
93
as well as the splitting and selection strategy are set.
 
94
In auto mode SPASS is complete. Mixing the auto mode with user defined options
 
95
may destroy completeness.
 
96
Default is 1.
 
97
</p></dd>
 
98
<dt> <kbd>-Stdin</kbd></dt>
 
99
<dd><p>Enables/disables input in SPASS via stdin. The file argument is ignored. Default is 0.
 
100
</p></dd>
 
101
<dt> <kbd>-Interactive</kbd></dt>
 
102
<dd><p>Enables/disables the interactive mode. First, SPASS is given a set of axioms and then
 
103
the prover accepts subsequent proof tasks. Default is 0.
 
104
</p></dd>
 
105
<dt> <kbd>-Flotter</kbd></dt>
 
106
<dd><p>Enables/disables the CNF translation mode of SPASS. If the option is set, SPASS only
 
107
performs a clause normal form translation. If no output file argument is given
 
108
SPASS prints the CNF to stdout. Default is 0.
 
109
</p></dd>
 
110
<dt> <kbd>-SOS</kbd></dt>
 
111
<dd><p>Enables/disables the set of support strategy. Default is 0.
 
112
</p></dd>
 
113
<dt> <kbd>-Splits=<i>n</i></kbd></dt>
 
114
<dd><p>Sets the number of possible splitting applications to <i>n</i>. If <i>n</i>=-1 then
 
115
the number of splits is not limited. Default is 0.
 
116
</p></dd>
 
117
<dt> <kbd>-Memory=<i>n</i></kbd></dt>
 
118
<dd><p>Sets the amount of memory available to SPASS for the proof search to <i>n</i> bytes. 
 
119
The memory needed to startup SPASS cannot be restricted.
 
120
Default is -1 meaning that memory allocations is only restricted by available memory.
 
121
</p></dd>
 
122
<dt> <kbd>-TimeLimit=<i>n</i></kbd></dt>
 
123
<dd><p>Sets a time limit for the proof search to <i>n</i> seconds. Default is -1 meaning that
 
124
SPASS may run forever. The time limit is polled when SPASS selects a new clause for
 
125
inferences. If a single inference step causes an explosion to the number of generated
 
126
clauses it may therefore happen that a given time limit is significantly exceeded.
 
127
</p></dd>
 
128
<dt> <kbd>-DocSST</kbd></dt>
 
129
<dd><p>Enables/disables documentation output for static soft typing. 
 
130
The used sort theory as well as the (failed) proof attempt for
 
131
the sort constraint is printed.
 
132
Default is 0.
 
133
</p></dd>
 
134
<dt> <kbd>-DocProof</kbd></dt>
 
135
<dd><p>Enables/disables proof documentation. If SPASS finds a proof it is eventually
 
136
printed. If SPASS finds a saturation, the saturated set of clauses is eventually printed.
 
137
Enabling proof documentation may significantly decrease SPASS's performance, because
 
138
the prover must store clauses that can be thrown away otherwise. Default is 0.
 
139
</p></dd>
 
140
<dt> <kbd>-DocSplit</kbd></dt>
 
141
<dd><p>Sets the documentation of split backtracking steps. If set to 1, the
 
142
current backtracking level is printed. If set to 2, it also prints in case
 
143
of a split backtrack the backtracked clauese.
 
144
Default is 0.
 
145
</p></dd>
 
146
<dt> <kbd>-Loops</kbd></dt>
 
147
<dd><p>Sets the maximal number of mainloop iterations for SPASS.
 
148
Default is -1.
 
149
</p></dd>
 
150
<dt> <kbd>-PSub</kbd></dt>
 
151
<dd><p>Enables/disables printing of subsumed clauses.
 
152
Default is 0.
 
153
</p></dd>
 
154
<dt> <kbd>-PRew</kbd></dt>
 
155
<dd><p>Enables/disables printing of simple rewrite applications.
 
156
Default is 0.
 
157
</p></dd>
 
158
<dt> <kbd>-PCon</kbd></dt>
 
159
<dd><p>Enables/disables printing of condensation applications.
 
160
Default is 0.
 
161
</p></dd>
 
162
<dt> <kbd>-PTaut</kbd></dt>
 
163
<dd><p>Enables/disables printing of tautology deletion applications.
 
164
Default is 0.
 
165
</p></dd>
 
166
<dt> <kbd>-PObv</kbd></dt>
 
167
<dd><p>Enables/disables printing of obvious reduction applications.
 
168
Default is 0.
 
169
</p></dd>
 
170
<dt> <kbd>-PSSi</kbd></dt>
 
171
<dd><p>Enables/disables printing of sort simplification applications.
 
172
Default is 0.
 
173
</p></dd>
 
174
<dt> <kbd>-PSST</kbd></dt>
 
175
<dd><p>Enables/disables printing of static soft typing applications.
 
176
All deleted clauses are printed.
 
177
Default is 0.
 
178
</p></dd>
 
179
<dt> <kbd>-PMRR</kbd></dt>
 
180
<dd><p>Enables/disables printing of matching replacement resolution applications.
 
181
Default is 0.
 
182
</p></dd>
 
183
<dt> <kbd>-PUnC</kbd></dt>
 
184
<dd><p>Enables/disables printing of unit conflict applications.
 
185
Default is 0.
 
186
</p></dd>
 
187
<dt> <kbd>-PAED</kbd></dt>
 
188
<dd><p>Enables/disables printing of clauses where redundant
 
189
equations have been removed (assignment equation deletion).
 
190
</p></dd>
 
191
<dt> <kbd>-PDer</kbd></dt>
 
192
<dd><p>Enables/disables printing of clauses derived by inferences.
 
193
Default is 0.
 
194
</p></dd>
 
195
<dt> <kbd>-PGiven</kbd> </dt>
 
196
<dd><p>Enables/disables printing of the given clause, selected
 
197
to perform inferences.
 
198
Default is 0.
 
199
</p></dd>
 
200
<dt> <kbd>-PLabels</kbd></dt>
 
201
<dd><p>Enables/disables printing of labels. If the -DocProof is
 
202
set and no labels for formulae are provided by the input,
 
203
SPASS generates generic labels that are then printed by enabling this option.
 
204
Default is 0.
 
205
</p></dd>
 
206
<dt> <kbd>-PKept</kbd></dt>
 
207
<dd><p>Enables/disables printing of kept clauses. These are clauses
 
208
generated by inferences (backtracking) that are not redundant.
 
209
Clauses derived during input reduction/saturation are not printed.
 
210
Default is 0.
 
211
</p></dd>
 
212
<dt> <kbd>-PProblem</kbd></dt>
 
213
<dd><p>Enables/disables printing of the input clause set.
 
214
Default is 1.
 
215
</p></dd>
 
216
<dt> <kbd>-PEmptyClause</kbd></dt>
 
217
<dd><p>Enables/disables printing of derived empty clauses.
 
218
Default is 0.
 
219
</p></dd>
 
220
<dt> <kbd>-PStatistic</kbd></dt>
 
221
<dd><p>Enables/disables printing of a final statistics on derived/backtracked/kept clauses, performed splits,
 
222
used time and used space.
 
223
Default is 1.
 
224
</p></dd>
 
225
<dt> <kbd>-FPModel</kbd></dt>
 
226
<dd><p>Enables/disables the output of an eventually found model to a file. If set
 
227
to 1, all clauses in the final set are printed. If set to 2, only
 
228
potentially productive clauses are printed, that are clauses with no selected
 
229
negative literal and a maximal positive one. If &lt;problemfile&gt; is the name
 
230
of the input problem and the eventually generated set is saturated, the
 
231
saturation is printed to the file &lt;problemfile&gt;.model, for otherwise
 
232
to &lt;problemfile&gt;.clauses. The latter case may, e.g., be caused by a time limit.
 
233
Default is 0.
 
234
</p></dd>
 
235
<dt> <kbd>-FPDFGProof</kbd></dt>
 
236
<dd><p>Enables/disables the output of an eventually found proof to a file. Using this
 
237
option requires to set the option -DocProof. If &lt;problemfile&gt; is the name
 
238
of the input problem the proof is printed to &lt;problemfile&gt;.prf.
 
239
Default is 0.
 
240
</p></dd>
 
241
<dt> <kbd>-PFlags</kbd></dt>
 
242
<dd><p>Enables/disables the output of all flag values. The flag settings are
 
243
printed at the end of a SPASS run in form of a DFG-Syntax input section.
 
244
Default is 0.
 
245
</p></dd>
 
246
<dt> <kbd>-POptSkolem</kbd></dt>
 
247
<dd><p>Enables/disables the output of optimized Skolemization applications.
 
248
Default is 0.
 
249
</p></dd>
 
250
<dt> <kbd>-PStrSkolem</kbd></dt>
 
251
<dd><p>Enables/disables the output of strong Skolemization applications.
 
252
Default is 0.
 
253
</p></dd>
 
254
<dt> <kbd>-PBDC</kbd></dt>
 
255
<dd><p>Enables/disables the output of clauses deleted because of
 
256
bound restrictions. 
 
257
Default is 0.
 
258
</p></dd>
 
259
<dt> <kbd>-PBInc</kbd></dt>
 
260
<dd><p>Enables/disables the output of bound restriction changes. 
 
261
Default is 0.
 
262
</p></dd>
 
263
<dt> <kbd>-PApplyDefs</kbd> </dt>
 
264
<dd><p>Enables/disables printing of expansions of atom definitions.
 
265
Default is 0.
 
266
</p></dd>
 
267
<dt> <kbd>-Select</kbd></dt>
 
268
<dd><p>Sets the selection strategy for SPASS. If set to 0 no selection
 
269
of negative literals is done. If set to any other value, at most
 
270
one negative literal in a clause is selected. If set to 1 negative 
 
271
literals in clauses with more than one maximal literal are selected.
 
272
Either a negative literal with a predicate from the selection list (see below) is chosen
 
273
or if no such negative literal is available, a negative literal with maximal weight is chosen.
 
274
If set to 2 negative literals are always selected. Again,
 
275
either a negative literal with a predicate from the selection list (see below) is chosen
 
276
or if no such negative literal is available, a negative literal with maximal weight is chosen.
 
277
The latter case results
 
278
in an ordered hyperresolution like behavior of ordered resolution.
 
279
If set to 3 any negative literal with a predicate specified by the selection list (see below)
 
280
is selected.
 
281
Default is 1.
 
282
</p></dd>
 
283
<dt> <kbd>-RInput</kbd></dt>
 
284
<dd><p>Enables/disables the reduction of the initial clause set.
 
285
Default is 1.
 
286
</p></dd>
 
287
<dt> <kbd>-Sorts</kbd></dt>
 
288
<dd><p>Determines the monadic literals that built the sort constraint
 
289
for the initial clause set.
 
290
If set to 0, no sort constraint is built. If set to 1, all negative
 
291
monadic literals with a variable as argument form the sort constraint.
 
292
If set to 2, all negative monadic literals form the sort constraint.
 
293
Setting -Sorts to 2 may harm completeness, since sort constraints are
 
294
subject to the basic strategy and to static soft typing.
 
295
Default is 1.
 
296
</p></dd>
 
297
<dt> <kbd>-SatInput</kbd></dt>
 
298
<dd><p>Enables/disables input saturation. The saturation is incomplete
 
299
but is guaranteed to terminate.
 
300
Default is 0.
 
301
</p></dd>
 
302
<dt> <kbd>-WDRatio</kbd></dt>
 
303
<dd><p>Sets the ratio between given clauses selected by
 
304
weight or the depth in the search space. The weight is the
 
305
sum of all symbol weights determined by the -FuncWeight and
 
306
-VarWeight options. The depth of all initial clauses is 0 and
 
307
clauses generated by inferences get the maximal depth of a parent
 
308
clause plus 1.
 
309
Default is 5, meaning
 
310
that 4 clauses are selected by weight and the fifth clause is
 
311
selected by depth.
 
312
</p></dd>
 
313
<dt> <kbd>-PrefCon</kbd></dt>
 
314
<dd><p>Sets the ratio to compute the weight for conjecture clauses
 
315
and therefore allows to prefer those. Default is 0 meaning that
 
316
the weight computation for conjecture clauses is not changed.
 
317
</p></dd>
 
318
<dt> <kbd>-FullRed</kbd></dt>
 
319
<dd><p>Enables/disables full reduction. If set to 0, only the set of worked
 
320
off clauses is completely inter-reduced. If set to 1, all currently
 
321
hold clauses (worked off and usable) are completely inter-reduced.
 
322
Default is 1.
 
323
</p></dd>
 
324
<dt> <kbd>-FuncWeight</kbd> </dt>
 
325
<dd><p>Sets the weight of function/predicate symbols. The weight of
 
326
clauses is the sum of all symbol weights. This weight is considered
 
327
for the selection of the given clause. Default is 1.
 
328
</p></dd>
 
329
<dt> <kbd>-VarWeight</kbd> </dt>
 
330
<dd><p>Sets the weight of variable symbols (see -FuncWeight).
 
331
Default is 1.
 
332
</p></dd>
 
333
<dt> <kbd>-PrefVar</kbd> </dt>
 
334
<dd><p>Enables/disables the preference for clauses with many variables.
 
335
While clauses are selected by weight, if this option is set and
 
336
two clauses have the same weight, the clause with more variable
 
337
occurrences is preferred.
 
338
Default is 0.
 
339
</p></dd>
 
340
<dt> <kbd>-BoundMode</kbd></dt>
 
341
<dd><p>Selects the mode for bound restrictions. Mode 0 means no
 
342
restriction, if set to 1 all newly generated clauses are restricted by weight
 
343
(see -BoundStart) and if set to 2 clauses are restricted
 
344
by depth. Default is 0.
 
345
</p></dd>
 
346
<dt> <kbd>-BoundStart</kbd></dt>
 
347
<dd><p>The start restriction of the selected bound mode. For example,
 
348
if bound mode is 1 and bound start set to 5, all clauses with
 
349
a weight larger than 5 are deleted until the set is saturated.
 
350
This causes an increase of the used bound value that is
 
351
determined by the minimal increase saving a before deleted
 
352
clause. Default is -1 meaning no bound restriction.
 
353
</p></dd>
 
354
<dt> <kbd>-BoundLoops</kbd> </dt>
 
355
<dd><p>The number of loops applying the actions restrictions/increasing bound.
 
356
If the number of loops is exceeded all bound restrictions are
 
357
cancelled. Default is 1.
 
358
</p></dd>
 
359
<dt> <kbd>-ApplyDefs</kbd></dt>
 
360
<dd><p>Sets the maximal number of applications of atom definitions to input formulae.
 
361
Default is 0, meaning no applications at all.
 
362
</p></dd>
 
363
<dt> <kbd>-Ordering</kbd> </dt>
 
364
<dd><p>Sets the term ordering. If 0 then KBO is selected,
 
365
if 1 the RPOS is selected. Default is 0.          
 
366
</p></dd>
 
367
<dt> <kbd>-CNFQuantExch</kbd></dt>
 
368
<dd><p>If set, non-constant Skolem terms in the clausal form of the
 
369
conjecture are replaced by constants.
 
370
Will automatically be set for the optimized functional translation of
 
371
modal or description logic formulae.
 
372
Default is 0.
 
373
</p></dd>
 
374
<dt> <kbd>-CNFOptSkolem</kbd>  </dt>
 
375
<dd><p>Enables/disables optimized Skolemization.
 
376
Default is 1.
 
377
</p></dd>
 
378
<dt> <kbd>-CNFStrSkolem</kbd> </dt>
 
379
<dd><p>Enables/disables Strong Skolemization.
 
380
Default is 1.
 
381
</p></dd>
 
382
<dt> <kbd>-CNFProofSteps</kbd></dt>
 
383
<dd><p>Sets the maximal number of proof steps
 
384
in an optimized Skolemization proof attempt.
 
385
Default is 100. 
 
386
</p></dd>
 
387
<dt> <kbd>-CNFSub</kbd></dt>
 
388
<dd><p>Enables/disables subsumption on the clauses generated by the CNF procedure.
 
389
Default is 1.    
 
390
</p></dd>
 
391
<dt> <kbd>-CNFCon</kbd></dt>
 
392
<dd><p>Enables/disables condensing on the clauses generated by the CNF procedure.
 
393
Default is 1.
 
394
</p></dd>
 
395
<dt> <kbd>-CNFRedTime</kbd></dt>
 
396
<dd><p>Sets the overall amount of time in seconds to be spend on reduction during
 
397
CNF transformation. Affected reductions are optimized Skolemization, condensing,
 
398
and subsumption. Default is -1 meaning that the reduction time is not limited
 
399
at all.
 
400
</p></dd>
 
401
<dt> <kbd>-CNFRenaming</kbd>  </dt>
 
402
<dd><p>Enables/disables formula renaming.
 
403
If set to 1 optimized renaming is enabled that minimizes
 
404
the number of eventually generated clauses.
 
405
If set to 2 complex renaming is enabled that introduces a
 
406
new Skolem predicate for every complex  formula, i.e., any
 
407
formula that is not a literal.
 
408
If set to 3 quantification renaming is enabled that introduces
 
409
a new Skolem predicate for every subformula starting with
 
410
a quantifier.
 
411
Default is 1.
 
412
</p></dd>
 
413
<dt> <kbd>-CNFRenMatch</kbd></dt>
 
414
<dd><p>If set, renaming variant subformulae are replaced by the same
 
415
Skolem literal.
 
416
Default is 1.
 
417
</p></dd>
 
418
<dt> <kbd>-CNFPRenaming</kbd>    </dt>
 
419
<dd><p>Enables/disables the printing of formula renaming applications.
 
420
Default is 0.
 
421
</p></dd>
 
422
<dt> <kbd>-CNFFEqR</kbd></dt>
 
423
<dd><p>Enables/disables certain equality reduction techniques
 
424
on the formula level. Default is 1.
 
425
</p></dd>
 
426
<dt> <kbd>-IEmS</kbd>  </dt>
 
427
<dd><p>Enables/disables the inference rule Empty Sort.
 
428
Default is 0.
 
429
</p></dd>
 
430
<dt> <kbd>-ISoR</kbd>  </dt>
 
431
<dd><p>Enables/disables the inference rule Sort Resolution.
 
432
Default is 0. 
 
433
</p></dd>
 
434
<dt> <kbd>-IEqR</kbd></dt>
 
435
<dd><p>Enables/disables the inference rule Equality Resolution.
 
436
Default is 0. 
 
437
</p></dd>
 
438
<dt> <kbd>-IERR</kbd></dt>
 
439
<dd><p>Enables/disables the inference rule Reflexivity Resolution.
 
440
Default is 0. 
 
441
</p></dd>
 
442
<dt> <kbd>-IEqF</kbd>   </dt>
 
443
<dd><p>Enables/disables the inference rule Equality Factoring.
 
444
Default is 0.       
 
445
</p></dd>
 
446
<dt> <kbd>-IMPm</kbd>  </dt>
 
447
<dd><p>Enables/disables the inference rule Merging Paramodulation.
 
448
Default is 0.             
 
449
</p></dd>
 
450
<dt> <kbd>-ISpR</kbd>   </dt>
 
451
<dd><p>Enables/disables the inference rule Superposition Right.
 
452
Default is 0.    
 
453
</p></dd>
 
454
<dt> <kbd>-IOPm</kbd></dt>
 
455
<dd><p>Enables/disables the inference rule Ordered Paramodulation.
 
456
Default is 0.      
 
457
</p></dd>
 
458
<dt> <kbd>-ISPm</kbd>   </dt>
 
459
<dd><p>Enables/disables the inference rule Standard Paramodulation.
 
460
Default is 0.    
 
461
</p></dd>
 
462
<dt> <kbd>-ISpL</kbd>               </dt>
 
463
<dd><p>Enables/disables the inference rule Superposition Left.
 
464
Default is 0.
 
465
</p></dd>
 
466
<dt> <kbd>-IORe</kbd></dt>
 
467
<dd><p>Enables/disables the inference rule Ordered Resolution.
 
468
If set to 1, Ordered Resolution is enabled but no resolution
 
469
inferences with equations are generated. If set to 2, equations
 
470
are considered for Ordered Resolution steps as well.
 
471
Default is 0. 
 
472
</p></dd>
 
473
<dt> <kbd>-ISRe</kbd></dt>
 
474
<dd><p>Enables/disables the inference rule Standard Resolution.
 
475
If set to 1, Standard Resolution is enabled but no resolution
 
476
inferences with equations are generated. If set to 2, equations
 
477
are considered for Standard Resolution steps as well.
 
478
Default is 0.   
 
479
</p></dd>
 
480
<dt> <kbd>-ISHy</kbd> </dt>
 
481
<dd><p>Enables/disables the inference rule Standard Hyper-Resolution.
 
482
Default is 0.     
 
483
</p></dd>
 
484
<dt> <kbd>-IOHy</kbd></dt>
 
485
<dd><p>Enables/disables the inference rule Ordered Hyper-Resolution.
 
486
Default is 0.  
 
487
</p></dd>
 
488
<dt> <kbd>-IURR</kbd></dt>
 
489
<dd><p>Enables/disables the inference rule Unit Resulting Resolution.
 
490
Default is 0.
 
491
</p></dd>
 
492
<dt> <kbd>-IOFc</kbd></dt>
 
493
<dd><p>Enables/disables the inference rule Ordered Factoring.
 
494
If set to 1, Ordered Factoring is enabled but only factoring
 
495
inferences with positive literals are generated. If set to 2,
 
496
negative literals are considered for inferences as well.
 
497
Default is 0. 
 
498
</p></dd>
 
499
<dt> <kbd>-ISFc</kbd></dt>
 
500
<dd><p>Enables/disables the inference rule Standard Factoring.
 
501
Default is 0. 
 
502
</p></dd>
 
503
<dt> <kbd>-IUnR</kbd></dt>
 
504
<dd><p>Enables/disables the inference rule Unit Resolution.
 
505
Default is 0.        
 
506
</p></dd>
 
507
<dt> <kbd>-IBUR</kbd></dt>
 
508
<dd><p>Enables/disables the inference rule Bounded Depth Unit Resolution.
 
509
Default is 0.      
 
510
</p></dd>
 
511
<dt> <kbd>-IDEF</kbd></dt>
 
512
<dd><p>Enables/disables the inference rule Apply Definitions.
 
513
Currently not supported.
 
514
Default is 0.               
 
515
</p></dd>
 
516
<dt> <kbd>-RFRew</kbd></dt>
 
517
<dd><p>Enables/disables the reduction rule Forward Rewriting.
 
518
If set to 1 unit rewriting and non-unit rewriting based on
 
519
a subsumption test is activated.
 
520
If set to 2 in addition to unit and non-unit rewriting
 
521
local contextual rewriting is activated.
 
522
If set to 3 in  addition to unit and non-unit rewriting
 
523
subterm contextual rewriting is activiated. Subterm contextual
 
524
rewriting subsumes local contextual rewriting.
 
525
If set to 4 in addition of the rewriting rules of 3, subterm
 
526
contextual rewriting also tests for negative literal elimination.
 
527
Default is 0.   
 
528
</p></dd>
 
529
<dt> <kbd>-RBRew</kbd></dt>
 
530
<dd><p>Enables/disables the reduction rule Backward Rewriting.
 
531
Same values and meaning as for flag -RFRew but used in backward direction.
 
532
Default is 0.    
 
533
</p></dd>
 
534
<dt> <kbd>-RFMRR</kbd></dt>
 
535
<dd><p>Enables/disables the reduction rule Forward Matching Replacement Resolution.
 
536
Default is 0.              
 
537
</p></dd>
 
538
<dt> <kbd>-RBMRR</kbd></dt>
 
539
<dd><p>Enables/disables the reduction rule Backward Matching Replacement Resolution.
 
540
Default is 0.   
 
541
</p></dd>
 
542
<dt> <kbd>-RObv</kbd></dt>
 
543
<dd><p>Enables/disables the reduction rule Obvious Reduction.
 
544
Default is 0.                
 
545
</p></dd>
 
546
<dt> <kbd>-RUnC</kbd></dt>
 
547
<dd><p>Enables/disables the reduction rule Unit Conflict.
 
548
Default is 0. 
 
549
</p></dd>
 
550
<dt> <kbd>-RTer</kbd> </dt>
 
551
<dd><p>Enables/disables the terminator by setting the maximal number
 
552
of non-unit clauses to be used during the search.   
 
553
Default is 0.
 
554
</p></dd>
 
555
<dt> <kbd>-RTaut</kbd></dt>
 
556
<dd><p>Enables/disables the reduction rule Tautology Deletion. If
 
557
set to 1, only syntactic tautologies are detected and
 
558
deleted. If
 
559
set to 2, additionally semantic tautologies are removed.
 
560
Default is 0.              
 
561
</p></dd>
 
562
<dt> <kbd>-RSST</kbd></dt>
 
563
<dd><p>Enables/disables the reduction rule Static Soft Typing.
 
564
Default is 0.            
 
565
</p></dd>
 
566
<dt> <kbd>-RSSi</kbd></dt>
 
567
<dd><p>Enables/disables the reduction rule Sort Simplification.
 
568
Default is 0.               
 
569
</p></dd>
 
570
<dt> <kbd>-RFSub</kbd></dt>
 
571
<dd><p>Enables/disables the reduction rule Forward Subsumption Deletion.
 
572
Default is 0.              
 
573
</p></dd>
 
574
<dt> <kbd>-RBSub</kbd></dt>
 
575
<dd><p>Enables/disables the reduction rule Backward Subsumption Deletion.
 
576
Default is 0.  
 
577
</p></dd>
 
578
<dt> <kbd>-RAED</kbd></dt>
 
579
<dd><p>Enables/disables the reduction rule Assignment Equation Deletion.
 
580
This rule removes particular occurrences of equations from clauses.
 
581
If set to 1, the reduction is guaranteed to be sound.
 
582
If set to 2, the reduction is only sound if any potential model
 
583
of the considered problem has a non-trivial domain.
 
584
Default is 0.
 
585
</p></dd>
 
586
<dt> <kbd>-RCon</kbd></dt>
 
587
<dd><p>Enables/disables the reduction rule Condensation.
 
588
Default is 0.               
 
589
</p></dd>
 
590
<dt> <kbd>-TDfg2OtterOptions</kbd></dt>
 
591
<dd><p>Enables/disables the inclusion of an Otter options
 
592
header. This option only applies to dfg2otter. If
 
593
set to 1 it includes a setting that makes Otter nearly
 
594
complete. If set to 2 it activates auto modus and if
 
595
set to 3 it activates the auto2 modus.
 
596
Default is 0.
 
597
</p></dd>
 
598
<dt> <kbd>-EML</kbd></dt>
 
599
<dd><p>A special EML flag for modal logic or description logic formulae.
 
600
Never needs to be set explicitly.  Is set during parsing.
 
601
</p></dd>
 
602
<dt> <kbd>-EMLAuto</kbd></dt>
 
603
<dd><p>Intended for EML Autonomous mode, as yet not functional.
 
604
Default is 0.              
 
605
</p></dd>
 
606
<dt> <kbd>-EMLTranslation</kbd></dt>
 
607
<dd><p>Determines the translation method used
 
608
for modal logic or description logic formulae.
 
609
If set to 0, the standard relational translation method (which
 
610
is determined by the usual Kripke semantics) is used.
 
611
If set to 1, the functional translation method is used.
 
612
If set to 2, the optimised functional translation method is used.
 
613
If set to 3, the semi-functional translation method is used.
 
614
A variation of the optimised functional translation method is used, when
 
615
the following settings are specified: -EMLTranslation=2 -EMLFuncNary=1.
 
616
The translation will be in terms of n-ary predicates instead of unary
 
617
predicates and paths.
 
618
In the current implementation the standard relational translation method
 
619
is most general. Some
 
620
restrictions apply to the other methods. The functional translation
 
621
method and semi-functional translation methods are available only for
 
622
the basic multi-modal logic K(m) possibly with serial (total) modalities
 
623
(-EMLTheory=1), plus nominals (ABox statements), terminological axioms
 
624
and general inclusion and equivalence axioms. The optimised functional
 
625
translation methods are implemented only for K(m), possibly with serial
 
626
modalities.
 
627
Default is 0.              
 
628
</p></dd>
 
629
<dt> <kbd>-EML2Rel</kbd></dt>
 
630
<dd><p>If set, propositional/Boolean-type formulae are converted to relational formulae
 
631
before they are translated to first-order logic.
 
632
Default is 0.              
 
633
</p></dd>
 
634
<dt> <kbd>-EMLTheory</kbd></dt>
 
635
<dd><p>Determines which background theory is assumed.
 
636
If set to 0, the background theory is empty.
 
637
If set to 1, then seriality (the background theory for KD) is added for
 
638
all modalities. 
 
639
If set to 2, then reflexivity (the background theory for KT) is added for
 
640
all modalities. 
 
641
If set to 3, then symmetry (the background theory for KB) is added for
 
642
all modalities. 
 
643
If set to 4, then transitivity (the background theory for K4) is added for
 
644
all modalities. 
 
645
If set to 5, then Euclideanness (the background theory for K5) is added for
 
646
all modalities. 
 
647
If set to 6, then transitivity and Euclideanness (the background theory
 
648
for S4) is added for all modalities. 
 
649
If set to 7, then reflexivity, transitivity and Euclideanness (the
 
650
background theory for S5) is added for all modalities. 
 
651
Default is 0.              
 
652
</p></dd>
 
653
<dt> <kbd>-EMLFuncNdeQ</kbd></dt>
 
654
<dd><p>If set, diamond formulae are translated according to
 
655
tr(dia(phi),s) = nde(s) /\ exists x tr(phi,[s x])
 
656
(a nde / quantifier formula),
 
657
otherwise the translation is in accordance with
 
658
tr(dia(phi),s) = exists x nde(s) /\ tr(phi,[s x])
 
659
(a quantifier / nde formula).  
 
660
The transltion for box formulae is defined dually.
 
661
Setting this flag is only meaningful when the flag for the functional or
 
662
semi functional translation method is set.
 
663
Default is 1.              
 
664
</p></dd>
 
665
<dt> <kbd>-EMLFuncNary</kbd></dt>
 
666
<dd><p>If set, the functional translation into fluted logic is used.
 
667
This means n-ary predicate symbols are used instead of unary predicate
 
668
symbols and paths.
 
669
Setting this flag is only meaningful for testing local
 
670
satisfiability/validity in multi-modal K.
 
671
Default is 0.              
 
672
</p></dd>
 
673
<dt> <kbd>-EMLFFSorts</kbd></dt>
 
674
<dd><p>If set, sorts for terms are used.
 
675
Default is 0.              
 
676
</p></dd>
 
677
<dt> <kbd>-EMLElimComp</kbd></dt>
 
678
<dd><p>If set, try to eliminate relational composition in modal parameters.
 
679
Default is 0.   
 
680
</p></dd>
 
681
<dt> <kbd>-EMLPTrans</kbd></dt>
 
682
<dd><p>If set, the EML to first-order logic translation is documented.
 
683
Default is 0.    
 
684
</p></dd>
 
685
<dt> <kbd>-TPTP</kbd></dt>
 
686
<dd><p>If set, SPASS expects an input file in TPTP syntax.
 
687
Default is 0. 
 
688
</p></dd>
 
689
<dt> <kbd>-rf</kbd></dt>
 
690
<dd><p>If set, SPASS deletes the input file before termination.
 
691
Default is 0.            
 
692
</p></dd>
 
693
</dl>
 
694
 
 
695
<hr size="6">
 
696
<a name="SEC6"></a>
 
697
<h2 class="section"> 1.5 SETTINGS </h2>
 
698
<p>You can also specify options for SPASS in the input problem.
 
699
In the DFG syntax, you would use
 
700
</p><table><tr><td>&nbsp;</td><td><pre class="example">list_of_settings(SPASS).
 
701
{*
 
702
  set_flag(DocProof,1).
 
703
*}
 
704
end_of_list.
 
705
</pre></td></tr></table>
 
706
<p>to set the DocProof flag.
 
707
</p>
 
708
<p>There are three types of options you can set in the input:
 
709
</p>
 
710
<dl compact="compact">
 
711
<dt> <code>set_flag(&lt;flag&gt;,&lt;value&gt;).</code></dt>
 
712
<dd><p>Sets a flag to a value. Valid flags and values are described
 
713
in the OPTIONS section.
 
714
</p></dd>
 
715
<dt> <code>set_precedence(&lt;comma-separated list of function and/or predicate symbols&gt;).</code></dt>
 
716
<dd><p>Sets the precedence for the listed symbols. The precedence is
 
717
decreasing from left to right, i.e. the leftmost symbol has
 
718
the highest precedence.
 
719
</p>
 
720
<p>Every entry in the list has the form
 
721
</p><table><tr><td>&nbsp;</td><td><pre class="example">SYMBOL | (SYMBOL, WEIGHT [, {l, r, m}])
 
722
</pre></td></tr></table>
 
723
<p>You can use the second form to assign weights to symbols (for KBO) or a
 
724
status (for RPOS). Status is either <tt>l</tt> for left-to-right, <tt>m</tt> for
 
725
multiset, or <tt>r</tt> for right-to-left. Weight is given as an integer.
 
726
</p>
 
727
</dd>
 
728
<dt> <code>set_DomPred(&lt;comma-separated list of predicate symbols&gt;).</code></dt>
 
729
<dd><p>Listed predicate (<em>DomPred</em> for dominant predicate) symbols are
 
730
first ordered according to their precedence, not according to
 
731
their argument lists. Only in case of equal predicates, the
 
732
arguments are examined. For example, if we add the option
 
733
</p><table><tr><td>&nbsp;</td><td><pre class="example">set_DomPred(P).
 
734
</pre></td></tr></table>
 
735
<p>then in the clause
 
736
</p><table><tr><td>&nbsp;</td><td><pre class="example"> -&gt; R(f(x,y),a), P(x,a).
 
737
</pre></td></tr></table>
 
738
<p>the atom <i>P(x,a)</i> is strictly maximal.
 
739
Predicates listed by the <i>set_DomPred</i> option are
 
740
compared according to the precedence.
 
741
</p>
 
742
</dd>
 
743
<dt> <code>set_selection(&lt;comma-separated list of predicate symbols&gt;).</code></dt>
 
744
<dd><p>Sets the selection list that can be employed by the Select flag (see above).
 
745
</p>
 
746
</dd>
 
747
<dt> <code>set_ClauseFormulaRelation(&lt;comma separated list auf tuples (&lt;clause number&gt;, sequence of axiom name strings)).</code></dt>
 
748
<dd><p>This list is in particular set by FLOTTER and enables SPASS for an eventually found proof to show
 
749
the relation between the clauses used in the proof and the input formulas.
 
750
If combined with option DocProof, then there needs to be an entry for every clause number.
 
751
Otherwise an error is reported.
 
752
</p><table><tr><td>&nbsp;</td><td><pre class="example">set_ClauseFormulaRelation((1,ax2),(2,ax1),(3,ax3,ax1)).
 
753
</pre></td></tr></table>
 
754
 
 
755
</dd>
 
756
</dl>
 
757
 
 
758
<hr size="6">
 
759
<a name="SEC7"></a>
 
760
<h2 class="section"> 1.6 EXAMPLES </h2>
 
761
<p>To run SPASS on a single file without options:
 
762
</p><table><tr><td>&nbsp;</td><td><pre class="example">SPASS  <i>filename</i>
 
763
</pre></td></tr></table>
 
764
<p>To disable all SPASS output except for the final result:
 
765
</p><table><tr><td>&nbsp;</td><td><pre class="example">SPASS  -PGiven=0 -PProblem=0 <i>filename</i>
 
766
</pre></td></tr></table>
 
767
 
 
768
<hr size="6">
 
769
<a name="SEC8"></a>
 
770
<h2 class="section"> 1.7 AUTHORS </h2>
 
771
<p>Contact : spass@mpi-inf.mpg.de
 
772
</p>
 
773
 
 
774
<hr size="6">
 
775
<a name="SEC9"></a>
 
776
<h2 class="section"> 1.8 SEE ALSO </h2>
 
777
<p>checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1), tpget(1), deprose(1), dfg2otter(1), dfg2otterpl(1), dfg2dfg(1)
 
778
</p>
 
779
 
 
780
 
 
781
 
 
782
<hr size="6">
 
783
<table cellpadding="1" cellspacing="1" border="0">
 
784
<tr><td valign="middle" align="left">[<a href="#SEC1" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
 
785
<td valign="middle" align="left">[<a href="script_2.html#SEC10" title="Next chapter"> &gt;&gt; </a>]</td>
 
786
<td valign="middle" align="left"> &nbsp; </td>
 
787
<td valign="middle" align="left"> &nbsp; </td>
 
788
<td valign="middle" align="left"> &nbsp; </td>
 
789
<td valign="middle" align="left"> &nbsp; </td>
 
790
<td valign="middle" align="left"> &nbsp; </td>
 
791
<td valign="middle" align="left">[<a href="script.html#Top" title="Cover (top) of document">Top</a>]</td>
 
792
<td valign="middle" align="left">[Contents]</td>
 
793
<td valign="middle" align="left">[Index]</td>
 
794
<td valign="middle" align="left">[<a href="script_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
 
795
</tr></table>
 
796
<p>
 
797
 <font size="-1">
 
798
  This document was generated by <em>Christoph Weidenbach</em> on <em>February, 23 2010</em> using <a href="http://www.nongnu.org/texi2html/"><em>texi2html 1.78</em></a>.
 
799
 </font>
 
800
 <br>
 
801
 
 
802
</p>
 
803
</body>
 
804
</html>