MSPASS (original) (raw)

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
The SPASS Handbook in the SPASS distribution provides comprehensive documentation. See also the MSPASS Documentation webpage.
Manual
Benchmark problems
Download area of SPASS

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

Last modified: 22 May 08