RE: SUO: questions about SUMO
Hi Michal,
Please see my comments below.
-Ian
> -----Original Message-----
> From: Michal Sevcenko SITE [mailto:sevcenko@vc.cvut.cz]
> Sent: Tuesday, April 30, 2002 12:54 AM
> 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".
Well, one problem I see with your proposed axiom is that there isn't a
single real number which is larger than every other real number. The real
numbers are uncountably infinite. In the case of time points, however, we
can posit or at least pretend that there is a single point in time which is
greater than all other points in time. This supposition may be just a
useful fiction, but it does allow us to create an ordering of time points,
and it doesn't seem to have any undesirable consequences. Note that the
concepts of the time points 'PositiveInfinity' and 'NegativeInfinity' were
borrowed from the PSL ontology.
>
> 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.
There's no disagreement about this general principle.
>
> 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?
I agree that this should follow from the SUMO. I'll try to construct a
proof for it.
>
> > > > (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.
Now I understand. My apologies for being so dense in my earlier message.
I'll revise the documentation string for 'overlapsTemporally' so that it
reflects the axiom.
>
> 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
>
>