(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-1995First 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 Keil1991-1992implemented a resolution based prover called STOP.
Peter Graf1991-1995implemented indexing structures and sorted unification in STOP. He then analyzed term indexing techniques and suggested substitution tree indexing.
Bernd Gaede1994-1995on 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 Rock1994-1995implemented 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 Meyer1994-1997implemented substitution tree indexing and related data structures in SPASS.
Christian Cohrs1995-1998reimplemented the data structures for splitting in SPASS and added several refinements to it. Added support for atom definitions.
Enno Keen1994-2000introduced generic parsing support and is responsible for bug fixing. Student in chief.
Thorsten Engel1996-1998reimplemented the proof documentation of SPASS and added a generic proof checker.
Dalibor Topic1998-1999reimplemented and extended our memory management. It can now catch a bunch of memory errors.
2000-2008student in chief. Implemented the Qt based GUI for Windows and MAC.
Christian Theobalt1998-1999ported SPASS to the Windows world.
Uwe Brahm1998-1999put SPASS on the Web.
Georg Jung1998-1999prepared drawings for our logo(s), see below.
Bijan Afshordel1998-1999implemented several reductions on the formula level and redesigned/extended the atom definition support in SPASS.
Christof Brinker1998-1999added the detection and elemination of local semantic tautologies.
Renate Schmidt2006-contributed translation technology for extended modal logics.
Patrick Wischnewski2006-implemented contextual rewriting and updated existing rewriting.
Arnaud Fietzke2006-2014refined spitting backtracking.
Evgeny Kruglov2006-2013build the first version of SPASS(LA) implementing superposition modulo linear arithmetic constraints.
Jennifer Müller2008-takes care of maintaining the SPASS web pages.
Martin Suda2008-2015implemented TPTP syntax support, faster parsing and integration of chaining.
Rohit Kumar2008-2009implemented the new command line parser.
Dilyana Dimova2008-2009reimplemented parts of the sort module.
Matthias Horbach2009- is doing an integration of disunification and predicate completion into SPASS. First version is available from the prototype section.
Anand Ramkumar2009-2010 did the Windows and Mac porting.
Sri Charanya Dhinakaran2009-2010prepared 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 Bromberger2014-is developing efficient arithmetic constraint solvers.
Dominik Wagner2014-is setting up new backbone data structures and builds SAT solvers on top of it.
Uwe Brahm, Patrick Cernco2016-2017set 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.