RE: SUO: questions about SUMO
Dear Michael and Ian,
OK. I think I should point out that time is not a real number, as
Michael seems to be suggesting. Time is something that can be
mapped to real number.
That time can be usefully mapped to real number is a consequence
of time and reals sharing some properties. In particular that all
points in time are part of a continuum (at least this is how this
mapping represents time). (This is true for all properties that can
be expressed by a number in a unit of measure. The unit of measure
is the name of the mapping between the property and the number
space).
In fact there are multiple possible mappings of time to real number,
depending on the unit of time that is used, and almost certainly it
is to a subset of real numbers. (Current knowledge suggests that the
universe came into existence some 13b years ago, in which case the
lower limit will at least not be minus infinity).
Matthew West
Principal Consultant
Shell Information Technology International Limited
Shell Centre, London SE1 7NA, United Kingdom
Tel: +44 20 7934 4490 Other Tel: +44 7796 336538
Email: matthew.r.west@is.shell.com
Internet: http://www.shell.com
> -----Original Message-----
> From: Michal Sevcenko SITE [mailto:sevcenko@vc.cvut.cz]
> Sent: 30 April 2002 08:54
> To: standard-upper-ontology@ieee.org
> Subject: RE: SUO: questions about SUMO
>
>
>
>
> Dear Ian,
>
> >
> > To my mind, the relationship between 'RealNumber' and
> 'TimePoint' is the
> > same as the relationship between 'RealNumber' and any other
> unit of measure,
> > and this relationship is, I think, already captured in the ontology.
> > However, if you can specify some other relation that allows
> us to infer
> > additional, true content, we'll consider adding it to the SUMO.
> >
> >
> > It may be that the axiom that every 'TimePoint' being
> greater than negative
> > infinity follows solely from number theory. Unfortunately,
> I don't know
> > enough about number theory to say one way or the other. If you can
> > construct a proof that derives the axiom from principles
> about the real
> > numbers, I'll try to make the axiomatization in the SUMO
> reflect your proof.
> >
> >
> > As for the claim that 'TimePoints' are dense, I don't think
> this follows
> > from what we have in the SUMO. Please let me know, though,
> if you think any
> > axiom or combination of axioms implies this.
> >
>
> I don't know such a number theory axiomatization either. But
> what I am
> wondering about is why you didn't add e.g. an axiom
>
> (=>
> (and
> (instance ?NUMBER RealNumber)
> (not
> (equal ?NUMBER NumericPositiveInfinity)))
> (lessThan ?NUMBER NumericPositiveInfinity))
>
> instead of
>
> (=>
> (and
> (instance ?POINT TimePoint)
> (not
> (equal ?POINT PositiveInfinity)))
> (before ?POINT PositiveInfinity))
>
> This more general axiom could be than extended (hopefully) to
> TimePoint, as
> well as to other quantities. In the same way you can say that
> RealNumbers,
> not TimePoints, are dense. This would be an axiomatization of
> my "number
> theory".
>
> I think that this should be a general principe for
> constructing ontologies
> (as well as other taxonomy-based artifacts): when writing axioms (or
> whatever), use classes as close to the root of the class hierarchy as
> possible, to achieve an economy of expression.
>
> As I browsed through SUMO to learn more about numbers and
> quantities, I was
> wondering that I found no relation between 'lessThan' and
> 'before'. Can you
> tell me if the following axiom (which I believe is true) is
> entailed by
> SUMO?
>
> (=>
> (and
> (instance ?TIME1 TimePoint)
> (instance ?TIME2 TimePoint)
> (instance ?NUMBER1 RealNumber)
> (instance ?NUMBER2 RealNumber)
> (instance ?UNIT UnitOfMeasure)
> (instance ?UNIT TimeDuration)
> (equal (MeasureFn(?NUMBER1, ?UNIT)) ?TIME1)
> (equal (MeasureFn(?NUMBER2, ?UNIT)) ?TIME2))
> (<=>
> (lessThan(?NUMBER1 ?NUMBER2))
> (before(?TIME1 ?TIME2))))
>
> i.e does hold that if two numbers are in < relation, are the
> corresponding
> time points in before relation?
>
> > > > (overlapsTemporally ?interval1 ?interval2) means that the two
> > > > TimeIntervals ?interval1 and ?interval2 have a TimeInterval
> > > in common.
> > > > Note that this is consistent with ?interval1 and ?interval2
> > > being the
> > > > same TimeInterval.
> > >
> > > It suggests that if we think the intervals as sets of TimePoints,
> > > they have nonempty intersection. However, the
> axiomatization of this
> > > relation:
> > >
> > > > (<=>
> > > > (overlapsTemporally ?INTERVAL1 ?INTERVAL2)
> > > > (or
> > > > (equal ?INTERVAL1 ?INTERVAL2)
> > > > (during ?INTERVAL1 ?INTERVAL2)
> > > > (starts ?INTERVAL1 ?INTERVAL2)
> > > > (finishes ?INTERVAL1 ?INTERVAL2)))
> > >
> > > says that ?INTERVAL1 is a subset of ?INTERVAL2 (in the
> set analogy),
> > > which is indeed something different. Am I right?
> >
> > As I understand you, you're worried about the case of "empty time
> > intervals", i.e. intervals that have no points in time. If
> this is indeed
> > the worry, then I think we should just add the following
> axiom to the SUMO:
> >
> > (=>
> > (instance ?INTERVAL TimeInterval)
> > (exists (?POINT)
> > (and
> > (instance ?POINT TimePoint)
> > (temporalPart ?POINT ?INTERVAL))))
> >
>
> I'm not worrying about empty time intervals. Let me explain
> the issue on an
> example. Let A and B be two intervals, and C their intersection:
>
> A |--------|
> B |------------|
> C |-----|
>
> The documentation comment of the overlapsTemporally relation
> says, that the
> relation holds, when A and B have an interval in common (in
> our case they
> have, it is C).
>
> However, the axiomatization says that when relation holds, B must
> completely subsume A, which does not hold for our A and B.
>
> It could be seen that something is wrong from the fact that
> the informal
> formulation in the documentation of overlapsTemporally is completely
> symmetric with respect to ?interval1 and ?interval2, but
> overlapsTemporally
> is PartialOrdering, i.e. antisymmetric relation.
>
> with best regards
> Michal Sevcenko
> ----------------------------------------
> Ing. Michal Sevcenko
> Department of Computer Science
> Faculty of Electrical Engineering
> Czech Technical University in Prague
> Tel +420 2 2435 3661
> http://webis.felk.cvut.cz/en/people/sevcenm.html
>