# Publication details

##
Higher-Order Syntax and Saturation Algorithms for Hybrid Logic

Moritz Hardt, Gert Smolka

Electronic Notes in Theoretical Computer Science 174(6):15-27, June 2007

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.

Download PDF
Show BibTeX

@ARTICLE{HardtSmolkaHOSHybrid06,
title = {Higher-Order Syntax and Saturation Algorithms for Hybrid Logic},
author = {Moritz Hardt and Gert Smolka},
year = {2007},
month = {June},
journal = {{Electronic Notes in Theoretical Computer Science}},
volume = {174},
pages = {{15--27}},
number = {6},
note = {{Proceedings of the International Workshop on Hybrid Logic (HyLo 2006)}},
}

Login to edit

Webmaster,
Wed Sep 16 10:47:00 2009