Lightweight hybrid tableaux (Q631086)

The paper presents a decision procedure for some fragments of the hybrid logic. The main difference between hybrid logic and modal logic is the presence of nominals, which are propositional symbols true at exactly one world in a model. The decision procedure is based on a prefixed tableau calculus. The general idea of the termination proof of this system is that, on the one hand, the quasi-subformula property guarantees that a given prefix can only make true finitely many formulas and, on the other hand, there can only be finitely many prefixes in a branch of the tableau.