B12. TIME
1. The Topology of Time:
Instants, Intervals, and Temporal Sequences
This development of an ontology of time is a condensation and
abridgement of OWL-Time (Hobbs and Pan, 2004), with some minor
differences.
There are two kinds of temporal entities -- instants and intervals.
(forall (t) (if (instant t) (temporalEntity t))) (1)
(forall (t) (if (interval t) (temporalEntity t))) (2)
No assumptions are made about whether intervals _consist_ of instants.
Rather one can specify relations between the two, such as that an
instant begins or ends or is inside an interval. Later in this
section we will introduce the idea of the time span of an eventuality.
The predicates "begins", "ends", "insideTime" and several others will
allow temporal sequences and eventualities as well as temporal
entities in their second argument positions. Axioms presented below
will specify the coercion from eventualities to their time spans. We
thus include eventualities in the constraints on the arguments of
these predicates.
(forall (t1 t2) (3)
(if (begins t1 t2)
(and (instant t1)
(or (temporalEntity t2)(tseq t2)(eventuality t2)))))
(forall (t1 t2) (4)
(if (ends t1 t2)
(and (instant t1)
(or (temporalEntity t2)(tseq t2)(eventuality t2)))))
(forall (t1 t2) (5)
(if (insideTime t1 t2)
(and (instant t1)
(or (temporalEntity t2)(tseq t2)(eventuality t2)))))
The beginning and end of an instant is itself.
(forall (t1 t2) (6)
(if (and (instant t2)(begins t1 t2))
(equal t1 t2)))
(forall (t1 t2) (7)
(if (and (instant t2)(ends t1 t2))
(equal t1 t2)))
An interval t between two instants t1 and t2 is an interval that
begins at t1 and ends at t2. It will be useful to extend this to
intervals and define it as the interval from the end of t1 to the
beginning of t2.
(forall (t t1 t2) (8)
(iff (intervalBetween t t1 t2)
(exists (t3 t4)
(and (ends t3 t1)(begins t4 t2)
(begins t3 t)(ends t4 t))))
A positively infinite interval is one that has no end.
(forall (t) (9)
(iff (posInfInterval t)
(and (interval t)(not (exists (t2) (ends t2 t))))))
A positively infinite interval may or may not have a beginning. In
the full OWL-Time, negatively infiinite intervals are also defined,
but they will not be needed here.
The ontology is silent about whether there can be intervals of zero
length, but when the beginning and end of an interval are distinct, we
will call it a proper interval. Positive infinite intervals are
regarded as proper intervals; we ignore negative infinite intervals
here.
(forall (t) (10)
(iff (properInterval t)
(or (exists (t1 t2)
(and (begins t1 t)(ends t2 t)(nequal t1 t2)))
(posInfInterval t))))
Time is ordered by a "before" relation that we explicate in Section
3. It is basically a relation between instants, but we can extend it
to intervals in the obvious way. We will use it here in defining
temporal sequences.
A temporal sequence is a set of nonoverlapping temporal entities. In
Hobbs and Pan (2004) we allowed concatenations to be temporal
sequences, and then defined the minimal temporal sequence in which no
two intervals in the set meet. Here we will shortcut past that
wrinkle and define temporal sequences to be minimal. Concatenations
are not allowed. Thus, between any two distinct members of the set
there is another interval or instant that is not in the set.
(forall (s) (11)
(iff (tseq s)
(and (forall (t) (if (member t s)(temporalEntity t)))
(forall (t1 t2)
(if (and (member t1 s)(member t2 s))
(and (or (equal t1 t2)(before t1 t2)
(before t2 t1))
(if (before t1 t2)
(exists (t3)
(and (not (member t3 s))
(before t1 t3)
(before t3 t2))))))))))
Line 3 of this definition says that the members of a temporal sequence
are instants or intervals. Lines 5-7 say they are nonoverlapping.
Lines 8-12 say they have a temporal entity between them that is not in
the temporal sequence.
If there is an element of the temporal sequence before all its other
elements, this is called the "first" element.
(forall (s t) (12)
(if (tseq s)
(iff (first t s)
(and (member t s)
(forall (t1)
(if (member t1 s)
(or (equal t1 t)(before t t1))))))))
If there is an element of the temporal sequence after all its other
elements, this is called the "last" element.
(forall (s t) (13)
(if (tseq s)
(iff (last t s)
(and (member t s)
(forall (t1)
(if (member t1 s)
(or (equal t1 t)(before t1 t))))))))
Note that these axioms do not imply that there really is a first or
last element.
Two elements of a temporal sequence are "successive elements" if there
is no element between them.
(forall (s t1 t2) (14)
(iff (successiveElts t1 t2 s)
(and (member t1 s)(member t2 s)(before t1 t2)
(not (exists (t)
(and (member t s)(before t1 t)
(before t t2)))))))
If the temporal sequence is finite, it can be viewed as a (finite)
sequence in the sense of Chapter B5. In this case, the predicates
"first" and "last" defined here and there are consistent.
The predicate "before" is a partial ordering on the elements of a
temporal sequence.
(forall (e t1 t2 s) (15)
(if (and (tseq s)(before' e t1 t2))
(partialOrdering e t1 t2 s)))
A temporal sequence is scale whose ordering relation is "before".
(forall (s e t1 t1) (16)
(if (and (tseq s)(before' e t1 t2))
(scaleDefinedBy s s e)))
The convex hull of a temporal sequence is the smallest interval
spanning all the members of the temporal sequence. We will define it
here only for the finite case.
(forall (s t1 t2 t3 t4) (17)
(if (and (tseq t)(first t1 s)(begins t3 t1)
(last t2 s)(ends t4 t2))
(forall (t)
(iff (convexHull t s)
(intervalBetween t t3 t4)))))
The three basic relations, "begins", "ends" and "insideTime", can be
extended to cover temporal sequences as well as instants and
intervals.
(forall (t s) (18)
(if (tseq s)
(iff (begins t s)
(exists (t1) (and (first t1 s)(begins t t1))))))
(forall (t s) (19)
(if (tseq s)
(iff (ends t s)
(exists (t1) (and (last t1 s)(ends t t1))))))
(forall (t s) (20)
(if (and (tseq s)(insideTime t s))
(and (not (begins t s))(not (ends t s))
(exists (t1)
(and (member t1 s)
(or (equal t1 t)(insideTime t t1)
(begins t t1)(ends t t1)))))))
(forall (t s) (21)
(if (tseq s)
(if (exists (t1)
(and (member t1 s)
(or (equal t1 t)(insideTime t t1))))
(insideTime t s))))
There are two axioms for "insideTime" to stay neutral about the
beginnings and ends of intervals in the temporal sequence. Axiom (20)
says that if instant t is inside temporal sequence s, it may be the
beginning or end of one of its intervals (but not the beginning or end
of the temporal sequence as a whole). Axiom (21) only guarantees
being inside the temporal sequence if it is _inside_ one of the
intervals; the endpoints of the interval may or may not be inside the
temporal sequence.
2. Relating Eventualities and Time
There are four predicates that relate eventualities to instants and
intervals. The first is "atTime" and it relates an eventuality to an
instant, saying that that eventuality really exists or obtains at that
instant. We state the constraints on its arguments, but we do not
attempt to define it.
(forall (e t) (22)
(if (atTime e t)(and (eventuality e)(instant t))))
The predicate "during" says that the eventuality really exists or
obtains throughout an interval.
(forall (e t) (23)
(iff (during e t)
(and (eventuality e)(interval t)
(forall (t1) (if (insideTime t1 t)(atTime e t1))))))
The theory is silent on whether the eventuality really exists or
obtains at the end points of the interval.
The "timeSpanOf" of an eventuality encompasses all the instants and
intervals for which it really exists or obtains. The time span may be
an instant, an interval, or a temporal sequence.
(forall (t e) (24)
(iff (timeSpanOf t e)
(or (and (instant t)(atTime e t)
(forall (t1)
(if (nequal t1 t)(not (atTime e t1)))))
(and (interval t)(during e t)
(forall (t1)
(if (atTime e t1)
(or (insideTime t1 t)(begins t1 t)
(ends t1 t)))))
(and (tseq t)
(forall (t1)
(if (and (member t1 t)(instant t1))
(atTime e t1)))
(forall (t1)
(if (and (member t1 t)(interval t1))
(during e t1)))
(forall (t1)
(if (and (instant t1)(atTime e t1))
(or (member t1 t)
(exists (t2)
(and (interval t2)(member t2 t)
(or (begins t1 t2)
(insideTime t1 t2)
(ends t1 t2)))))))))))
This definition is complicated only because there are several cases to
capture. In lines 3-5, if the time span is an instant, then the
eventuality really exists at that instant and no others. In lines
6-10, if the time span is an interval, the eventuality really exists
at every instant inside the interval and at no instants that are
outside it. Lines 11-25 cover the case where the time span is a
temporal sequence. The eventuality is happening at every instant in
the temporal sequence (lines 12-14), and during every interval in the
temporal sequence (lines 15-17). Lines 18-25 say that any instant at
which the eventuality is happening (line 19) must be an instant in the
temporal sequence (line 20) or in an interval in the temporal sequence
(lines 21-25).
We will say that an eventuality "happens in" a temporal entity or
sequence if its time span is entirely included in the temporal entity
or sequence.
(forall (e t) (25)
(iff (happensIn e t)
(exists (t1)
(and (timeSpanOf t1 e)
(forall (t2)
(if (or (begins t2 t1)(insideTime t2 t1)
(ends t2 t1))
(or (begins t2 t)(insideTime t2 t)
(ends t2 t))))))))
The three basic relations of Section 1 can now be extended to
eventualities as well.
(forall (t e) (26)
(if (eventuality e)
(iff (begins t e)
(exists (t1)(and (timeSpanOf t1 e)(begins t t1))))))
(forall (t e) (27)
(if (eventuality e)
(iff (insideTime t e)
(exists (t1)
(and (timeSpanOf t1 e)(insideTime t t1))))))
(forall (t e) (28)
(if (eventuality e)
(iff (ends t e)
(exists (t1)(and (timeSpanOf t1 e)(ends t t1))))))
The predicate "posInfIntervalEv" says that its argument is either a
positive infinite interval or an eventuality whose time span is a
positive infinite interval.
(forall (e) (29)
(iff (posInfIntervalEv e)
(or (posInfInterval e)
(exists (t)
(and (timeSpanOf t e)(posInfInterval t))))))
The predicate "properIntervalEv" says that its argument is either a
proper interval or an eventuality whose time span is a proper
interval.
(forall (e) (30)
(iff (properIntervalEv e)
(or (properInterval e)
(exists (t)
(and (timeSpanOf t e)(properInterval t)))
(posInfIntervalEv e))))
It will be useful to have a category for the relations "atTime",
"during", "timeSpanOf", "happensIn", and several other predicates when
we are axiomatizing scheduling. We will call them "temporal".
(forall (e0 e t)(if (atTime' e0 e t)(temporal e0))) (31)
(forall (e0 e t)(if (during' e0 e t)(temporal e0))) (32)
(forall (e0 e t)(if (timeSpanOf' e0 t e)(temporal e0))) (33)
(forall (e0 e t)(if (happensIn' e0 e t)(temporal e0))) (34)
A nontemporal eventuality is one that isn't temporal.
(forall (e) (iff (nontemporal e)(not (temporal e)))) (35)
Temporal properties are ones that say something about when an
eventuality occurs.
3. Temporal Ordering and Interval Relations
Instants are at least partially ordered by a "before" relation. The
"before" relation will also be extended to intervals, temporal
sequences, and eventualities, so the constraints on its arguments are
as follows:
(forall (t1 t2) (36)
(if (before t1 t2)
(and (or (temporalEntity t1)(tseq t1)(eventuality t1))
(or (temporalEntity t2)(tseq t2)(eventuality t2)))))
The ontology is silent about whether time is linearly ordered. In the
full OWL-Time, one can assert a single proposition to enable the axiom
for linear ordering. We will not require linear ordering in this
book.
The beginning of a proper interval is before the instants inside,
which are before the end.
(forall (t1 t2 t3 t) (37)
(if (properIntervalEv t)
(and (if (and (begins t1 t)(ends t3 t))
(before t1 t3))
(if (and (begins t1 t)(insideTime t2 t))
(before t1 t2))
(if (and (insideTime t2 t)(ends t3 t))
(before t2 t3)))))
The beginning of a positive infinite interval, if there is one, is
before all the instants inside it.
(forall (t1 t2 t) (38)
(if (and (posInfInterval t)(begins t1 t)(insideTime t2 t))
(before t1 t2)))
The "before" relation is antireflexive.
(forall (t) (not (before t t))) (39)
It is antisymmetric.
(forall (t1 t2) (40)
(if (before t1 t2)
(not (before t2 t1))))
It is transitive.
(forall (t1 t2 t3) (41)
(if (and (before t1 t2)(before t2 t3))
(before t1 t3)))
Allen and Kautz (1985) and Allen and Ferguson (1997) describe an
algebra of relations between intervals. We will use four of them, and
define them in terms of "begins", "ends" and "before". These
relations hold only between proper intervals or eventualities that
have proper intervals as time spans.. The predicate "intMeets" means
that the end of one interval is the beginning of the other.
(forall (t1 t2) (42)
(iff (intMeets t1 t2)
(and (properIntervalEv t1)(properIntervalEv t2))
(exists (t) (and (ends t t1)(begins t t2)))))
Two intervals overlap if the beginning of one is inside the other.
(forall (t1 t2) (43)
(iff (intOverlap t1 t2)
(and (properIntervalEv t1)(properIntervalEv t2))
(exists (t)
(or (and (begins t t1)(insideTime t t2))
(and (begins t t2)(insideTime t t1))))))
Note that this predicate subsumes both Allen's "overlaps" relation and
its inverse.
One interval finishes the other if it begins inside and ends the same
place. We have to complicate this relation a bit to accommodate
positive infinite intervals.
(forall (t1 t2) (44)
(iff (intFinishes t1 t2)
(and (properIntervalEv t1)(properIntervalEv t2)
(exists (t3 t4)
(and (begins t3 t1)(begins t4 t2)(before t4 t3)))
(or (exists (t)
(and (ends t t1)(ends t t2)))
(and (posInfIntervalEv t1)
(posInfIntervalEv t2))))))
One interval t1 is during another t2 if t1 begins after t2 and ends
before t2. The conditional in the last line of the definition is to
accommodate positive infinite intervals.
(forall (t1 t2) (45)
(iff (intDuring t1 t2)
(and (properIntervalEv t1)(properIntervalEv t2)
(exists (t3 t4)
(and (begins t3 t1)(begins t4 t2)(before t4 t3)))
(exists (t5)
(and (ends t5 t1)
(forall (t6)
(if (ends t6 t2)(before t5 t6))))))))
We can also extend the "before" relation from instants to intervals,
temporal sequences, and eventualities; one of them is before another
if the first's end is before the second's beginning.
(forall (t1 t2) (46)
(iff (before t1 t2)
(exists (t3 t4)
(and (ends t3 t1)(begins t4 t2)(before t3 t4)))))
This axiom allows us to use instant, interval, temporal sequence, and
eventuality arguments in the "before" relation and to reduce all
"before" judgments to judgments about instants.
We will sometimes have occasion to talk about one temporal entity
being before or meeting another. We will define the predicate
"beforeOrMeets" as follows:
(forall (t1 t2) (47)
(iff (beforeOrMeets t1 t2)
(exists (t3 t4)
(and (ends t3 t1)(begins t4 t2)
(or (before t3 t4)(equal t3 t4))))))
Note that this also covers the case where t1 is the instant that
begins t2.
Time is a scale whose ordering relation is "before" and whose
components are instants and intervals.
(forall (t) (48)
(iff (timeScale t)
(exists (s e t2 t3)
(and (forall (t1)
(iff (member t1 s)
(or (instant t1)(interval t1))))
(before' e t2 t3)
(scaleDefinedBy t s e)))))
Since all the elements in a time scale are temporal entities, a time
scale can be viewed as a possible ground.
(forall (t) (if (timeScale t)(ground t))) (49)
Then "atTime" can be viewed as an "at" relation.
(forall (s e t) (50)
(if (and (timeScale s)(atTime e t s)(inScale t s))
(at e t s)))
It is because of this metaphor that we can, for example, speak of
moving a meeting from one time to another.
The notions of change and causality are probably prior to time in
evolution and in individual development, and our ideas about time
probably arise out of these prior notions. In a way, we can think of
time as an idealized sequence of events or changes, say, the ticks of
a clock in some Platonic National Bureau of Standards in the sky. It
is not necessary to adopt this view of time, but it is important to
relate the fundamental notions of "change" and "cause" with the notion
of "before". The constraint for change is that final states can't
happen before initial states.
(forall (e1 e2) (51)
(if (change e1 e2)(not (before e2 e1))))
An effect cannot happen before its cause.
(forall (e1 e2) (52)
(if (cause e1 e2)(not (before e2 e1))))
A similar rule holds for enablement
(forall (e1 e2) (53)
(if (enable e1 e2)(not (before e2 e1))))
These axioms leave open the possibility of instantaneous change and
causality.
We can state stronger relations between causal predicates and
"before". In fact, we are now able to state one of the two principal
properties causal complexes, that if all the eventualities in the
causal complex happen or hold, then the effect will happen or hold.
Moreover, the effect is not before the elements of the causal
complex.
(forall (s e t1) (54)
(if (and (causalComplex s e)
(forall (e1)(if (member e1 s)(atTime e1 t1))))
(exists (t2)
(and (not (before t2 t1))(atTime e t2)))))
There is a similar, defeasible, rule for "cause".
(forall (e1 e2 t1) (55)
(if (and (cause e1 e2)(atTime e1 t1)(etc))
(exists (t2)
(and (not (before t2 t1))(atTime e2 t2)))))
This axiom is a kind of causal modus ponens; if e1 happens and e1
causes e2, then e2 happens. The "etc" condition is that all the
other, presumable or nonproblematic, eventualities in the causal
comples happen or hold. The relation "before" is temporal.
(forall (e t1 t2)(if (before' e t1 t2)(temporal e))) (56)
4. Durations
There are two ways we could introduce measures of the duration of
intervals.
The first is to map the time scale directly to the real numbers, and
define duration in terms of the difference between the numbers that
the beginning and end of the interval are mapped to.
The second is to introduce a relation of "sameDuration" between
intervals and to stipulate that certain intervals are standard
durations, called "temporal units". Then any hour-long interval has
the same duration as the standard hour. Durations of arbitrary
intervals are then defined in terms of concatenations of unit-duration
intervals.
We will take the second approach since it is probably closer to the
way the notion of duration arose in evolution and arises in individual
development.
We will assume that people can make the judgment that two intervals
are of the same duration. The predicate "sameDuration" basically
applies to intervals, but trivially every instant is of the same
duration, namely, zero. So the constraints on the argument of
"sameDuration" are that its arguments are temporal entities.
(forall (t1 t2) (57)
(if (sameDuration t1 t2)
(and (temporalEntity t1)(temporalEntity t2))))
(forall (t1 t2) (58)
(if (and (instant t1)(instant t2))
(sameDuration t1 t2)))
The predicate "sameDuration" is reflexive, symmetric, and transitive.
(forall (t) (sameDuration t t)) (59)
(forall (t1 t2) (60)
(iff (sameDuration t1 t2)(sameDuration t2 t1)))
(forall (t1 t2 t3) (61)
(if (and (sameDuration t1 t2)(sameDuration t2 t3))
(sameDuration t1 t3)))
We will take temporal units to be arbitrary intervals on the time
scale. In a sense, the standard hour will be some hour-long interval,
but we will never know exactly which hour-long interval it is. We
will then say another interval has a duration of an hour if it has the
same duration as the standard hour. The only property of
"temporalUnit" that we can state is that it is an interval.
(forall (u) (62)
(if (temporalUnit u)(interval u)))
The full OWL-Time ontology describes the relations among different
temporal units, e.g., that a minute is sixty seconds. But we will not
need that knowledge here.
A proper interval is a concatenation of a set of proper intervals if
every instant inside the interval is inside, the beginning or the end
of some interval in the set and the intervals in the set are
nonoverlapping. We will only deal with concatenation of finite
intervals.
(forall (t s) (63)
(iff (concatenation t s)
(and (properInterval t)
(forall (t1)(if (member t1 s)(properInterval t1)))
(exists (t1 t2)
(and (begins t1 t)(member t2 s)(begins t1 t2)))
(exists (t1 t2)
(and (ends t1 t)(member t2 s)(ends t1 t2)))
(forall (t1)
(if (insideTime t1 t)
(exists (t2)
(and (member t2 s)
(or (insideTime t1 t2)(begins t1 t2)
(ends t1 t2))))))
(forall (t1 t2)
(if (and (member t1 s)(member t2 s))
(or (equal t1 t2)(not (intOverlap t1 t2))))))))
Line 4 says that s is a set of proper intervals. Lines 5-6 say that
one of those intervals begins with the beginning of t. Lines 7-8 say
that one of those intervals ends with the end of t. Lines 9-14 say
that any instant inside t is inside some member of s. Lines 15-17 say
that the members of s are nonoverlapping.
The predication "(durationOf d t u)" says that t is made up of d
intervals having the same duration as u. We will allow the second
argument to be an instant, an interval, a temporal sequence, or an
eventuality.
(forall (d t u) (64)
(if (durationOf d t u)
(and (nonNegInteger d)(temporalUnit u)
(or (temporalEntity t)(tseq t)(eventuality t)))))
The duration of an instant is zero.
(forall (d t u) (65)
(if (instant t)(durationOf 0 t u)))
The duration of an interval is determined by concatenation.
(forall (d t u) (66)
(if (interval t)
(iff (durationOf d t u)
(exists (s)
(and (concatenation t s)
(forall (t1)
(if (member t1 s)(sameDuration t1 u)))
(card d s))))))
The duration of a temporal sequence is the sum of the durations of its
members. We define this recursively.
(forall (s u) (67)
(if (null s)(durationOf 0 s u)))
(forall (s s1 t u d d1 d2) (68)
(if (and (tseq s)(tseq s1)(not (member t s1))(addElt s s1 t)
(durationOf d1 s1 u)(durationOf d2 t u)(sum d d1 d2))
(durationOf d s u)))
The duration of an eventuality is the duration of its time span.
(forall (d e u) (69)
(if (eventuality e)
(iff (durationOf d e u)
(exists (t)
(and (timeSpanOf t e)(durationOf d t u))))))
We have stipulated that the relevant intervals are integer multiples
of the temporal unit u. This is harmless. In Hobbs and Pan (2004) we
define the arithmetic relations among the various temporal units,
allowing us to convert from one to the other and thus to talk about
fractional durations. We can always pick our original unit to be
small enough (e.g., microsecond) that for all practical purposes the
intervals _are_ integer multiples of the unit. We can then apply the
arithmetic relations among units to get a fractional duration in a
more convenient unit.
The predicate "durationOf" is temporal.
(forall (e d t u) (70)
(if (durationOf' e d t u)(temporal e)))
5. Periodicity
A temporal sequence is periodic if there is a constant duration
between any two successive temporal entities in the temporal
sequence.
(forall (s) (71)
(iff (periodicTseq s)
(and (tseq s)
(exists (d u)
(forall (t1 t2)
(if (successiveElts t1 t2 s)
(exists (t)
(and (intervalBetween t t1 t2)
(durationOf d t u)))))))))
The constant duration in a periodic temporal sequence can be called
the "gap duration".
(forall (s d t1 t2 t n1 n2 u) (72)
(if (and (periodicTseq s)(successiveElts t1 t2 s)
(temporalUnit u)(intervalBetween t t1 t2))
(iff (gapDuration d s u)(durationOf d t u))))
Sometimes in commonsense reasoning, it is too stringent a requirement
that the gap between two elements of a temporal sequence be exactly
equal. It is enough that they be roughly equal, that is, that they
be of the same half order of magnitude. We define the notion of
"roughly periodic temporal sequences" to cover this case. This has to
be with respect to a granularity defined by a temporal unit.
(forall (s) (74)
(iff (roughlyPeriodicTseq s u)
(and (tseq s)(temporalUnit u)
(exists (d)
(forall (t1 t2 t3 t4)
(if (and (successiveElts t1 t2 s)
(successiveElts t3 t4 s))
(exists (t12 t34 e d)
(and (intervalBetween t12 t1 t2)
(intervalBetween t34 t3 t4)
(durationOf' e d t12 u)
(sameHOM t12 t34 e))))))))
Lines 5-10 pick out the intervals between two pairs of arbitrary
successive elements of the temporal sequence. Line 11 says that they
will be measured by the "durationOf" function with respect to u. Line
12 says that they are of the same half order of magnitude under this
function.
6. Rates and Frequency
We would like to define a notion of "rate" that will cover the
following cases, among others:
He was driving 60 miles per hour.
We have 3 meetings every 4 1/2 months.
I see 4 students a day.
We discuss three topics every meeting.
In the most primitive case, there is a set S of events. In our four
examples, the events are driving a mile, having a meeting, seeing a
student, and discussing a topic. There is also a set T of time
intervals that may or may not be all of equal duration. In the first
three examples, the durations are one hour, 4 1/2 months, and one day.
In the fourth example, the length of the meetings may differ. There
is a function mapping the intervals into a subset of S, namely, those
events that occur during that interval. If the concept of "rate"
applies truly, the cardinalities of all these subsets are the same.
This analysis provides us with all we need to define the primitive
case. The concept of "rate" will be extended beyond this below, so
here we use "if" rather than "iff".
(forall (s s0 t d u f n) (74)
(if (and (eventualities s)(set t)(powerSet s0 s)
(forall (t1)
(if (member t1 t)(interval t1)))
(function f t s0)
(forall (t1 s1)
(if (map f t1 s1)
(and (forall (e)
(if (member e s1)(happensIn e t1)))
(card n s1)))))
(rate n s t)))
Lines 3-4 say that t is a set of intervals. Lines 5-10 say that the
same number n of events in s happen during each of those intervals.
Line 11 says that n is the rate of the events happening in the
intervals in t.
Next we extend the definition to the case where the third argument of
"rate" is a temporal unit, by assuming that the members of t all have
a duration of one in that unit.
(forall (n s t u) (75)
(if (and (eventualities s)(temporalUnit u)
(forall (t1)(if (member t1 t)(durationOf 1 t1 u)))
(rate n s t))
(rate n s u)))
Finally, we extend "rate" to units which are not the duration of the
temporal intervals on which the events were measured, allowing us to
say "He was driving 60 miles per hour," even though he was only
driving at that rate for five minutes.
(forall (r1 r2 s u1 u2 j) (76)
(if (and (rate r1 s u1)(product r2 j r1)
(forall (t n1 n2)
(iff (and (durationOf n1 t u1)(durationOf n2 t u2))
(product n1 j n2))))
(rate r2 s u2)))
Lines 3-5 define j as the ratio between the two units. For example,
if u1 is minutes, u2 is hours, and n2 is 10, i.e., t is 10 hours, then
n1 is 600, and j is 60. Thus, if someone is going 4 miles a minute
(r1 = 4), then they are going 240 miles an hour (r2 = 60*4 = 240).
Rate defines a scale, whose elements are the sets of events whose rate
is being measured and whose ordering is the "less than" relation
between rates.
(forall (s s0) (77)
(iff (rateScale s s0)
(and (forall (s1)(if (member s1 s0)(eventualities s1)))
(exists (u e s1 s2)
(and (temporalUnit u)(lts' e s1 s2 s0)
(forall (s3 s4)
(iff (and (lts' e s3 s4 s0)(Rexist e))
(exists (r1 r2)
(and (rate r1 s3 u)(rate r2 s4 u)
(lt r1 r2)))))
(scaleDefinedBy s s0 e))))))
Here, s is a "rate scale" for the set s0 of sets of eventualities.
Line 3 says that s0 is a set of sets of eventualities. Lines 4-10
define e as the ordering relation on sets of eventualities in terms of
their rates. Line 11 says that s is the scale whose elements are s0
and whose ordering relation is e.
A set of events is "frequent" if it is in the Hi region of a rate
scale.
(forall (s1) (78)
(iff (frequent s1)
(exists (s s0 s2)
(and (member s1 s0)(rateScale s s0)(Hi s2 s)
(inScale s1 s2)))))
Here, s1 is a set of eventualities. It is being compared with other
sets of eventualities with respect to rate. The entire set of these
sets of eventualities is s0. The scale s is the rate scale for s0.
The subscale s2 is the Hi region of s. The set s1 of eventualities is
frequent if it is in s2.
Recalling the discussion of Section B8.4, by saying that some set of
eventualities is in the Hi region of a rate scale, we are defeasibly
implying that it lies in the upper end of a distribution of such
rates, and that its high rate plays some causal role in someone's
goals.
Predicates Introduced in this Chapter
(instant t): t is an instant of time.
(interval t): t is an interval of time.
(temporalEntity t): t is an instant or an interval.
(begins t1 t2): Instant t1 is the beginning of t2.
(ends t1 t2): Instant t1 is the end of t2.
(insideTime t1 t2): Instant t1 is inside t2.
(intervalBetweeen t t1 t2): t is the interval between t1 and t2.
(posInfInterval t): t is a positive infinite interval.
(properInterval t): The beginning and end of interval t are
distinct.
(tseq s): s is a sequence of temporal entities.
(first t s): t is the first temporal entity in temporal
sequence s.
(last t s): t is the last temporal entity in temporal
sequence s.
(successiveElts t1 t2 s): t1 is immediately followed by t2 in
temporal sequence s.
(convexHull t s): Interval t is the convex hull of temporal
sequence s.
(atTime e t): Eventuality e is occurring at instant t.
(during e t): Eventuality e is occurring at every instant
inside interval t.
(timeSpanOf t e): Temporal entity or sequence t is all the
instants and intervals for which
eventuality e really exists or obtains.
(happensIn e t): t subsumes the time span of e.
(posInfIntervalEv e): e is a positive infinite interval or an
eventuality whose time span is a positive
infinite interval.
(properIntervalEv e): e is a proper interval or an eventuality
whose time span is a proper interval.
(temporal e): e is a temporal property, i.e., "atTime",
"during", "timeSpanOf", "happensIn",
"before", or "durationOf".
(nontemporal e): e is not a temporal property.
(before t1 t2): t1 is before t2.
(intMeets t1 t2): Interval t1 meets interval t2.
(intOverlaps t1 t2): Intervals t1 and t2 overlap.
(intFinishes t1 t2): Interval t1 begins inside interval t2, and
their ends are the same.
(intDuring t1 t2): Interval t1 begins after and ends before
interval t2.
(beforeOrMeets t1 t2): The end of t1 is before or equal to the
beginning of t2.
(timeScale t): t is a scale whose elements are temporal
entities and whose ordering is "before".
(sameDuration t1 t2): Temporal entities t1 and t2 have the same
duration.
(temporalUnit u): Interval u is a temporal unit.
(concatenation t s): Interval t is the concatenation of the
intervals in the set s.
(durationOf d t u): The duration of t is d units u.
(periodicTseq s): Temporal sequence s is periodic, in that the
gaps between successive elements are all
equal.
(gapDuration d s u): d is the duration of the equal gaps in
periodic temporal sequence s measured in
units u.
(roughlyPeriodicTseq s): Temporal sequence s is roughly periodic, in
that the gaps between successive elements
are all the same half order of magnitude.
(rate n s t): Eventualities in s occur n times in every
element of t, if t is a set of intervals
of equal length, or in every interval of
duration u if u is a temporal unit.
(rateScale s s0): s is a scale whose elements are the sets of
eventualities in s0 and whose ordering is
the rate of the sets.
(frequent s1): Set s1 of eventualities is in the high
region of a rate scale.
References:
Allen, James F., and George Ferguson, 1997. ``Actions and Events in
Interval Temporal Logic'', in O. Stock (ed.), {\it Spatial and
Temporal Reasoning}, Kluwer Academic Publishers, Dordrecht,
Netherlands, pp. 205-245.
Allen, James F., and Henry A. Kautz. 1985. ``A Model of Naive Temporal
Reasoning'', {\it Formal Theories of the Commonsense World}, ed. by
Jerry R. Hobbs and Robert C. Moore, Ablex Publishing Corp., pp. 251-268.
Hobbs, Jerry R., and Feng Pan, 2004. ``An Ontology of Time for the
Semantic Web'', ACM Transactions on Asian Language Information
Processing, Vol. 3, No. 1, March 2004.