Weidenbach, Christoph; Brahm, Uwe; Hillenbrand, Thomas; Keen, Enno; Theobald, Christian; Topić, Dalibor SPASS version 2.0. (English) Zbl 1072.68596 Voronkov, Andrei (ed.), Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27–30, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43931-5). Lect. Notes Comput. Sci. 2392, 275-279 (2002). Summary: SPASS is an automated theorem prover for full first-order logic with equality. This system description provides an overview of recent developments in SPASS 2.0, including among others an implementation of contextual rewriting, refinements of the clause normal form transformation, and enhancements of the inference engine.For the entire collection see [Zbl 0993.00050]. Cited in 18 Documents MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Software:SPASS PDFBibTeX XMLCite \textit{C. Weidenbach} et al., Lect. Notes Comput. Sci. 2392, 275--279 (2002; Zbl 1072.68596) Full Text: Link