To:  "[ontologforum] " <ontologforum@xxxxxxxxxxxxxxxx> 

From:  Pat Hayes <phayes@xxxxxxx> 
Date:  Tue, 29 Jan 2008 00:41:11 0600 
Messageid:  <p06230912c3bd813c4fb9@[10.100.0.14]> 
This is the a simple basic time ontology with a few possible
extensions, adapted from my old 'catalog', modified and simplified and
transcribed into CL from KIF. It might give us something more concrete
to discuss.
Intuitions
The basic notions are timeinterval, timepoint
and duration.
Durations form a group under addition (operator ++ with
identity zero), can be multiplied by integers, and are ordered
by >. They are measures of amounts of time, like 20 seconds
or three years.
A timeinterval is a particular chunk of time, such as from 3
to 5 pm GMT on 25 December 2007. Note, a timeinterval need not be
an interval in the conventional mathematical sense, i.e. a set of real
numbers.
Timepoints are the places where timeintervals meet, and which
they have at their ends. (It turns out that these two ways of defining
points are interconvertible, so we might as well use both.) Timepoints
have zero duration, and are totally ordered by before.
Order
(forall (x y z)(and
(if (and (before x y)(before y z))(before x
z))
(if (before x y)(not (before y x)))
))
Timeintervals have exactly two associated timepoints, one at each
end, called the begin and end of the interval. A
meets B when the end of A is the same as the begin of B. Two
timepoints x and y with x before y define a unique interval
from them. There are some obvious identities:
BEF
(forall (x y i)(and
(= x (begin (from x y)))
(= y (end (from x y)))
(= i (from (begin i)(end i)))
))
Its easy to define the Allen relations by conjunctions of
conditions on the ordering of the endpoints. For completeness, these
are their definitions:
Allen
(forall ((i timeinterval)(j timeinterval))(and
(iff (before i j)(before (end i)(begin
j)))
(iff (meets i j)(= (end i)(begin j)))
(iff (overlaps i j)(and (before (begin i)(begin
j))
(iff (starts i j)(and (= (begin i)(begin
j))(before (end i)(end j)) ))
(iff (inside i j)(and (before (begin j)(begin
i))(before (end i)(end j)) ))
(iff (ends i j)(and (before (begin i)(begin j))(=
(end i)(end j)) ))
))
plus their inverses (permute the arguments) and equality, makes
13.
Its useful to extend inside to also apply between a point
and an interval:
Inside
(forall (p (i timeinterval))(iff (inside p i)
(and (before (begin i)
p)(before p (end i)) )
))
There are three basic assumptions about duration:
BD1
(forall (p q)(iff (before p q)(> (duration (from p q))
zero) ))
BD2
(forall ((p timepoint)(= (duration p) zero) )
BD3
(forall (p q r)(if (= (duration (from p q))(duration (from p
r))) (= q r) ))
Note, BD3 rules out branching futures. The ordering assumptions
rule out circular models of time. However, this theory so far is
seriously agnostic:
= time can be dense or discrete or continuous (or indeed any
combination of these, or something else entirely)
= time can be finite or infinite, in either direction
= points can be distinct from intervals, or not
= a timeinterval can be identified with a set of points, or not;
and if it is, it can be an open or a closed or a clopen set.

First extension: clocks
A clock is a set of intervals called ticks, each meeting
the next and all having the same duration, called the period of
the clock. (This is a simple clock which has no provision for leap
seconds and other exotica, or for having its rate reset. Those can be
modelled as sequences of simple clocks.) The time of a point according
to a clock is the number of ticks in the set which end at or before
the point. As the logic provides no way to speak of numbers of points
in a sequence or a set, we will assume that there is a tick
function from the clock and natural numbers to ticks which gives the
clock time directly, so that (tick c n) is the nth tick
of c. (This description takes the natural numbers and simple
operations on them  in particular, addition  for granted, which we
will do from now on without further comment. In practice, of course,
we mean the elements of any some model of the arithmetic axioms which
are in use. Number is true of all and only the natural
numbers.)
Notation: (tick c) is a predicate true of all ticks of the
clock c, and (time c) is the function from timepoints to clock
times according to the clock c.
CLOCK
(forall ((c Clock))(and
(forall (x)(iff ((tick c) x)(exists ((n
Number))(= x (tick c n))) ))
(forall (x)(if ((tick c) x) (= (duration
x)(period c)) ))
(forall ((n Number))(meets (tick c n)(tick
c (+ n 1))
(forall ((p timepoint) n)(iff
(= ((time c)
p) n)(or (= p (end(tick c n)))
(inside p (tick c (plus n 1)))
)) ))
))
Given this, things like changes of the base time of a clock, or
conversions of one clock to another, are left as exercises for the
reader :)
Clock times which are more structured than simple integers, such
as hours/minutes/seconds, can usually be viewed as alternative
notations for integers, e.g. on a 24hour 1second period clock which
repeats each day, H:M:S is a notation for (3600*H)+(60*M)+S. Notice
that according to the above, such a clock is replaced at midnight by a
new clock. A repeating clock is a clock (eg a day count from Jan 1)
with every tick (eg a day) itself inhabited by a clock, so that the
begin of tick one of the inner clock is the begin of this tick of the
outer clock.
This whole scheme works well for days and smaller intervals, and
for years and longer intervals, but it does not work for months.
Months are a royal PITA. In the time catalog I invented one way to
handle them, but I think the way that Jerry Hobbs handles them in the
DAML/OWLtime ontology is better: his 'hath' function (as in '30 days
hath September'.) Using this, one can treat each month as a
[daytick/secondclick] repeating clock.
As the above illustrates, these basic time axioms are sufficient
to define and derive the basic properties of quite a lot of 'temporal'
phenomena in everyday life. However, they can be extended in various
ways to conform to various intuitions about the basic structure of the
timeline.

One whole class of extensions turn on the notion of a 'moment',
by which I mean an interval which is not a point, but is a smallest
possible interval, i.e. it has no points inside it, only
endpoints.
Moment
(forall ((i timeinterval))(iff (moment i)(forall ((p
timepoint))(not (inside p i))) ))
The first question is, do such things exist? You can have it
either way.
Case 1a: Discrete time: every timepoint is the meeting point of
two intervals:
DISCRETE
(forall ((p timepoint))(exists ((i moment)(j moment))(= p (end
i)(begin j)) ))
Case 1b: Dense time: Intervals are impossible (so between any two
points there is a third):
DENSE
(forall ((p timepoint)(q timepoint))(if (before p q)
(exists ((r
timepoint))(and (before p r)(before r q)))
))
from which it follows that
Theorem
(forall ((i timeinterval))(not (moment i)))
(Note, to specify the real line one would have to use
higherorder logic and define limits.)
These two cases are not exhaustive. One can for example allow
moments to exist but only 'sparsely', so that two moments can never
meet:
Case 1c:
AH1
(forall ((i moment)(j moment))(not (meets i j)) )
This allows one to treat these isolated moments as being rather
like points: they are a kind of 'fat point' which can be thought of as
intervals of 'infinitesimal' duration. Other models are also possible,
but lets leave this topic for now.

One problem with the axiom BEF is that since all intervals must
have endpoints, it seems that semiinfinite intervals are impossible,
and if time is infinite then the entire timeline is not an interval.
If this is an issue, we can extend the theory by adding two special
'points at infinity'. (This is a very old mathematical trick, of
course, and is quite safe.) We have to allow an infinite duration to
go along with these, and extend the arithmetic of durations to include
this infinite value. We call these BOT and EOT (begin of time and end
of time). Note, we do not classify these as timepoints: this
keeps the axioms simpler; and the values of the from function applied
to either of these arguments is not classified as a
timeinterval. Similarly, we introduce the special duration value
FOREVER.
INF1
(forall ((p timepoint))(and (before BOT p)(before p
EOT)))
INF2
(forall ((p timepoint))(and (= FOREVER (duration (from BOT
p)))
(= FOREVER (duration (from p
EOT)))
(= FOREVER (duration (BOT
EOT)))
))
FOREV
(forall ((i timeinterval)(n number))(and
(> FOREVER (duration
i))
(= FOREVER (++ FOREVER
(duration i)))
(= FOREVER (* n
FOREVER))
))

Up to now the theory makes a clear distinction between points and
intervals; but if preferred, we can treat points as a special kind of
interval, the result of applying from to the same point twice,
so that p = (from p p) for any point p:
IP1
(forall ((p timepoint))(and (timeinterval p)(= p (from p p))
))
This is consistent with all the earlier options, though it does
have some apparently odd consequences. Points meet themselves,
for example: indeed, this can be used as the definition of a
point:
Theorem:
(forall ((i timeinterval)(iff (timepoint i)(meets i
i)))
Also, any point is a moment; but not necessarily
vice versa. The discrete timeline, for example, is now a totally
ordered series of meeting timeintervals which are all
moments, but only every other one is a timepoint.
This means also that the usual relationships between the Allen
relations is disturbed somewhat: normally for example it is assumed
that if i meets j meets k, then i cannot meet k: but now, if j is a
point, then i does meet k. Reasoners which use the standard Allen
composition algebra therefore have to be reconsidered with this option
(or else restricted to nonpoint intervals, which is probably the most
sensible option.)

Allowing points to be intervals amounts to treating (from p
q) as meaningful both when p is before q and when p=q. We can go
the extra step of treating it as meaningful when q is before p. What
could (from p q) mean when p is after q? It seems
to be a 'backwardpointing interval', whose end is earlier than
its begin. Although this might seem a rather unintuitive kind
of object, it does make sense. Its the 'interval' one gets when some
event is earlier than expected and one is using an interval to
represent the amount by which something is late; or when it is
late, and one is using an interval to measure how early it is. It is
the interval after the start gun that someone begins to run when they
in fact start prematurely; and so on.
All that is needed to make this picture coherent is to allow such
backward intervals to have a negative duration:
V1
(forall ((p timepoint)(q timepoint))(=
(++ (duration (from p q))(duration (from q
p)))
zero
))
Now the function from is a total function on any
pair of points whatsoever: given any two points, without qualification
as to their ordering, there is a unique interval going from one of
them to another. It has zero duration iff they are the same point; it
has positive duration iff the first is before the second; and negative
duration iff the second is before the first.
We can now do full arithmetic on durations, and have complete
expressive power to conclude, for example, that given any
sequence p1,...pn of points, the duration of the interval
(from p1 pn) is the sum of the durations of the intervals (from
p1 p2), (from p2 p3)...(from pn1 pn). In general,
allowing 'backward' intervals has the same advantages in temporal
reasoning that the invention of negative numbers had on the ability to
do arithmetic. For example, a clock which is running fast misstates
all its times by a negative duration.

OK, maybe this will give us something concrete to discuss.
Pat
 
IHMC 40 South Alcaniz St. Pensacola FL 32502 phayesATSIGNihmc.us http://www.ihmc.us/users/phayes _________________________________________________________________ Message Archives: http://ontolog.cim3.net/forum/ontologforum/ Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontologforum/ Unsubscribe: mailto:ontologforumleave@xxxxxxxxxxxxxxxx Shared Files: http://ontolog.cim3.net/file/ Community Wiki: http://ontolog.cim3.net/wiki/ To Post: mailto:ontologforum@xxxxxxxxxxxxxxxx (01) 
<Prev in Thread]  Current Thread  [Next in Thread> 


Previous by Date:  Re: [ontologforum] OWL to KIF translator?, Elisa F. Kendall 

Next by Date:  Re: [ontologforum] Time representation, Pat Hayes 
Previous by Thread:  Re: [ontologforum] (administrivia) Preservation of semantic value, Peter Yim 
Next by Thread:  Re: [ontologforum] Axiomatic ontology, John F. Sowa 
Indexes:  [Date] [Thread] [Top] [All Lists] 