« back to all changes in this revision
Viewing changes to doc/texinfo/script.info
- browse files at revision 5
- compare with another revision
- download diff
- download tarball
- view history from revision 5
- Committer: Bazaar Package Importer
- Author(s): Roland Stigge
- Date: 2010-06-29 22:04:02 UTC
- Revision ID: james.westby@ubuntu.com-20100629220402-o813i7ey64facu7i
Tags: 3.7-2
* Remove debian patches to broken texinfo files until fixed upstream
* debian/control: Standards-Version: 3.9.0
* debian/control: Standards-Version: 3.9.0
- files removed:
- .pc
- .pc/debian-changes-3.7-1
- .pc/debian-changes-3.7-1/doc
- .pc/debian-changes-3.7-1/doc/man
- .pc/debian-changes-3.7-1/doc/texinfo
- debian/patches
- files modified:
- debian/changelog
added
removed
doc/texinfo/script.info
1
This is doc/texinfo/script.info, produced by makeinfo version 4.13 from ./doc/texinfo/script.texi.
1
This is doc/texinfo/script.info, produced by makeinfo version 4.11 from ./doc/texinfo/script.texi.
2
2
3
3
4
4
File: script.info, Node: Top, Up: (dir)
5
5
6
* Menu:
7
8
* SPASS:: describes SPASS
9
* checkstat:: describes the checkstat script
10
* filestat:: describes the filestat script
11
* pcs:: describes the pcs script
12
* pgen:: describes the pgen script
13
* rescmp:: describes the rescmp script
14
* tpform:: describes the tpform script
15
* tpget:: describes the tpget script
16
* deprose:: describes the deprose script
17
* dfg2ascii:: describes the dfg2ascii program
18
* dfg2otter:: describes dfg2otter.pl
19
* dfg2otter.pl:: describes dfg2otter.pl
20
* dfg2dfg:: describes the dfg2dfg program
21
* dfg2tptp:: describes the dfg2tptp program
22
* tptp2dfg:: describes the tptp2dfg program
23
* daVinci and VCG:: daVinci and VCG
24
* spassfaq:: frequently asked questions about SPASS
25
26
27
File: script.info, Node: SPASS, Next: checkstat, Prev: Top, Up: Top
28
29
1 SPASS
30
*******
31
32
1.1 NAME
33
========
34
35
SPASS - an automated theorem prover for full first-order logic with
36
equality
37
38
1.2 SYNOPSIS
39
============
40
41
SPASS [`options'] [INPUTFILE]
42
43
1.3 DESCRIPTION
44
===============
45
46
SPASS is an automated theorem prover for full sorted first-order logic
47
with equality that extends superposition by sorts and a splitting rule
48
for case analysis. SPASS can also be used as a modal logic and
49
description logic theorem prover.
50
51
1.4 OPTIONS
52
===========
53
54
Command line options in SPASS are implemented via modifications to the
55
GNU command line option package for C. Just giving the option sets its
56
value to 1 and means enabling the option. In order to disable an option
57
the value has to be set to 0 by declaring -Option=0. The following
58
options are currently supported by SPASS:
59
60
`-Auto'
61
Enables/disables the auto mode where SPASS configures itself
62
automatically. The inference/reduction rules, the sort
63
technology, the ordering and precedence as well as the splitting
64
and selection strategy are set. In auto mode SPASS is complete.
65
Mixing the auto mode with user defined options may destroy
66
completeness. Default is 1.
67
68
`-Stdin'
69
Enables/disables input in SPASS via stdin. The file argument is
70
ignored. Default is 0.
71
72
`-Interactive'
73
Enables/disables the interactive mode. First, SPASS is given a set
74
of axioms and then the prover accepts subsequent proof tasks.
75
Default is 0.
76
77
`-Flotter'
78
Enables/disables the CNF translation mode of SPASS. If the option
79
is set, SPASS only performs a clause normal form translation. If
80
no output file argument is given SPASS prints the CNF to stdout.
81
Default is 0.
82
83
`-SOS'
84
Enables/disables the set of support strategy. Default is 0.
85
86
`-Splits=n'
87
Sets the number of possible splitting applications to n. If n=-1
88
then the number of splits is not limited. Default is 0.
89
90
`-Memory=n'
91
Sets the amount of memory available to SPASS for the proof search
92
to n bytes. The memory needed to startup SPASS cannot be
93
restricted. Default is -1 meaning that memory allocations is only
94
restricted by available memory.
95
96
`-TimeLimit=n'
97
Sets a time limit for the proof search to n seconds. Default is -1
98
meaning that SPASS may run forever. The time limit is polled when
99
SPASS selects a new clause for inferences. If a single inference
100
step causes an explosion to the number of generated clauses it may
101
therefore happen that a given time limit is significantly exceeded.
102
103
`-DocSST'
104
Enables/disables documentation output for static soft typing. The
105
used sort theory as well as the (failed) proof attempt for the
106
sort constraint is printed. Default is 0.
107
108
`-DocProof'
109
Enables/disables proof documentation. If SPASS finds a proof it is
110
eventually printed. If SPASS finds a saturation, the saturated set
111
of clauses is eventually printed. Enabling proof documentation
112
may significantly decrease SPASS's performance, because the prover
113
must store clauses that can be thrown away otherwise. Default is 0.
114
115
`-DocSplit'
116
Sets the documentation of split backtracking steps. If set to 1,
117
the current backtracking level is printed. If set to 2, it also
118
prints in case of a split backtrack the backtracked clauese.
119
Default is 0.
120
121
`-Loops'
122
Sets the maximal number of mainloop iterations for SPASS. Default
123
is -1.
124
125
`-PSub'
126
Enables/disables printing of subsumed clauses. Default is 0.
127
128
`-PRew'
129
Enables/disables printing of simple rewrite applications. Default
130
is 0.
131
132
`-PCon'
133
Enables/disables printing of condensation applications. Default
134
is 0.
135
136
`-PTaut'
137
Enables/disables printing of tautology deletion applications.
138
Default is 0.
139
140
`-PObv'
141
Enables/disables printing of obvious reduction applications.
142
Default is 0.
143
144
`-PSSi'
145
Enables/disables printing of sort simplification applications.
146
Default is 0.
147
148
`-PSST'
149
Enables/disables printing of static soft typing applications. All
150
deleted clauses are printed. Default is 0.
151
152
`-PMRR'
153
Enables/disables printing of matching replacement resolution
154
applications. Default is 0.
155
156
`-PUnC'
157
Enables/disables printing of unit conflict applications. Default
158
is 0.
159
160
`-PAED'
161
Enables/disables printing of clauses where redundant equations
162
have been removed (assignment equation deletion).
163
164
`-PDer'
165
Enables/disables printing of clauses derived by inferences.
166
Default is 0.
167
168
`-PGiven'
169
Enables/disables printing of the given clause, selected to perform
170
inferences. Default is 0.
171
172
`-PLabels'
173
Enables/disables printing of labels. If the -DocProof is set and
174
no labels for formulae are provided by the input, SPASS generates
175
generic labels that are then printed by enabling this option.
176
Default is 0.
177
178
`-PKept'
179
Enables/disables printing of kept clauses. These are clauses
180
generated by inferences (backtracking) that are not redundant.
181
Clauses derived during input reduction/saturation are not printed.
182
Default is 0.
183
184
`-PProblem'
185
Enables/disables printing of the input clause set. Default is 1.
186
187
`-PEmptyClause'
188
Enables/disables printing of derived empty clauses. Default is 0.
189
190
`-PStatistic'
191
Enables/disables printing of a final statistics on
192
derived/backtracked/kept clauses, performed splits, used time and
193
used space. Default is 1.
194
195
`-FPModel'
196
Enables/disables the output of an eventually found model to a
197
file. If set to 1, all clauses in the final set are printed. If
198
set to 2, only potentially productive clauses are printed, that
199
are clauses with no selected negative literal and a maximal
200
positive one. If <problemfile> is the name of the input problem
201
and the eventually generated set is saturated, the saturation is
202
printed to the file <problemfile>.model, for otherwise to
203
<problemfile>.clauses. The latter case may, e.g., be caused by a
204
time limit. Default is 0.
205
206
`-FPDFGProof'
207
Enables/disables the output of an eventually found proof to a
208
file. Using this option requires to set the option -DocProof. If
209
<problemfile> is the name of the input problem the proof is
210
printed to <problemfile>.prf. Default is 0.
211
212
`-PFlags'
213
Enables/disables the output of all flag values. The flag settings
214
are printed at the end of a SPASS run in form of a DFG-Syntax
215
input section. Default is 0.
216
217
`-POptSkolem'
218
Enables/disables the output of optimized Skolemization
219
applications. Default is 0.
220
221
`-PStrSkolem'
222
Enables/disables the output of strong Skolemization applications.
223
Default is 0.
224
225
`-PBDC'
226
Enables/disables the output of clauses deleted because of bound
227
restrictions. Default is 0.
228
229
`-PBInc'
230
Enables/disables the output of bound restriction changes. Default
231
is 0.
232
233
`-PApplyDefs'
234
Enables/disables printing of expansions of atom definitions.
235
Default is 0.
236
237
`-Select'
238
Sets the selection strategy for SPASS. If set to 0 no selection of
239
negative literals is done. If set to any other value, at most one
240
negative literal in a clause is selected. If set to 1 negative
241
literals in clauses with more than one maximal literal are
242
selected. Either a negative literal with a predicate from the
243
selection list (see below) is chosen or if no such negative
244
literal is available, a negative literal with maximal weight is
245
chosen. If set to 2 negative literals are always selected. Again,
246
either a negative literal with a predicate from the selection list
247
(see below) is chosen or if no such negative literal is available,
248
a negative literal with maximal weight is chosen. The latter case
249
results in an ordered hyperresolution like behavior of ordered
250
resolution. If set to 3 any negative literal with a predicate
251
specified by the selection list (see below) is selected. Default
252
is 1.
253
254
`-RInput'
255
Enables/disables the reduction of the initial clause set. Default
256
is 1.
257
258
`-Sorts'
259
Determines the monadic literals that built the sort constraint for
260
the initial clause set. If set to 0, no sort constraint is built.
261
If set to 1, all negative monadic literals with a variable as
262
argument form the sort constraint. If set to 2, all negative
263
monadic literals form the sort constraint. Setting -Sorts to 2
264
may harm completeness, since sort constraints are subject to the
265
basic strategy and to static soft typing. Default is 1.
266
267
`-SatInput'
268
Enables/disables input saturation. The saturation is incomplete
269
but is guaranteed to terminate. Default is 0.
270
271
`-WDRatio'
272
Sets the ratio between given clauses selected by weight or the
273
depth in the search space. The weight is the sum of all symbol
274
weights determined by the -FuncWeight and -VarWeight options. The
275
depth of all initial clauses is 0 and clauses generated by
276
inferences get the maximal depth of a parent clause plus 1.
277
Default is 5, meaning that 4 clauses are selected by weight and
278
the fifth clause is selected by depth.
279
280
`-PrefCon'
281
Sets the ratio to compute the weight for conjecture clauses and
282
therefore allows to prefer those. Default is 0 meaning that the
283
weight computation for conjecture clauses is not changed.
284
285
`-FullRed'
286
Enables/disables full reduction. If set to 0, only the set of
287
worked off clauses is completely inter-reduced. If set to 1, all
288
currently hold clauses (worked off and usable) are completely
289
inter-reduced. Default is 1.
290
291
`-FuncWeight'
292
Sets the weight of function/predicate symbols. The weight of
293
clauses is the sum of all symbol weights. This weight is considered
294
for the selection of the given clause. Default is 1.
295
296
`-VarWeight'
297
Sets the weight of variable symbols (see -FuncWeight). Default is
298
1.
299
300
`-PrefVar'
301
Enables/disables the preference for clauses with many variables.
302
While clauses are selected by weight, if this option is set and
303
two clauses have the same weight, the clause with more variable
304
occurrences is preferred. Default is 0.
305
306
`-BoundMode'
307
Selects the mode for bound restrictions. Mode 0 means no
308
restriction, if set to 1 all newly generated clauses are
309
restricted by weight (see -BoundStart) and if set to 2 clauses are
310
restricted by depth. Default is 0.
311
312
`-BoundStart'
313
The start restriction of the selected bound mode. For example, if
314
bound mode is 1 and bound start set to 5, all clauses with a
315
weight larger than 5 are deleted until the set is saturated. This
316
causes an increase of the used bound value that is determined by
317
the minimal increase saving a before deleted clause. Default is -1
318
meaning no bound restriction.
319
320
`-BoundLoops'
321
The number of loops applying the actions restrictions/increasing
322
bound. If the number of loops is exceeded all bound restrictions
323
are cancelled. Default is 1.
324
325
`-ApplyDefs'
326
Sets the maximal number of applications of atom definitions to
327
input formulae. Default is 0, meaning no applications at all.
328
329
`-Ordering'
330
Sets the term ordering. If 0 then KBO is selected, if 1 the RPOS
331
is selected. Default is 0.
332
333
`-CNFQuantExch'
334
If set, non-constant Skolem terms in the clausal form of the
335
conjecture are replaced by constants. Will automatically be set
336
for the optimized functional translation of modal or description
337
logic formulae. Default is 0.
338
339
`-CNFOptSkolem'
340
Enables/disables optimized Skolemization. Default is 1.
341
342
`-CNFStrSkolem'
343
Enables/disables Strong Skolemization. Default is 1.
344
345
`-CNFProofSteps'
346
Sets the maximal number of proof steps in an optimized
347
Skolemization proof attempt. Default is 100.
348
349
`-CNFSub'
350
Enables/disables subsumption on the clauses generated by the CNF
351
procedure. Default is 1.
352
353
`-CNFCon'
354
Enables/disables condensing on the clauses generated by the CNF
355
procedure. Default is 1.
356
357
`-CNFRedTime'
358
Sets the overall amount of time in seconds to be spend on
359
reduction during CNF transformation. Affected reductions are
360
optimized Skolemization, condensing, and subsumption. Default is
361
-1 meaning that the reduction time is not limited at all.
362
363
`-CNFRenaming'
364
Enables/disables formula renaming. If set to 1 optimized renaming
365
is enabled that minimizes the number of eventually generated
366
clauses. If set to 2 complex renaming is enabled that introduces a
367
new Skolem predicate for every complex formula, i.e., any formula
368
that is not a literal. If set to 3 quantification renaming is
369
enabled that introduces a new Skolem predicate for every
370
subformula starting with a quantifier. Default is 1.
371
372
`-CNFRenMatch'
373
If set, renaming variant subformulae are replaced by the same
374
Skolem literal. Default is 1.
375
376
`-CNFPRenaming'
377
Enables/disables the printing of formula renaming applications.
378
Default is 0.
379
380
`-CNFFEqR'
381
Enables/disables certain equality reduction techniques on the
382
formula level. Default is 1.
383
384
`-IEmS'
385
Enables/disables the inference rule Empty Sort. Default is 0.
386
387
`-ISoR'
388
Enables/disables the inference rule Sort Resolution. Default is 0.
389
390
`-IEqR'
391
Enables/disables the inference rule Equality Resolution. Default
392
is 0.
393
394
`-IERR'
395
Enables/disables the inference rule Reflexivity Resolution.
396
Default is 0.
397
398
`-IEqF'
399
Enables/disables the inference rule Equality Factoring. Default
400
is 0.
401
402
`-IMPm'
403
Enables/disables the inference rule Merging Paramodulation.
404
Default is 0.
405
406
`-ISpR'
407
Enables/disables the inference rule Superposition Right. Default
408
is 0.
409
410
`-IOPm'
411
Enables/disables the inference rule Ordered Paramodulation.
412
Default is 0.
413
414
`-ISPm'
415
Enables/disables the inference rule Standard Paramodulation.
416
Default is 0.
417
418
`-ISpL'
419
Enables/disables the inference rule Superposition Left. Default
420
is 0.
421
422
`-IORe'
423
Enables/disables the inference rule Ordered Resolution. If set to
424
1, Ordered Resolution is enabled but no resolution inferences with
425
equations are generated. If set to 2, equations are considered for
426
Ordered Resolution steps as well. Default is 0.
427
428
`-ISRe'
429
Enables/disables the inference rule Standard Resolution. If set
430
to 1, Standard Resolution is enabled but no resolution inferences
431
with equations are generated. If set to 2, equations are
432
considered for Standard Resolution steps as well. Default is 0.
433
434
`-ISHy'
435
Enables/disables the inference rule Standard Hyper-Resolution.
436
Default is 0.
437
438
`-IOHy'
439
Enables/disables the inference rule Ordered Hyper-Resolution.
440
Default is 0.
441
442
`-IURR'
443
Enables/disables the inference rule Unit Resulting Resolution.
444
Default is 0.
445
446
`-IOFc'
447
Enables/disables the inference rule Ordered Factoring. If set to
448
1, Ordered Factoring is enabled but only factoring inferences with
449
positive literals are generated. If set to 2, negative literals
450
are considered for inferences as well. Default is 0.
451
452
`-ISFc'
453
Enables/disables the inference rule Standard Factoring. Default
454
is 0.
455
456
`-IUnR'
457
Enables/disables the inference rule Unit Resolution. Default is 0.
458
459
`-IBUR'
460
Enables/disables the inference rule Bounded Depth Unit Resolution.
461
Default is 0.
462
463
`-IDEF'
464
Enables/disables the inference rule Apply Definitions. Currently
465
not supported. Default is 0.
466
467
`-RFRew'
468
Enables/disables the reduction rule Forward Rewriting. If set to
469
1 unit rewriting and non-unit rewriting based on a subsumption
470
test is activated. If set to 2 in addition to unit and non-unit
471
rewriting local contextual rewriting is activated. If set to 3 in
472
addition to unit and non-unit rewriting subterm contextual
473
rewriting is activiated. Subterm contextual rewriting subsumes
474
local contextual rewriting. If set to 4 in addition of the
475
rewriting rules of 3, subterm contextual rewriting also tests for
476
negative literal elimination. Default is 0.
477
478
`-RBRew'
479
Enables/disables the reduction rule Backward Rewriting. Same
480
values and meaning as for flag -RFRew but used in backward
481
direction. Default is 0.
482
483
`-RFMRR'
484
Enables/disables the reduction rule Forward Matching Replacement
485
Resolution. Default is 0.
486
487
`-RBMRR'
488
Enables/disables the reduction rule Backward Matching Replacement
489
Resolution. Default is 0.
490
491
`-RObv'
492
Enables/disables the reduction rule Obvious Reduction. Default is
493
0.
494
495
`-RUnC'
496
Enables/disables the reduction rule Unit Conflict. Default is 0.
497
498
`-RTer'
499
Enables/disables the terminator by setting the maximal number of
500
non-unit clauses to be used during the search. Default is 0.
501
502
`-RTaut'
503
Enables/disables the reduction rule Tautology Deletion. If set to
504
1, only syntactic tautologies are detected and deleted. If set to
505
2, additionally semantic tautologies are removed. Default is 0.
506
507
`-RSST'
508
Enables/disables the reduction rule Static Soft Typing. Default
509
is 0.
510
511
`-RSSi'
512
Enables/disables the reduction rule Sort Simplification. Default
513
is 0.
514
515
`-RFSub'
516
Enables/disables the reduction rule Forward Subsumption Deletion.
517
Default is 0.
518
519
`-RBSub'
520
Enables/disables the reduction rule Backward Subsumption Deletion.
521
Default is 0.
522
523
`-RAED'
524
Enables/disables the reduction rule Assignment Equation Deletion.
525
This rule removes particular occurrences of equations from clauses.
526
If set to 1, the reduction is guaranteed to be sound. If set to
527
2, the reduction is only sound if any potential model of the
528
considered problem has a non-trivial domain. Default is 0.
529
530
`-RCon'
531
Enables/disables the reduction rule Condensation. Default is 0.
532
533
`-TDfg2OtterOptions'
534
Enables/disables the inclusion of an Otter options header. This
535
option only applies to dfg2otter. If set to 1 it includes a
536
setting that makes Otter nearly complete. If set to 2 it activates
537
auto modus and if set to 3 it activates the auto2 modus. Default
538
is 0.
539
540
`-EML'
541
A special EML flag for modal logic or description logic formulae.
542
Never needs to be set explicitly. Is set during parsing.
543
544
`-EMLAuto'
545
Intended for EML Autonomous mode, as yet not functional. Default
546
is 0.
547
548
`-EMLTranslation'
549
Determines the translation method used for modal logic or
550
description logic formulae. If set to 0, the standard relational
551
translation method (which is determined by the usual Kripke
552
semantics) is used. If set to 1, the functional translation
553
method is used. If set to 2, the optimised functional translation
554
method is used. If set to 3, the semi-functional translation
555
method is used. A variation of the optimised functional
556
translation method is used, when the following settings are
557
specified: -EMLTranslation=2 -EMLFuncNary=1. The translation will
558
be in terms of n-ary predicates instead of unary predicates and
559
paths. In the current implementation the standard relational
560
translation method is most general. Some restrictions apply to the
561
other methods. The functional translation method and
562
semi-functional translation methods are available only for the
563
basic multi-modal logic K(m) possibly with serial (total)
564
modalities (-EMLTheory=1), plus nominals (ABox statements),
565
terminological axioms and general inclusion and equivalence
566
axioms. The optimised functional translation methods are
567
implemented only for K(m), possibly with serial modalities.
568
Default is 0.
569
570
`-EML2Rel'
571
If set, propositional/Boolean-type formulae are converted to
572
relational formulae before they are translated to first-order
573
logic. Default is 0.
574
575
`-EMLTheory'
576
Determines which background theory is assumed. If set to 0, the
577
background theory is empty. If set to 1, then seriality (the
578
background theory for KD) is added for all modalities. If set to
579
2, then reflexivity (the background theory for KT) is added for
580
all modalities. If set to 3, then symmetry (the background theory
581
for KB) is added for all modalities. If set to 4, then
582
transitivity (the background theory for K4) is added for all
583
modalities. If set to 5, then Euclideanness (the background
584
theory for K5) is added for all modalities. If set to 6, then
585
transitivity and Euclideanness (the background theory for S4) is
586
added for all modalities. If set to 7, then reflexivity,
587
transitivity and Euclideanness (the background theory for S5) is
588
added for all modalities. Default is 0.
589
590
`-EMLFuncNdeQ'
591
If set, diamond formulae are translated according to
592
tr(dia(phi),s) = nde(s) /\ exists x tr(phi,[s x]) (a nde /
593
quantifier formula), otherwise the translation is in accordance
594
with tr(dia(phi),s) = exists x nde(s) /\ tr(phi,[s x]) (a
595
quantifier / nde formula). The transltion for box formulae is
596
defined dually. Setting this flag is only meaningful when the
597
flag for the functional or semi functional translation method is
598
set. Default is 1.
599
600
`-EMLFuncNary'
601
If set, the functional translation into fluted logic is used.
602
This means n-ary predicate symbols are used instead of unary
603
predicate symbols and paths. Setting this flag is only meaningful
604
for testing local satisfiability/validity in multi-modal K.
605
Default is 0.
606
607
`-EMLFFSorts'
608
If set, sorts for terms are used. Default is 0.
609
610
`-EMLElimComp'
611
If set, try to eliminate relational composition in modal
612
parameters. Default is 0.
613
614
`-EMLPTrans'
615
If set, the EML to first-order logic translation is documented.
616
Default is 0.
617
618
`-TPTP'
619
If set, SPASS expects an input file in TPTP syntax. Default is 0.
620
621
`-rf'
622
If set, SPASS deletes the input file before termination. Default
623
is 0.
624
625
1.5 SETTINGS
626
============
627
628
You can also specify options for SPASS in the input problem. In the
629
DFG syntax, you would use
630
list_of_settings(SPASS).
631
{*
632
set_flag(DocProof,1).
633
*}
634
end_of_list.
635
to set the DocProof flag.
636
637
There are three types of options you can set in the input:
638
639
`set_flag(<flag>,<value>).'
640
Sets a flag to a value. Valid flags and values are described in
641
the OPTIONS section.
642
643
`set_precedence(<comma-separated list of function and/or predicate symbols>).'
644
Sets the precedence for the listed symbols. The precedence is
645
decreasing from left to right, i.e. the leftmost symbol has the
646
highest precedence.
647
648
Every entry in the list has the form
649
SYMBOL | (SYMBOL, WEIGHT [, {l, r, m}])
650
You can use the second form to assign weights to symbols (for KBO)
651
or a status (for RPOS). Status is either l for left-to-right, m for
652
multiset, or r for right-to-left. Weight is given as an integer.
653
654
`set_DomPred(<comma-separated list of predicate symbols>).'
655
Listed predicate (_DomPred_ for dominant predicate) symbols are
656
first ordered according to their precedence, not according to
657
their argument lists. Only in case of equal predicates, the
658
arguments are examined. For example, if we add the option
659
set_DomPred(P).
660
then in the clause
661
-> R(f(x,y),a), P(x,a).
662
the atom P(x,a) is strictly maximal. Predicates listed by the
663
set_DomPred option are compared according to the precedence.
664
665
`set_selection(<comma-separated list of predicate symbols>).'
666
Sets the selection list that can be employed by the Select flag
667
(see above).
668
669
`set_ClauseFormulaRelation(<comma separated list auf tuples (<clause number>, sequence of axiom name strings)).'
670
This list is in particular set by FLOTTER and enables SPASS for an
671
eventually found proof to show the relation between the clauses
672
used in the proof and the input formulas. If combined with option
673
DocProof, then there needs to be an entry for every clause number.
674
Otherwise an error is reported.
675
set_ClauseFormulaRelation((1,ax2),(2,ax1),(3,ax3,ax1)).
676
677
678
1.6 EXAMPLES
679
============
680
681
To run SPASS on a single file without options:
682
SPASS filename
683
To disable all SPASS output except for the final result:
684
SPASS -PGiven=0 -PProblem=0 filename
685
686
1.7 AUTHORS
687
===========
688
689
Contact : spass@mpi-inf.mpg.de
690
691
1.8 SEE ALSO
692
============
693
694
checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1),
695
tpget(1), deprose(1), dfg2otter(1), dfg2otterpl(1), dfg2dfg(1)
696
697
698
File: script.info, Node: checkstat, Next: filestat, Prev: SPASS, Up: Top
699
700
2 checkstat
701
***********
702
703
2.1 NAME
704
========
705
706
checkstat - checks SPASS behavior on problem files
707
708
2.2 SYNOPSIS
709
============
710
711
*checkstat* [`-cdFiklmopPrstTuvVwx'] DIR_1/FILE_1 ... DIR_N/FILE_N
712
713
2.3 DESCRIPTION
714
===============
715
716
The *checkstat* script is intended for automatically checking the
717
declared state of a theorem proving problem, specified in *DFG*
718
syntax, against the state computed by the *SPASS* theorem prover. The
719
script is written in *Perl*.
720
721
For using the proof and model checking facilities, the *pcs* and
722
*rescmp* programs must exist in the same directory as *checkstat*, or
723
the corresponding environment variables *PCS* and *RESCMP* must be set
724
to their paths.
725
726
*checkstat* examines the set of files that is given by all specified
727
files and all files in the specified directories that have a '.cnf',
728
'.frm', or '.dfg' extension. *checkstat* evokes *SPASS* on each file
729
and compares its result with the problem state specified in the
730
'status' field of the *DFG* problem description. Optionally (see
731
below), *SPASS* proofs can be verified by a proof checker, and *SPASS*
732
completions can be checked against reference completions. If *SPASS*
733
outputs memory check information in the format produced by the 'CHECK'
734
compile time variable, then *checkstat* verifies that all memory has
735
been cleaned up at the end of the *SPASS* run.
736
737
*checkstat* continues as long as no critical events occur, which are
738
(besides standard system errors, e.g. in file access):
739
740
* A problem state is declared satisfiable (unsatisfiable), and
741
*SPASS* computes unsatisfiable (satisfiable).
742
743
* *SPASS* returns an invalid proof (only if proof checking is
744
enabled).
745
746
* The *SPASS* completion and the reference completion differ (if
747
completion checking is enabled, and a reference file is present).
748
749
* *SPASS* reports that not all memory has been cleaned up.
750
751
* *SPASS* memory use reporting is inconsistent: Either *SPASS*
752
gives memory use information for the current file, but has not
753
given it for the previous files, or vice versa, gives no memory
754
information for the current file, but has done this for previous
755
files.
756
757
* The problem state could not be extracted from the problem file.
758
759
* No problem state could be extracted from the *SPASS* output, for
760
example due to a segmentation fault.
761
762
These errors are reported, and *checkstat* stops. All other possible
763
events are classified as uncritical. They are fully reported in the
764
moment of their occurrence only if the *-v* option has been activated.
765
Their occurrence is always mentioned in a final event statistic, but
766
not with the associated problem files. Uncritical events are:
767
* *SPASS* runs out of time or out of memory.
768
769
* *SPASS* decides a problem whose state is declared 'unknown'.
770
If a file 'filename.dfg' is in the set of specified files, and there
771
exists corresponding corresponding '.cnf' file 'filename.cnf' in the
772
same directory, then this file is passed to *SPASS*, even if it is not
773
a parameter to *checkstat*. I.e.,
774
*checkstat* test.dfg
775
passes the file 'test.cnf' to *SPASS* if it exists in the current
776
working directory.
777
778
2.4 OPTIONS
779
===========
780
781
The following options are supported by *checkstat*:
782
783
`-v'
784
Verbose mode. Prints information on the currently checked
785
directory, file, and uncritical events. Default is 'off'.
786
787
`-V'
788
Very verbose mode. Enables verbose mode, and prints output of
789
proof checker *pcs*.
790
791
`-p prover'
792
Specify prover. Can be used for setting *SPASS* options, see
793
examples below. Default is value of the environment variable
794
'SPASS'.
795
796
`-t limit'
797
Specify a time limit for *SPASS* (in seconds). Default is 10
798
seconds.
799
800
`-c'
801
Specify time limit for proof checker *pcs*.
802
803
`-l'
804
Log *SPASS* result for each file 'filename.cnf' in 'filename.log'.
805
Default is 'off'. This option is to be used with care, as a *Perl*
806
variable with the same size as the *SPASS* output is created in
807
the memory.
808
809
`-u'
810
Check *SPASS* proofs for correctness ('u' for 'unsatisfiable').
811
812
`-s'
813
Check *SPASS* completions against reference completions. The
814
reference completion corresponding to a problem file filename
815
.ext', where ext is some *DFG* file extension, is 'filename.mod'
816
and must be located in the same directory as the problem file.
817
('s' is for 'satisfiable).
818
819
`-r'
820
Run. Continue after errors.
821
822
`-w'
823
Print warning if model checking is enabled, a model has been found,
824
but the reference does not exist.
825
826
`-P'
827
Specify *SPASS* options. Enclose in single quotes to protect from
828
shell please.
829
830
`-T limit'
831
Enable timing by shell. Stops in time even if *SPASS* timing does
832
not work.
833
834
`-c limit'
835
Specify time limit in seconds for proof checker. This is the time
836
available for verifying one proof step in a proof.
837
838
`-d'
839
Debug. Lots of output about intermediate results etc.
840
841
`-k'
842
Keep. Keep generated temporary files.
843
844
`-o'
845
Use *SPASS* instead of OTTER for proof checking.
846
847
`-x'
848
Extension. Process all file parameters, regardless of extension.
849
Normally, files with unknown extensions are ignored.
850
851
`-i'
852
Interactive. Reads file names from standard input.
853
854
`-m'
855
Mode. Print out command line.
856
857
2.5 EXAMPLES
858
============
859
860
To check a single file with some extra *SPASS* options:
861
*checkstat* -p 'SPASS options' filename
862
To check all files with '.cnf' suffix in directory 'Test':
863
*checkstat* Test/*.cnf
864
865
2.6 AUTHORS
866
===========
867
868
Thorsten Engel and Christian Theobalt
869
870
Contact : spass@mpi-inf.mpg.de
871
872
2.7 SEE ALSO
873
============
874
875
filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1), tpget(1),
876
deprose(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)
877
878
879
File: script.info, Node: filestat, Next: pcs, Prev: checkstat, Up: Top
880
881
3 filestat
882
**********
883
884
3.1 NAME
885
========
886
887
filestat - compares SPASS results with status in problem files
888
889
3.2 SYNOPSIS
890
============
891
892
*filestat* [ -vc] file_1 ... file_n
893
894
3.3 DESCRIPTION
895
===============
896
897
Like *checkstat*, *filestat* is a script for automatically comparing a
898
set of *SPASS* results against reference results. Unlike *checkstat*,
899
*SPASS* is not actually run on the problems. Instead, input to
900
*filestat* are *SPASS* result files, which contain concatenations of
901
*SPASS* outputs, describing the input file and the result. *filestat*
902
compares the problem status in each of these input files with the
903
problem status computed by *SPASS* and outputs differences.
904
905
3.4 OPTIONS
906
===========
907
908
The following options are supported by *filestat*:
909
`-c'
910
Continue after status differences. Default: 'Off'.
911
912
`-v'
913
Report in detail. Especially, print out which *SPASS* result file
914
is currently processed. Default: 'Off'.
915
916
3.5 AUTHORS
917
===========
918
919
Thorsten Engel and Christian Theobalt
920
921
Contact : spass@mpi-inf.mpg.de
922
923
3.6 SEE ALSO
924
============
925
926
checkstat(1), pcs(1), pgen(1), rescmp(1), tpform(1), tpget(1),
927
deprose(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)
928
929
930
File: script.info, Node: pcs, Next: pgen, Prev: filestat, Up: Top
931
932
4 pcs
933
*****
934
935
4.1 NAME
936
========
937
938
pcs - checks SPASS proofs
939
940
4.2 SYNOPSIS
941
============
942
943
*pcs* [ -cdfrstv] file
944
945
4.3 DESCRIPTION
946
===============
947
948
*pcs* is a Perl script that supports automatic checking of proofs
949
specified in *DFG* syntax with the theorem prover OTTER. It uses
950
* the C-program *pgen*, which generates proof tasks corresponding to
951
inference steps for each proof step of a *DFG* proof and checks
952
the tableau structure.
953
954
* the C-program *SPASS* with the -Flotter option for converting
955
*DFG* syntax files with formulas into *DFG* syntax files with
956
clauses.
957
958
* the C-program dfg2otter, which transforms files in *DFG* syntax
959
with clauses only into files for OTTER syntax.
960
*pcs* checks that:
961
* The conclusion in each proof step is a logical consequence of the
962
assumptions in that proof step.
963
964
* Each clause in a subtableau uses only parents clauses that are
965
visible at this point in the tableau.
966
967
* Each clause, except for split clauses, has the maximum split level
968
of its parents.
969
970
* If the first half of a split was ground, then negations of its
971
literals can be used in the tableau branch corresponding to the
972
second half of the split.
973
974
* The tableau is complete and closed.
975
The second condition is verified by checking the unsatisfiability
976
Assumptions \wedge \neg Conclusion
977
for each proof step (inference rule application) by running OTTER
978
for a limited time. The appropriate *DFG* files for these problems are
979
generated by *pgen*. OTTER may fail to terminate within this time,
980
leaving the correctness of a proof step undecided, which leads to the
981
three possible results of *pcs*:
982
* The proof is correct: Both conditions are satisfied for all proof
983
steps.
984
985
* The proof is not correct: One condition is definitely violated for
986
at least one proof step.
987
988
* Correctness is undecided: The first condition is satisfied, but
989
the second condition could not be verified nor falsified for at
990
least one proof step.
991
992
*pcs* uses a working directory, in which all proof tasks corresponding
993
to the proof steps are generated using the *pgen* program. These tasks
994
are subsequently checked using OTTER.
995
996
4.4 OPTIONS
997
===========
998
999
Several options control the behavior of *pcs* when it fails to verify a
1000
proof step, its output and the naming of generated files and the
1001
working directory:
1002
1003
`-c'
1004
Continue even if a single proof step could not be verified.
1005
Default 'off'.
1006
1007
`-d suffix'
1008
Suffix of created working directory. For an input file root.ext,
1009
the working directory <root><suffix> is created. If suffix does
1010
not end with a backslash, it is taken as a prefix for files
1011
generated by *pgen*, which are then created in the current working
1012
directory. Default is '_SubProofs/'.
1013
1014
`-f'
1015
Overwrite working directory if it already exists. Default 'off'.
1016
1017
`-o'
1018
Use *SPASS* as proof checker instead of OTTER. This option is
1019
especially useful when checking proofs generated by a different
1020
prover. Default is 'off'.
1021
1022
`-p path'
1023
Location of *DFG* prover to be used instead of the default one. If
1024
-o is specified, then it overrides this option, and *SPASS* is used
1025
instead. If a *DFG* converter is specified, then a prover must be
1026
specified as well. Default is OTTER.
1027
1028
`-q'
1029
Be quiet and do not print program paths. This option is especially
1030
useful inside *checkstat*. Default is 'off'.
1031
1032
`-r'
1033
Clean up all generated files at the end, even if the proof is not
1034
valid. Default 'off'.
1035
1036
`-s suffix'
1037
Suffix of files generated by *pgen*. Default is '.dfg'.
1038
1039
`-t limit'
1040
Number of seconds for each proof attempt for each proof step.
1041
Default is 3 seconds.
1042
1043
`-v'
1044
(verbose) Give some progress information. Default is 'off'.
1045
1046
`-w path'
1047
Location of *DFG* converter to be used instead of the default one.
1048
If a *DFG* converter is specified, then a prover must be specified
1049
as well. Default is *dfg2otter.pl*.
1050
1051
1052
4.5 AUTHORS
1053
===========
1054
1055
Thorsten Engel and Christian Theobalt.
1056
1057
Contact : spass@mpi-inf.mpg.de
1058
1059
4.6 SEE ALSO
1060
============
1061
1062
checkstat(1), filestat(1), pgen(1), rescmp(1), tpform(1), tpget(1),
1063
deprose(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)
1064
1065
1066
File: script.info, Node: pgen, Next: rescmp, Prev: pcs, Up: Top
1067
1068
5 pgen
1069
******
1070
1071
5.1 NAME
1072
========
1073
1074
pgen - generates single step proof obligations out of a DFG (SPASS)
1075
proof
1076
1077
5.2 SYNOPSIS
1078
============
1079
1080
*pgen* [ -dstqjnr] [-vinci -xvcg] filename
1081
1082
5.3 DESCRIPTION
1083
===============
1084
1085
� man begin DESCRIPTION *pgen* is a C-program that checks the tableau
1086
structure of SPASS tableau proofs and generates proof tasks
1087
corresponding to proof steps. Before the proof tasks are generated, the
1088
tableau is reduced in two steps:
1089
1. If an empty clause exists in a subtableau, all successors of the
1090
subtableau are deleted.
1091
1092
2. If a subtableau has a single successor subtableau, the successor
1093
is deleted.
1094
After the reduction, *pgen* checks that
1095
* Each clause in a subtableau uses only parents clauses that are
1096
visible at this point in the tableau.
1097
1098
* Each clause, except for split clauses, has the maximum split level
1099
of its parents.
1100
1101
* If the first half of a split was ground, then negations of its
1102
literals can be used in the tableau branch corresponding to the
1103
second half of the split.
1104
1105
* The tableau is complete and closed.
1106
1107
Generated filenames have the form <prefix><filename><suffix>, where
1108
suffix and prefix are specified by the *-d* and *-s* option.
1109
1110
*pgen* can generate graph representations of the tableau before and
1111
after the reduction using the *-n* and *-r* options. These
1112
representations can be written to a text file in either *daVinci* or
1113
*xvcg* format. See section *Note daVinci and VCG::, for these graph
1114
visualization programs.
1115
1116
5.4 OPTIONS
1117
===========
1118
1119
The following options are supported by *pgen*:
1120
`-j'
1121
Do not generate proof files.
1122
1123
`-q'
1124
Quiet mode.
1125
1126
`-d prefix'
1127
Prefix of generated files. The option name was chosen because the
1128
prefix is probably a directory.
1129
1130
`-t limit'
1131
Number of seconds for each proof attempt for each proof step.
1132
Default is 3 seconds.
1133
1134
`-s suffix'
1135
Suffix of files generated by *pgen*. Default is '.dfg'.
1136
1137
`-r filename'
1138
Write representation of the reduced tableau to <filename>.
1139
1140
`-n filename'
1141
Write representation of the non-reduced tableau to <filename>.
1142
1143
`-vinci'
1144
Write tableau representation in daVinci format.
1145
1146
`-xvcg'
1147
Write tableau representation in xvcg format.
1148
1149
1150
File: script.info, Node: daVinci and VCG, Up: Top
1151
1152
5.5 DAVINCI AND VCG
1153
====================
1154
1155
*VCG* is a public domain tool intended for visualizing compiler graphs.
1156
It is developed by Georg Sander at the University of Saarbruecken. It
1157
is available via anonymous ftp at
1158
ftp.cs.uni-sb.de
1159
in the directory pub/graphics/vcg. Or visit
1160
http://rw4.cs.uni-sb.de/~sander/html/gsvcg1.html.
1161
*daVinci* is another public domain graph visualizing tool. Get it at
1162
ftp.tzi.de
1163
in the directory /tzi/biss/daVinci. The WWW address is
1164
http://www.informatik.uni-bremen.de/daVinci/.
1165
1166
5.6 AUTHORS
1167
===========
1168
1169
Thorsten Engel and Christian Theobalt.
1170
1171
Contact : spass@mpi-inf.mpg.de
1172
1173
5.7 SEE ALSO
1174
============
1175
1176
checkstat(1), filestat(1), pcs(1), rescmp(1), tpform(1), tpget(1),
1177
deprose(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)
1178
1179
1180
File: script.info, Node: rescmp, Next: tpform, Prev: pgen, Up: Top
1181
1182
6 rescmp
1183
********
1184
1185
6.1 NAME
1186
========
1187
1188
rescmp - tests subsumption relation between clause sets
1189
1190
6.2 SYNOPSIS
1191
============
1192
1193
*rescmp* [ -v] file
1194
1195
6.3 DESCRIPTION
1196
===============
1197
1198
*rescmp* is a C-program that compares two clause sets specified by two
1199
*DFG* files. It tries to find, for each clause in the first set, a
1200
corresponding clause in the second set such that both clauses mutually
1201
subsume. It reports success only if there is a one-to-one mapping
1202
between the two sets under this condition.
1203
1204
6.4 OPTIONS
1205
===========
1206
1207
The following options are supported by *rescmp*:
1208
`-v'
1209
prints out unmapped clauses - that is clauses that have no
1210
corresponding clause - in both sets.
1211
1212
6.5 AUTHORS
1213
===========
1214
1215
Thorsten Engel and Christian Theobalt.
1216
1217
Contact : spass@mpi-inf.mpg.de
1218
1219
cc man end
1220
1221
6.6 SEE ALSO
1222
============
1223
1224
checkstat(1), filestat(1), pcs(1), pgen(1), tpform(1), tpget(1),
1225
deprose(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)
1226
1227
1228
File: script.info, Node: tpform, Next: tpget, Prev: rescmp, Up: Top
1229
1230
7 tpform
1231
********
1232
1233
7.1 NAME
1234
========
1235
1236
tpform - transforms SPASS output statements into TPTP style format
1237
1238
7.2 SYNOPSIS
1239
============
1240
1241
*tpform* [ -tb] [infile] [outfile]
1242
1243
7.3 DESCRIPTION
1244
===============
1245
1246
The *tpform* script transforms a list of SPASS outputs into a TPTP
1247
result file or another simple file format. Both formats are a list of
1248
problem file names annotated with information, like the logical status
1249
of the problem and time needed to decide the status etc.
1250
1251
If no file arguments are given, *tpform* reads from stdin and writes to
1252
stdout. If one file argument is given, *tpform* read from that file, and
1253
if a second argument is present, *tpform* writes to it.
1254
1255
1256
1257
7.4 OPTIONS
1258
===========
1259
1260
The following options are supported by *tpform*:
1261
`-b'
1262
Selects simple output format instead of TPTP format
1263
1264
`-t'
1265
If -b is selected, print *SPASS* running time at the end of each
1266
output line, eg: `SteamRoller + 00:00:05.28'
1267
1268
7.5 FORMATS
1269
===========
1270
1271
We take the following *SPASS* output as an example:
1272
1273
SPASS V0.78
1274
SPASS beiseite: Proof found.
1275
Problem: Tests/Pelletier/problem1.dfg
1276
SPASS derived 0 clauses, backtracked 0 clauses and kept 3 clauses.
1277
SPASS allocated 165 KBytes.
1278
SPASS spent 0:00:00.01 on the problem.
1279
0:00:00.00 for the input.
1280
0:00:00.00 for the FLOTTER CNF translation.
1281
0:00:00.00 for inferences.
1282
0:00:00.00 for the backtracking.
1283
1284
The TPTP format for this information is:
1285
1286
problem1.dfg P 1 0.01 165 3 - -
1287
^ ^ ^^^^ ^^^ ^ ^ ^
1288
P/M # proofs time memory clauses proof proof
1289
or error length depth
1290
message
1291
1292
The simple format is for this example:
1293
1294
problem1.dfg +
1295
1296
and in general:
1297
1298
filename {+|-|0} [time]
1299
1300
where '+' marks problems for which *SPASS* found a proof, '0' stands
1301
for found completions and '-' marks undecided problems. The time
1302
information is given if the -t option is used.
1303
1304
7.6 AUTHORS
1305
===========
1306
1307
Thorsten Engel and Christian Theobalt.
1308
1309
Contact : spass@mpi-inf.mpg.de
1310
1311
7.7 SEE ALSO
1312
============
1313
1314
checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpget(1),
1315
deprose(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)
1316
1317
1318
File: script.info, Node: tpget, Next: deprose, Prev: tpform, Up: Top
1319
1320
8 tpget
1321
*******
1322
1323
8.1 NAME
1324
========
1325
1326
tpget - selects problems from a library
1327
1328
8.2 SYNOPSIS
1329
============
1330
1331
*tpget* [-l libdir] file_1 ... file_n target
1332
1333
8.3 DESCRIPTION
1334
===============
1335
1336
*tpget* reads lists of theorem proving problems in TPTP format (TPTP
1337
scripts) and assembles the problem files specifying these problems into
1338
a target directory . The problem files are taken from the library
1339
specified by the -l option (see example below). If a problem file
1340
already exists in the target directory it is not copied again.
1341
1342
The files file_1 ... file_n have to contain one short problem name
1343
per line. Examples for short problem names are `SYN313-1.001:002' or
1344
`LCL354+1'.
1345
1346
8.4 OPTIONS
1347
===========
1348
1349
The following option is required by *tpget*:
1350
1351
`-l'
1352
Specifies the library where problem files are taken from.
1353
1354
8.5 EXAMPLES
1355
============
1356
1357
To assemble all problem files specified by file into Dir, using the
1358
library /foo/bar:
1359
*tpget* -l /foo/bar file Dir
1360
1361
8.6 AUTHORS
1362
===========
1363
1364
Thorsten Engel, Enno Keen and Christian Theobalt.
1365
1366
Contact : spass@mpi-inf.mpg.de
1367
1368
8.7 SEE ALSO
1369
============
1370
1371
checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1),
1372
deprose(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)
1373
1374
1375
File: script.info, Node: deprose, Next: dfg2ascii, Prev: tpget, Up: Top
1376
1377
9 deprose
1378
*********
1379
1380
9.1 NAME
1381
========
1382
1383
deprose - condenses checkstat error output
1384
1385
9.2 SYNOPSIS
1386
============
1387
1388
*deprose* [infile] [outfile]
1389
1390
9.3 DESCRIPTION
1391
===============
1392
1393
*deprose* is a *Perl* script for condensing *checkstat* error output.
1394
As input, it gets an arbitrary text containing messages of the
1395
following form:
1396
1397
* Problem 'xy':
1398
* SPASS computes problem state 'satisfiable'
1399
* which is declared 'unsatisfiable'
1400
1401
*deprose* outputs an annotated list of the files in which errors
1402
occurred. Each file in this list is annotated with '+', if *SPASS*
1403
found a proof on this file, or '-', if *SPASS* found a model.
1404
1405
If no file arguments are given, *deprose* reads from stdin and writes to
1406
stdout. If one file argument is given, *deprose* reads from that file,
1407
and if a second argument is given, *deprose* writes to that file.
1408
1409
9.4 AUTHORS
1410
===========
1411
1412
Thorsten Engel and Christian Theobalt
1413
1414
Contact : spass@mpi-inf.mpg.de
1415
1416
9.5 SEE ALSO
1417
============
1418
1419
checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1),
1420
tpget(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)
1421
1422
1423
File: script.info, Node: dfg2ascii, Next: dfg2otter, Prev: deprose, Up: Top
1424
1425
10 dfg2ascii
1426
************
1427
1428
10.1 NAME
1429
=========
1430
1431
dfg2ascii - transforms DFG files into pretty printed ASCII files
1432
1433
10.2 SYNOPSIS
1434
=============
1435
1436
*dfg2ascii* <infile>
1437
1438
10.3 DESCRIPTION
1439
================
1440
1441
*dfg2ascii* is a program to convert a problem input file in *DFG*
1442
format into pretty-printed ASCII text. It prints out the axioms and the
1443
conjectures, in that order.
1444
1445
10.4 AUTHORS
1446
============
1447
1448
Thomas Hillenbrand, Dalibor Topic and Christoph Weidenbach.
1449
1450
Contact : spass@mpi-inf.mpg.de
1451
1452
10.5 SEE ALSO
1453
=============
1454
1455
checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1),
1456
tpget(1), deprose(1), dfg2otter(1), SPASS(1)
1457
1458
1459
File: script.info, Node: dfg2otter, Next: dfg2otter.pl, Prev: dfg2ascii, Up: Top
1460
1461
11 dfg2otter
1462
************
1463
1464
11.1 NAME
1465
=========
1466
1467
dfg2otter - transforms DFG clause files into Otter format
1468
1469
11.2 SYNOPSIS
1470
=============
1471
1472
*dfg2otter* [options] <infile> <outfile>
1473
1474
11.3 DESCRIPTION
1475
================
1476
1477
*dfg2otter* is a C-program to transform problem input files in *DFG*
1478
syntax into *Otter* syntax. It accepts all options from *SPASS*,
1479
although only a subset has an effect on translation.
1480
1481
*dfg2otter* negates conjecture formulae of the *SPASS* input file
1482
before printing the Otter usable list. The *SPASS* conjecture formula
1483
list is translated into a disjunction of the negated single conjectures.
1484
If the *SPASS* input file consits of clauses, these are not modified.
1485
1486
11.4 AUTHORS
1487
============
1488
1489
Thomas Hillenbrand, Dalibor Topic and Christoph Weidenbach
1490
1491
Contact : spass@mpi-inf.mpg.de
1492
1493
11.5 SEE ALSO
1494
=============
1495
1496
checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1),
1497
tpget(1), deprose(1), dfg2otter.pl(1), SPASS(1)
1498
1499
1500
File: script.info, Node: dfg2otter.pl, Next: dfg2dfg, Prev: dfg2otter, Up: Top
1501
1502
12 dfg2otter.pl
1503
***************
1504
1505
12.1 NAME
1506
=========
1507
1508
dfg2otter.pl - transforms DFG clause files into Otter format including
1509
Otter options
1510
1511
12.2 SYNOPSIS
1512
=============
1513
1514
*dfg2otter.pl* [options] [infile] [outfile]
1515
1516
12.3 DESCRIPTION
1517
================
1518
1519
*dfg2otter.pl* is a *Perl* wrapper for the *dfg2otter*. Mainly, it adds
1520
a set of OTTER parameters to the transformation result of *dfg2otter*.
1521
Additionally, input/output redirection is simpler: If no file arguments
1522
are given, *dfg2otter.pl* reads from stdin and writes to stdout. If one
1523
file argument is given, *dfg2otter.pl* read from that file, and if a
1524
second argument is present, *dfg2otter.pl* writes to it.
1525
1526
12.4 OPTIONS
1527
============
1528
1529
`-t n'
1530
Sets the time limit for the OTTER proof attempt to n seconds.
1531
1532
12.5 AUTHORS
1533
============
1534
1535
Thorsten Engel and Christian Theobalt.
1536
1537
Contact : spass@mpi-inf.mpg.de
1538
1539
12.6 SEE ALSO
1540
=============
1541
1542
checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1),
1543
tpget(1), deprose(1), dfg2otter(1), SPASS(1)
1544
1545
1546
File: script.info, Node: dfg2dfg, Next: dfg2tptp, Prev: dfg2otter.pl, Up: Top
1547
1548
13 dfg2dfg
1549
**********
1550
1551
13.1 NAME
1552
=========
1553
1554
dfg2dfg - calculate approximations of problems
1555
1556
13.2 SYNOPSIS
1557
=============
1558
1559
*dfg2dfg* [-horn] [-monadic] [-linear] [-shallow] [INFILE] [OUTFILE]
1560
1561
13.3 DESCRIPTION
1562
================
1563
1564
*dfg2dfg* is a program that reads clauses from an input file in DFG
1565
syntax. It then calculates an approximation of the clause set
1566
depending on the command line options. Finally it writes the
1567
approximated clause set in DFG syntax to a file.
1568
1569
If neither INFILE nor OUTFILE are given, *dfg2dfg* reads from
1570
standard input and writes to standard output. If one file name is
1571
given, it reads from that file and writes the output to standard output.
1572
If more than one file name is given, *dfg2dfg* reads from the first
1573
file and writes to the second.
1574
1575
The approximations are described in technical detail in the separate
1576
paper *dfg2dfg.ps* included in the SPASS distribution.
1577
1578
13.4 OPTIONS
1579
============
1580
1581
*dfg2dfg* has four different command line options that may be combined.
1582
`-horn'
1583
This option enables the transformation of non-horn clauses into
1584
horn clauses. Each non-horn clause with _n_ positive literals is
1585
transformed into _n_ horn clauses, where the _i_-th clause
1586
contains the _i_-th positive literal and all negative literals of
1587
the non-horn clause. See also section 3 of the paper.
1588
1589
`-monadic[=n]'
1590
With this option atoms with non-monadic predicate symbols are
1591
transformed into monadic atoms. If _n_ is omitted or _n_=1 a term
1592
encoding is applied, i.e., all non-monadic predicates are moved to
1593
the term level. With _n_=2 a projection is applied. All
1594
non-monadic atoms are replaced by their monadic argument
1595
projections. See section 4.1 section 4.2 of the paper for more
1596
details.
1597
1598
`-linear'
1599
This approximation transforms a clause with monadic literals and
1600
non-linear variable occurrences in succedent atoms, into a new
1601
clause with possibly more negative literals, that doesn't contain
1602
any non-linear variables in the succedent. See section 5 of the
1603
paper for details.
1604
1605
`-shallow[=n]'
1606
This transformation tries to reduce the depth of the terms in
1607
positive literals. The transformation is applied to horn clauses
1608
with monadic literals only. If _n_ is omitted or _n_=1 a strict
1609
transformation is applied, that is equivalence preserving, however.
1610
For _n_=2 some preconditions are removed. This allows the
1611
transformation to be applied more often, but the transformation
1612
isn't equivalence preserving any more. For _n_=3 even more
1613
preconditions are removed. Take a look at section 6._n_ of the
1614
paper for the details of the command line option _-monadic=n_.
1615
1616
13.5 AUTHORS
1617
============
1618
1619
Enno Keen
1620
1621
Contact : spass@mpi-inf.mpg.de
1622
1623
13.6 SEE ALSO
1624
=============
1625
1626
SPASS(1)
1627
1628
1629
File: script.info, Node: dfg2tptp, Next: tptp2dfg, Prev: dfg2dfg, Up: Top
1630
1631
14 dfg2tptp
1632
***********
1633
1634
14.1 NAME
1635
=========
1636
1637
dfg2tptp - transforms DFG files into TPTP files.
1638
1639
14.2 SYNOPSIS
1640
=============
1641
1642
*dfg2tptp* <input-file> <output-file>
1643
1644
14.3 DESCRIPTION
1645
================
1646
1647
*dfg2tptp* is a program which converts a problem input file in *DFG*
1648
format into a problem input file in *TPTP* format. The *TPTP* problem
1649
format is used by the TPTP library of test problems for automated
1650
theorem proving, available at *http://www.math.miami.edu/~tptp/*.
1651
Various tools exist to convert problems in *TPTP* format into input
1652
files for other theorem provers.
1653
1654
14.4 AUTHORS
1655
============
1656
1657
Thomas Hillenbrand, Dalibor Topic and Christoph Weidenbach
1658
1659
Contact : spass@mpi-inf.mpg.de
1660
1661
14.5 SEE ALSO
1662
=============
1663
1664
checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1),
1665
tpget(1), deprose(1), dfg2otter(1), SPASS(1)
1666
1667
1668
File: script.info, Node: tptp2dfg, Next: spassfaq, Prev: dfg2tptp, Up: Top
1669
1670
15 tptp2dfg
1671
***********
1672
1673
15.1 NAME
1674
=========
1675
1676
tptp2dfg - transforms DFG files into TPTP files.
1677
1678
15.2 SYNOPSIS
1679
=============
1680
1681
*tptp2dfg* [-include] <input-file> <output-file>
1682
1683
15.3 DESCRIPTION
1684
================
1685
1686
*tptp2dfg* is a program which converts a problem input file in *TPTP*
1687
format into a problem input file in *DFG* format. The *TPTP* problem
1688
format is used by the TPTP library of test problems for automated
1689
theorem proving, available at *http://www.math.miami.edu/~tptp/*.
1690
1691
15.4 OPTIONS
1692
============
1693
1694
*tptp2dfg* supports the following command line options.
1695
`-include'
1696
This option enables the expansion of include directives in tptp
1697
files. If set all TPTP include directives in hte input-file are
1698
replaced by the respective file content during translation. If not
1699
set the TPTP include directives are translated into DFG include
1700
directives. Default is off.
1701
1702
15.5 AUTHORS
1703
============
1704
1705
Martin Suda and Christoph Weidenbach
1706
1707
Contact : spass@mpi-inf.mpg.de
1708
1709
15.6 SEE ALSO
1710
=============
1711
1712
dfg2tptp(1), dfg2otter(1), SPASS(1)
1713
1714
1715
File: script.info, Node: spassfaq, Prev: tptp2dfg, Up: Top
1716
1717
16 spassfaq
1718
***********
1719
1720
16.1 QUESTIONS
1721
==============
1722
1723
Q: How can I get an answer substitution?
1724
1725
16.2 ANSWERS
1726
============
1727
1728
A: There are no meta predicates in SPASS available. Hence,
1729
this functionality is not directly supported. However it can be
1730
achieved by a trick. The idea is to add a new literal to the
1731
conjecture clause that carries the substitution and will
1732
definitely be resolved away in the final step of the proof.
1733
For example: let x be the variable where we are interested in
1734
the subsitution. Let x occur in the single conjecture clause C.
1735
Then extend this clause to C,P(x,a,y) and add the clause
1736
-P(z,u,b), where P is new, and a,b are constants. Furthermore
1737
make P a minimal predicate using a set_DomPred declaration (see
1738
the SPASS man page). This will force that the final step in the
1739
proof is the one that eliminates the P literal and the x will
1740
be instantiated accordingly. To make this work it may be
1741
necessary to turn off certain reduction rules of SPASS. To get
1742
it rid of that, a trick is to extend all predicates in C by a
1743
further argument with the variable y and all other occurrences
1744
of these predicate with fresh variables.
1745
1746
16.3 AUTHORS
1747
============
1748
1749
Thomas Hillenbrand, Dalibor Topic and Christoph Weidenbach
1750
1751
Contact : spass@mpi-inf.mpg.de
1752
1753
16.4 SEE ALSO
1754
=============
1755
1756
SPASS(1)
1757
6
1758
7
1759
8
1760
Tag Table:
9
1761
Node: Top0
1762
Node: SPASS955
1763
Node: checkstat25745
1764
Node: filestat31578
1765
Node: pcs32830
1766
Node: pgen37169
1767
Node: daVinci and VCG39480
1768
Node: rescmp40322
1769
Node: tpform41337
1770
Node: tpget43767
1771
Node: deprose45060
1772
Node: dfg2ascii46227
1773
Node: dfg2otter46941
1774
Node: dfg2otter.pl47979
1775
Node: dfg2dfg49073
1776
Node: dfg2tptp51995
1777
Node: tptp2dfg52912
1778
Node: spassfaq54052
10
1779
11
1780
End Tag Table
Loggerhead is a web-based interface for Breezy
Version: 2.0.1