| 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. |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
