Satisfying First-Order Constraints about Time Intervals

James Allen defined a calculus of time intervals in [A1183], as a representation of temporal knowledge that could be used in AI. We shall call this the Interval Culculus. In his paper, Allen investigated specification and constraint satisfaction in the Interval Calculus. Other constraintsatisfaction algorithms for intervals have considered subclasses of Boolean formulas only. The methods herein extend consistency-checking and constraint-satisfaction procedures to finitely many arbitrary quantified formulas in the Interval Calculus. We use a first-order theory from [LadMad87. 1, LadMad88. 11, that precisely corresponds to Allen’s calculus. We show that every first-order constraint expressible in this theory is equivalent to a Boolean constraint of a particular restricted form. We use this result to obtain a procedure for detecting consistency of arbitrary quantified formulas, and finding intervals that satisfy arbitrary consistent formulas of the Interval Calculus.

Authors

• Peter B. Ladkin

Keywords

No keywords are indexed for this paper.