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.