U. Hustadt, R. A. Schmidt and C. Weidenbach (1999): MSPASS: Subsumption testing with SPASS

U. Hustadt, R. A. Schmidt, and C. Weidenbach (1999): ``MSPASS: Subsumption testing with SPASS.'' In P. Lambrix et al., editors, Proceedings of the International Workshop on Description Logics (DL'99) [Linköping University, Sweden], pp. 136-137.
Abstract, BiBTeX, PDF.

SPASS is an enhancement of the first-order theorem prover SPASS with a translator of modal formulae, formulae of description logics, and formulae of the relational calculus into first-order logic with equality. SPASS is one of the fastest and most sophisticated existing first-order theorem provers and its performance compares well with special purpose theorem provers for modal logics, description logics and first-order logic, in general.