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.

Web Interactive Input Form | Web Upload Form | Documentation | Manual

Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 22 May 08
Copyright © 1999-2007 Renate A. Schmidt, School of Computer Science, Man Univ,