Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

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               

@TECHREPORT{KaminskiSmolka08equality,
  title = {Terminating Tableau Systems for Modal Logic with Equality},
  author = {Mark Kaminski and Gert Smolka},
  year = {2008},
  address = {{Campus E1 3, 66123 Saarbrücken, Germany}},
  institution = {{Saarland University}},
  note = {{Submitted}},
}

Login to edit