@INPROCEEDINGS{Hustadt+Schmidt@TABLEAUX2000,
 AUTHOR        = {Hustadt, Ullrich and Schmidt, Renate},
 TITLE         = {{MSPASS}: Modal reasoning by translation and first-order resolution},
 PAGES         = {67-71},
 BOOKTITLE     = {Proceedings of the International Conference on
 Automated Reasoning with Analytic Tableaux and Related Methods 
 (TABLEAUX 2000) [St. Andrews, Scotland, 3-7 July 2000]},
 YEAR          = {2000},
 EDITOR        = {Dyckhoff, Roy},
 PUBLISHER     = {Springer},
 PADDRESS      = {Berlin},
 PYEAR         = {2000},
 CADDRESS      = {St. Andrews, Scotland},
 CYEAR         = {2000},
 CMONTH        = jul # {3-7},
 SERIES        = {LNAI},
 VOLUME        = {1847},
 ISBN          = {3-540-67697-X},
 URL           = {Hustadt+Schmidt@TABLEAUX2000.pdf},
 ABSTRACT      = {MSPASS is an extension of the first-order
 theorem prover 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.}
}