MSPASS is a fully automated theorem prover for numerous logics. Being an extension of SPASS, it is a resolution prover for first-order logic (with equality), but it is also a prover for numerous description logics, modal logics (both traditional modal logics and dynamic modal logics e.g. Boolean modal logic, Peirce logic) and the relational calculus.
July 2007: MSPASS is now incorporated into SPASS.
Spring 2008: John Kevin Smith has implemented the axiomatic translation for modal logic in SPASS. Web interface, Project page and downloads.