The logic of time representation
Peter Bernard Ladkin, Ralph McKenzie · 1987
This investigation concerns representations of time by means of intervals, stemming from work of Allen [All83] and van Benthem [vBen83]. Allen described an Interval Calculus of thirteen binary relations on convex intervals over a linear order (the real numbers). He gave a practical algorithm for checking the consistency of a subclass 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 an...