Abstract

This investigation concerns representations of time by means of intervals, stemming from work of Allen and van Benthem . Allen described an Interval Calculus of thirteen binary relations on convex intervals over a linear order . He gave a practical algorithm for checking the consistency of a sublclass of Boolean constraints. ;First, we describe a completeness theorem for Allen's calculus, in its corresponding formulation as a first-order theory LM. LM is countably categorical, and axiomatises the complete theory of intervals over a dense unbounded linear order. Its only countable model up to isomorphism is the non-trivial intervals over the rational numbers. ;Algorithms are given for quantifer-elimination, consistency checking, and satisfaction of arbitrary first-order formulas in the Interval Calculus. ;A natural countable model of the calculus is presented, the TUS, in which clock- and calendar-time may be represented in a straightforward way. ;Allen and Hayes described a first-order theory of intervals in . It is shown that the models of the theory are precisely the interval structures over an arbitrary unbounded linear order. ;An extension of the calculus to intervals which are union-of-convex is considered, introduced by concerns over the represention of interruptible processes. A taxonomy of necessary relations between union-of-convex intervals is given, and it is considered how to generalise to arbitrary non-convex intervals. Use of the extension is illustrated with an example of synthesising concurrent processes from high-level specifications. ;The extended calculus may be implemented in a high-level system with logic programming and data-types of sequence and set, and this feature is illustrated with a partial implementation of the TUS in such a system