@INPROCEEDINGS{HustadtSchmidt00b,
AUTHOR = {Hustadt, U. and Schmidt, R. A.},
YEAR = {2000},
TITLE = {{MSPASS}: Modal Reasoning by Translation and First-Order Resolution},
EDITOR = {Dyckhoff, R.},
BOOKTITLE = {Automated Reasoning with Analytic Tableaux and Related Methods, International Conference (TABLEAUX 2000)},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {1847},
PUBLISHER = {Springer},
PAGES = {67--71},
ISBN = {3-540-67697-X},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/HustadtSchmidt00b.html},
ABSTRACT = {\textsc{mspass} is an extension of the first-order theorem
prover \textsc{spass},
which can be used as a modal logic theorem prover, a theorem prover for
description logics and a theorem prover for the relational calculus.
}
}