Altaf Hussain

Application of Hybrid Logic to Intervals

We define an interval hybrid language with two relations: precedence and inclusion. We identify a minimal interval structure as the most basic interval structure. For technical reasons, we also identify a weaker class of structures called pre-interval structures. We then give a tableau calculus that is sound and complete for the class of minimal interval structures. In order to establish the decidability of our logic, we first prove a general truth lemma stating, if any formula is satisfiable in a model based on a minimal interval structure, then it is satisfiable in a finite model based on a pre-interval structure. We then show how a minimal interval structure can be obtained from such a finite model by developing a bulldozing technique that handles the interaction of the relations, and the presence of nominals. We then prove that the complexity of the satisfiability problem for our logic is EXPTIME-complete. Time permitting, we will conclude by showing that the incorporation of the \downarrow binder to our language gives rise to undecidability.