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