A new modal approach to the logic of intervals

In Artificial Intelligence there is a need for reasoning about continuous processes, where assertions refer to intervals rather than time points. Taking our lead from van Benthem's treatment of interval temporal structures Halpern and Shoham's work on intervals, we present a interval temporal logic with two binary relations, and inclusion. We study the logic in its full generality without making any assumptions about the underlying of time, be it discrete or dense, linear or branching. We identify two general classes of interval temporal minimal interval structures and van Benthem minimal interval structures. We show that in our interval language, the two classes in fact have the same logic. We go on to prove that the logic of minimal interval complete and decidable, possessing the finite model property, and that the satisfiability problem is complete. In order to establish the complexity result we extend the tableau method introduced by Horrocks et which treats transitive and inverse relations only, to also incorporate interaction between relations. We go identify some important limitations in the expressive power of our logic, before concluding the paper by number of interesting questions that follow from our work.