Models of Axioms for Time Intervals

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 6

Planning

James Allen and Pat Hayes have considered axioms expressed in first-order logic for relations between time intervals [AllHay85, AllHay87.1, AllHay87.2]. One important consequence of the results in this paper is that their theory is decidable [Lad87.4]. In this paper, we characterise all the models of the theory, and of an important subtheory. A model is isomorphic to an interval structure INT(S) over some unbounded linear order S, and conversely, INT(S), for or an arbitrary unbounded linear order S, is a model. The models of the subtheory are similar, but with an arbitrary number of copies of each interval (conversely, all structures of this form are models). We also show that one of the original axioms is redundant, and we exhibit an additional axiom which makes the Allen-Hayes theory complete and countably categorical, with all countable models isomorphic to INT(Q), the theory of intervals with rational endpoints, if this is desired. These results enable us to directly compare the Allen-Hayes theory with the theory of Ladkin and Maddux [LadMad87.1], and of van Benthem [vBen83].