1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
Version: 1.0.1
- Fixed a bug in the atom definition support where it could happen
that variable dependencies between the atom definition and formulae
outside the definition are discarded.
- Fixed a bug in the renaming module, where in some cases a renaming
with non-zero benefit was not performed.
Version: 1.0.2
- Fixed inconsistencies between the DFG proof format description in
dfgsyntax.ps and the actual implementation. Proof checking is more
more liberal, because the empty clause needs not to have the highest
clause number.
Version: 1.0.3
- Sharpend renaming; it now potentially produces fewer clauses.
Version: 1.0.4
- Changed some clause generation functions such that sequentially
applying FLOTTER, SPASS and just applying SPASS result in the
very same clause sets.
- Added the new tool dfg2dfg that supports transformations into
monadic clause classes and their further approximations.
Version: 1.0.5
- Improved SPASS man pages: In particular, we added further detailed
explanations of inference rule flags and soft typing flags.
- Significantly improved modularity of the code by making the flagstore
object part of the proof search object; so there is no global flagstore
around anymore. These changes touched nearly all modules.
- Changed certain clause generation procedures such that now applying SPASS
directly to a formula or subsequent application of FLOTTER and SPASS produce
exactly the same ordering of a clause set (literlas). Since the behaviour of
SPASS is not independant from initial clause/literal orderings the changes
make SPASS results a little more robust/more predictable.
As all code was touched, we also included a code style review (comments,
prototypes, ...).
- Flag values given to SPASS are now checked and rejected if out of range.
Version: 1.0.6
- Strengthened prototyping of functions in particular in the case of function
arguments. This resulted in specialized extra functions.
- Improved printing efficiency by replacing (f)printf calls with (f)puts calls
whenever possible.
- Removed the modul global precedence variable of the symbol modul and replaced
it by argument passing. The precedence is now stored in the proofsearch structure.
This affected huge parts of the SPASS code.
- Adjusted comments and code layout.
- Strengthened warnings for the gcc compiler.
- Increased usage of the string module.
Version: 2.0.0
- Corrections to spellings, documentation.
- Added handbooks for SPASS and dfg2dfg.
- Added contextual rewriting.
- Added semantic tautology check.
- Fixed bugs in CNF translation: Renaming, Equation elimination rules.
- Improved splitting clause selection on the basis of reduction potential.
- Improved robustness of initial clause list ordering.
- Added the terminator module.
- Extended formula definition detection/expansion to so called guarded definitions.
- Improved determination of initial precedence such that as many as possible
equations in the input clause list can be oriented.
- Added mainloop without complete interreduction.
- Developed PROOFSEARCH data type enabling a modularization of the SPASS
source code on search engine level, such that several proof attempts can
now be run completely independantly at the same time within SPASS.
- Moved GUI to Qt 3.0. The GUI now also includes dfg2dfg and new even more
user friendly layout. The GUI runs on any platform where SPASS and Qt are
available.
Version: 2.1
- Fixed a bug in the definition module. Formulae were not normalized before
application of the procedure, leading to wrong matchings of variables.
- Fixed a bug in the flag module. The subproof flagstore settings were not
complete: ordering flag and the weight flags were missing.
- Fixed a bug in dfgparser.y, where a missing semicolon with
bison version 1.75 now caused an error.
- Fixed a bug in cnf.c where the formula "equiv(false,false)" was
not properly treated in function cnf_RemoveTrivialAtoms.
- Fixed a bug in symbol_LowerSignature where capital 'A's and 'Z's were not
prefixed by a lowercase 'ss' due to their exclusion in the condition. This
caused problems in the result of dfg2tptp applied to dfg input files with
uppercase symbols starting with an 'A' or 'Z'.
- Now dfg2otter negates conjecture formulae of the SPASS input file
before printing the Otter usable list.
- Added man pages for dfg2ascii, dfg2otter and dfg2tptp.
|
