×

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

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

SPASS
PDFBibTeX XMLCite
Full Text: Link