Much previous work in artificial intelligence has neglected representing time in all its complexity. In particular, it has neglected continuous change and the indeterminacy of the future. To rectify this, I have developed a first‐order temporal logic, in which it is possible to name and prove things about facts, events, plans, and world histories. In particular, the logic provides analyses of causality, continuous change in quantities, the persistence of facts (the frame problem), and the relationship between tasks and actions. It (...) may be possible to implement a temporal‐inference machine based on this logic, which keeps track of several “maps” of a time line, one per possible history. (shrink)

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. (shrink)