SPASS

SPASS (main developer Christoph Weidenbach) is a first order theorem prover based on the superposition calculus, developped at the Max-Planck Institut für Informatik, Saarbrücken, Germany.

During my post-doc at MPI-I, I have made minor contributions to the development of this automated deduction system, implementating in particular approximation methods and Horn clauses transformation functions for the purpose of unification modulo sorted equational theories. This work was done in callaboration with Christoph Weidenbach and Christoph Meyer.