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