System Description: SPASS Version 3.0

Weidenbach, C., Schmidt, R. A., Hillenbrand, T., Rusev, R., and Topic, D. (2007)

In Pfenning, F. (eds), Automated Deduction-CADE-21. Lecture Notes in Artificial Intelligence, 4603 Springer, 514-520. BiBTeX, DOI Link.

SPASS is an automated theorem prover for full first-order logic with equality and a number of non-classical logics. This system description provides an overview of our recent developments in SPASS 3.0, including support for dynamic modal logics, relational logics and expressive description logics, additional renaming and selection strategies, and significant interface enhancements for human and machine users.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 08 Apr 08
Copyright © 2007 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk