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.