Higher-Order Syntax and Saturation Algorithms for Hybrid Logic

We present modal logic on the basis of the simply typed lambda calculus with a system of equational deduction. Combining first-order quantification and higher-order syntax, we can maintain modal reasoning in terms of classical logic by remarkably simple means. Such an approach has been broadly uninvestigated, even though it has notable advantages, especially in the case of Hybrid Logic. We develop a tableau-like semi-decision procedure and subsequently a decision procedure for an alternative characterization of HL(@), a well-studied fragment of Hybrid Logic. With regards to deduction, our calculus simplifies in particular the treatment of identities. Moreover, labeling and access information are both internal and explicit, while in contrast traditional modal tableau calculi either rely on external labeling mechanisms or have to maintain an implicit accessibility relation by equivalent formulas. With regards to computational complexity, our saturation algorithm is optimal. In particular, this proves the satisfiability problem for HL(@) to be in PSPACE, a result that was previously not achieved by the saturation approach.