SPASS v3.5+
A tableau-resolution prover

  What is SPASS v3.5+?
SPASS v3.5+ is an extension of the first-order resolution theorm prover SPASS that simulates semantic tableau provers. The simulation provides ground semantic tableau proofs and models that are translated from resolution proofs and saturated sets of clauses.

The current implementation provides tableau simulation for traditional modal logics and dynamic modal logics defined over relations closed under intersection, union and converse with the support of adding relational frame conditions.

  Download
SPASS v3.5+ source files (.tgz)
  1. Export the source files to a desired directory
  2. Run make, to compile the package.

  Reference
AlBarakati, Rawan (2009), Development of a Tableaux-Resolution Prover. Msc Thesis, The University of Manchester, UK.
This project was supervised by Dr. Renate Schmidt, School of Computer Science, The University of Manchester.



Rawan G. AlBarakati
Msc Student, 2009
The University of Manchester
Contact



Copyright © 2009, Rawan Ghali AlBarakati.