Publication details

Saarland University Computer Science

Terminating Tableau Systems for Modal Logic with Equality

Mark Kaminski, Gert Smolka

Technical Report, Saarland University, Campus E1 3, 66123 Saarbrücken, Germany, Submitted, 2008

The paper presents two terminating tableau systems for hybrid logic with the difference modality. Both systems are based on an abstract treatment of equality. They expand formulas with respect to a congruence closure that is not represented explicitly. The first system employs pattern-based blocking. The second system employs chain-based blocking and covers converse modalities. Both systems can handle transitive relations.

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009