Re: DTTF: How unasserted triples help

Dan Connolly wrote:

> On Wed, 2002-05-22 at 14:38, Jonathan Borden wrote:
...
> >
> > which roughly translates to: "There exists a class having the
intersectionOf
> > property whose object is a List, whose first element is #student and
whose
> > rest is another List whose first element is #employee and whose rest is
nil"
> >
> > As "asserted" triples, these statements are said to be _truths_, which
is a
> > bit strange because this isn't what we really mean.
>
> It's not strange at all; it's exactly what we mean:
>
> "for intersectionOf(X, Y) read: X is the intersection of the classes in
> the list Y"
>  -- http://www.w3.org/2001/10/daml+oil

Well yes, this _is_ what we want to say, we agree. Yet this is not what the
RDF triples themselves say. For instance, "classes in the list Y" has no
direct corrollary in RDF, which is the point. This is something which must
be infered, and in a way that does not license paradoxes.

>
> > Instead we mean to say:
> >
> > "There exists a class which is the intersectionOf #student and
#employee."
>
> That's an informal corrollary of the above, but it can't be
> stated formally/directly using 2-place predicates.

But we do intend the OWL MT to say this, agreed? Just as the RDF MT is not
itself written in RDF, there is no requirement that the OWL MT be limited to
say things using "2-place predicates"

>
>
> > So presumably the OWL MT would have a statement or axiom or something to
the
> > effect that:
> >
> > "intersectionOf(a , b) <=> intersectionOf( b, a)"
>
> Sorry, this is too hand-wavy to be convincing.

Well, of course the actual axiom will have to take care of intersectionOf(
a1, a2, ... an) which is exactly what it does do, or at least how I
understand the MT that I've seen from Peter.

>
>
> > In this way, having _unasserted_ triples allows the OWL MT to apply its
own
> > semantics to the triples (which we are using as syntax). The answer is
that
> > having unasserted triples:
> >
> > 1) prevents paradoxes
> > 2) allows the OWL MT to do its job of defining semantics for OWL
statements
>
> I can imaging that it might; but I would be entirely more convinced
> if there were an existence proof showing *how* unasserted triples
> allows the OWL MT to do this.

By "existence proof" you mean to say that you will be convinced once you see
the actual MT? I think the point is that "asserted" triples have been
demonstrated to cause paradoxes in the context of what we are trying to do.
Without asserting the triples we have syntax, and no paradox. As DAML+OIL
shows, it is possible to write down the _syntax_ in triples. So the
"existence proof" is merely the existence of a MT which defines a semantics
for the triples.

>
> > other examples would be
> >
> > owl:import
> >
> > etc. etc.
> >
> > the idea being not that these statements would be lacking semantics,
rather
> > that the truths stated in these OWL statements would be defined by the
OWL
> > MT i.e.
> >
> > "If it is true that John is a member of the intersectionOf(student,
> > employee) then it necessarily follows that John is a member of the
> > intersectionOf(employee,student)"
> >
> > Problem solved, etcetera.
>
> Not to my satisfaction.
>

Well you asked for a specific solution to a specific example, and I gave you
one in English -- this really is that easy. Hopefully someone who speaks
"MT" will be able to fill in the details of my handwaving.

Of course you will only be satisfied once the actual OWL MT is completed and
I suppose has made REC, but in the meantime the purpose of this exersize is
to agree on a way forward i.e. a way to go about layering OWL with its MT
onto RDF with its MT in a way that allows useful inferences to be drawn
about the things we care about.

Do we really want to wait until the OWL MT is actually written and argued
about and completed _before_ we pass this issue off to RDFCore? To turn the
question around, are you willing to hold up the RDFCore work including the
RDF MT, syntax etc. _until after_ the OWL MT, syntax etc. is completed?

The real world fact is that we have to make some decisions in relatively
short order else we might be stuck with something that, if paradoxical, is
useless.

Jonathan

Received on Wednesday, 22 May 2002 16:54:06 UTC