(Hi)Story
SPASS History before 1.0.0
| - | 1994 | We developed several prototypes and experimented with different data structures (e.g. different indexing approaches), memory models, sorted unification. | |
| 1994 | - | 1995 | First official release of SPASS, Version 0.42. It contained an implementation of the superposition calculus with sorted unification integrated by specific inference/reduction rules, a splitting rule and the clause normal form translator FLOTTER. |
| 1995 | - | 1996 | Internal release is SPASS Version 0.49. We officially released during this year SPASS Version 0.55 fixing several bugs in Version 0.49. |
| 1996 | - | 1997 | Internal release is SPASS Version 0.77. Improved the interface to the indexing module, added rewriting with unorientable equations and support for atom definitions. |
| 1997 | - | 1998 | Internal release is SPASS Version 0.95. We added a proof checker and reimplemented our proof generation module as well as the splitting module. |
| 1998 | - | 1999 | Internal release is SPASS Version 1.0.0a. We integrated further reduction/inference rules, some specific support for finite domains, improved speed of FLOTTER. |
| 1999 | - | 2000 | In October 1999 we put the third official release of SPASS, Version 1.0.0 on the Web. The distribution now contains man-pages, several tools and we offer a native version for Windows 95/98/NT. |
SPASS People
| Monika Keil | 1991 | - | 1992 | implemented a resolution based prover called STOP. |
| Peter Graf | 1991 | - | 1995 | implemented indexing structures and sorted unification in STOP. He then analyzed term indexing techniques and suggested substitution tree indexing. |
| Bernd Gaede | 1994 | - | 1995 | on the basis of the data structures used for STOP, he built the first SPASS version and created the acronym. Synergetic Prover Augmenting Superposition with Sorts |
| Georg Rock | 1994 | - | 1995 | implemented the first version of our sophisticated clause normal form translator FLOTTER. FLOTTER means "faster" in German and our CNF translation procedure can significantly speed up an afterwards applied theorem proving procedure. |
| Christoph Meyer | 1994 | - | 1997 | implemented substitution tree indexing and related data structures in SPASS. |
| Christian Cohrs | 1995 | - | 1998 | reimplemented the data structures for splitting in SPASS and added several refinements to it. Added support for atom definitions. |
| Enno Keen | 1994 | - | 2000 | introduced generic parsing support and is responsible for bug fixing. Student in chief. |
| Thorsten Engel | 1996 | - | 1998 | reimplemented the proof documentation of SPASS and added a generic proof checker. |
| Dalibor Topic | 1998 | - | 1999 | reimplemented and extended our memory management. It can now catch a bunch of memory errors. |
| 2000 | - | 2008 | student in chief. Implemented the Qt based GUI for Windows and MAC. | |
| Christian Theobalt | 1998 | - | 1999 | ported SPASS to the Windows world. |
| Uwe Brahm | 1998 | - | 1999 | put SPASS on the Web. |
| Georg Jung | 1998 | - | 1999 | prepared drawings for our logo(s), see below. |
| Bijan Afshordel | 1998 | - | 1999 | implemented several reductions on the formula level and redesigned/extended the atom definition support in SPASS. |
| Christof Brinker | 1998 | - | 1999 | added the detection and elemination of local semantic tautologies. |
| Renate Schmidt | 2006 | - | contributed translation technology for extended modal logics. | |
| Patrick Wischnewski | 2006 | - | implemented contextual rewriting and updated existing rewriting. | |
| Arnaud Fietzke | 2006 | - | 2014 | refined spitting backtracking. |
| Evgeny Kruglov | 2006 | - | 2013 | build the first version of SPASS(LA) implementing superposition modulo linear arithmetic constraints. |
| Jennifer Müller | 2008 | - | takes care of maintaining the SPASS web pages. | |
| Martin Suda | 2008 | - | 2015 | implemented TPTP syntax support, faster parsing and integration of chaining. |
| Rohit Kumar | 2008 | - | 2009 | implemented the new command line parser. |
| Dilyana Dimova | 2008 | - | 2009 | reimplemented parts of the sort module. |
| Matthias Horbach | 2009 | - | is doing an integration of disunification and predicate completion into SPASS. First version is available from the prototype section. | |
| Anand Ramkumar | 2009 | - | 2010 | did the Windows and Mac porting. |
| Sri Charanya Dhinakaran | 2009 | - | 2010 | prepared a move from the Qt to a Java based GUI. |
| Binod Bhattarai | 2009 | - | 2011 | cleaned our code for 64-Bit, in particular removed warnings and adjusted the code to C standards. |
| Martin Bromberger | 2014 | - | is developing efficient arithmetic constraint solvers. | |
| Dominik Wagner | 2014 | - | is setting up new backbone data structures and builds SAT solvers on top of it. | |
| Uwe Brahm, Patrick Cernco | 2016 | - | 2017 | set up the new WebSPASS |
Classic SPASS Logo
After having performed a strong logo contest that resulted in many fancy suggestions, e.g., have a look at an earlier logo suggestion from Georg Jung, we decided to take a drawing of Opistognathus Latitabunda from Georg Jung as the basis for our design. With the help of several weekends and a bunch of tools, we turned it into what it is now.
