U. Hustadt and R. A. Schmidt (2000c): ``MSPASS: Modal Reasoning by Translation and First-Order Resolution'' In R. Dyckhoff, editor, Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2000) [St. Andrews, Scotland, 3-7 July 2000], pp. 67-71. LNAI 1847, Springer 2000.
Abstract, BibTeX. PDF (© Springer).

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.