@INPROCEEDINGS{WeidenbachSchmidtEtAl07,
AUTHOR = {Weidenbach, C. and Schmidt, R. A. and Hillenbrand, T. and Rusev, R. and Topic, D.},
YEAR = {2007},
TITLE = {System Description: {SPASS} Version 3.0},
EDITOR = {Pfenning, F.},
BOOKTITLE = {Automated Deduction---CADE-21},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {4603},
PUBLISHER = {Springer},
PAGES = {514--520},
ISBN = {3-540-43931-5},
DOI = {http://dx.doi.org/10.1007/978-3-540-73595-3_38},
URL = {\url{http://www.cs.man.ac.uk/~schmidt/publications/WeidenbachSchmidtEtAl07.html}},
ABSTRACT = {
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.
}
}