U. Hustadt and R. A. Schmidt (2000c): MSPASS: Modal Reasoning by Translation and First-Order Resolution

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, July 3-7, 2000), pp. 67-71. LNAI 1847, Springer 2000.
Abstract, BibTeX. Postscript, PDF (© Springer-Verlag).

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. [an error occurred while processing this directive]