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