# Re: malformed OWL KBs (was Re: proposal for last session of July face-to-face (new issues?))

From: Dan Connolly <connolly@w3.org>
Date: 19 Jun 2002 15:11:16 -0500
To: "Peter F. "Patel-Schneider <pfps@research.bell-labs.com>

Message-Id: <1024517477.26130.338.camel@dirk>
```
On Wed, 2002-06-19 at 13:45, Peter F. Patel-Schneider wrote:
[...]
> > > For example, what is the meaning of a malformed list, i.e., a list
> > > 1/ where some list node does not have a rest,
> > > 2/ where some list node does not have a first,
> > > 3/ where some list node has two first[s],
> > > 4/ where some list node has two rests,
> >
> > Those don't seem hard: the latter two are contradictions,
> > and the former two just mean there aren't enough premises
> > or whatever to come to interesting conclusions.
>
> Not true.  The latter two are not contradictions unless the two firsts or
> rests can be shown to be distinct.

Well, yes, by "two firsts" I inferred that you meant first(L, X)
and first(L, Y) where X<>Y. That's the conventional meaning
of "two", no?

>  The former two may or may not lead to
> interesting conclusions and may complicate the formal specification and
> inference.   For example, a oneOf on a list missing a rest has a meaning.

I guess "complicated" is in the eye of the beholder. It doesn't
look complicated to me.

> > > 5/ that is circular, or
> > > 6/ that is infinite.
> >
> > I see two options:
> >
> > (a) do without lists altogether, ala writing
> > (and P (and Q (and R S))))
> > instead of (and P Q R S).
>
> How are you going to do this?  All you have to work with are triples, and a
> triple is not sufficient to atomically represent (and R S).

I don't see how being atomic is relevant. I expect something
like this would work:

:C ont:intersectionLHS :R.
:C ont:intersectionRHS :S.

> > That would be tedious; oneOf would go from a simple
> > binary relation to an ugly thing ala onProperty/hasValue.
>
> oneOf would certainly be difficult.

well, tedious, but not difficult:

:Stooges ont:oneOfFirstItem :Moe.
:Stooges ont:oneOfRest _:C1.
_:C1 ont:oneOfFirstItem :Larry.
_:C1 ont:oneOfRest _:C2.
_:C2 ont:oneOfFirstItem :Curly.
_:C2 ont:oneOfRest ont:Nothing.

> > (b) work thru the details of induction over lists.
> > This would take us outside of FOL, which would
> > make the formal aspects of our spec more complex,
> > but most users would probably prefer it
> > to the tedious option (a).
>
> Well, to make this work you would have to go through a lot of machinery to
> even show that your specification is well-formed at all.

Yes, we need to carefully review our spec.

(or is there some technical sense of "well-formed specification"
that you're using?)

>  You would also
> probably have to do a lot more work to show that your specification was
> realizeable.

Hmm... that looks like another term of art that I'm
not familiar with.

>  The kinds of things that could crop up include infinite lists
> that cover everything in an otherwise-recognizable category, thus leading
> to non-compactness.

I'm sure there are lots of ways to get it wrong.

> > Lots of practical systems do this: Larch
> > and ACL2 call themselves 1st order systems,
> > but they sneak in induction.
>
> > Well, ACL2 is much less sneaky...
> >
> >   A Precise Description of the ACL2 Logic
> >   http://www.cs.utexas.edu/users/moore/publications/km97a.ps.Z
>
> > But Larch is pretty glib...
> >
> > "Except for the fact that it provides a rich set of notations for
> > functions, LP is based on the syntax and semantics for first-order logic
> > found in many textbooks."
> >   -- LP, the Larch Prover -- Logical syntax and semantics
> >   http://www.sds.lcs.mit.edu/Larch/LP/logic/logic.html
> >
> > (I still need to study Michael's stuff on ACL2 and OWL...
> > http://lists.w3.org/Archives/Public/www-webont-wg/2002Mar/0301.html )
>
> Well, I don't think that you are going to get what you want out of these
> systems.

I don't want anything out of them.

>  The induction in ACL2 is used, for example, to prove conjectures about
> regular, i.e., finite and non-circular, lists.  Proving conjectures about
> infinite structures, i.e., infinite lists or the integers, is different.
>
> > > For example, what is the meaning of a malformed restriction, i.e., a
> > > restriction
> > > 1/ that is missing an onProperty element,
> > > 2/ that has none of the other parts of a restriction, or
> >
> > again, it's just as if you have a rule that says
> > IF: parent(X, Y)
> > AND brother(Y, Z)
> > THEN: uncle(X, Z)
> > and you have brother(a, b) with no clues about
> > who a is a parent of; you just can't come to any
> > uncle(X, b) conclusions.
>
> How have you shown that no conclusions can arise?

I haven't. I just made an analogy.

>  There are lots of
> unusual cases to consider, including cases where there only a limited
> number of classes or properties or individuals in any model.

Yes, I'm sure there are lots of ways to get it wrong.

> > > 3/ that has more than one of the other parts of a restriction.
> >
> > > These are a problem for the DAML+OIL way of expressing the model-theoretic
> > > semantics of triple KBs, but there is a solution there because the DAML+OIL
> > > model theory keys off the (syntactic) triples, not the (semantic) IEXT.
> > >
> > > [...]
> > >
> > > > > M3 What is the formal meaning of an OWL KB?
> > > >
> > > > Whatever we specify it to be, no?
> > >
> > > [...]
> > >
> > > > > 	http://www-db.research.bell-labs.com/user/pfps/owl/translation.html
> > > >
> > > > There's also my proposal to do a model theory straight from
> > > > the triple abstract syntax:
> > > >
> > > >   * layering (5.3,5.10): a same-syntax model theory
> > > >   Dan Connolly (Thu, May 30 2002)
> > > >   http://lists.w3.org/Archives/Public/www-webont-wg/2002May/0264.html
> > >
> > > Your proposal is not a model theory from the triple syntax but is instead a
> > > model theory from RDFS interpretations.  Your way of specifying semantics
> > > for triple KBs is *much* harder than specifying semantics from the triple
> > > syntax.  In particular, it cannot handle malformed lists and restrictions
> > > in the way that they are handled in the DAML+OIL semantics.
> >
> > Yes, specifying exactly how lists work is tricky. We could perhaps avoid
> > that. But I think it's worth the effort, since the effort is over
> > when we finish our spec, but the effort for users to deal with a klunky
> > language lasts long after.
>
> Well then I suggest that you get to work.

Is that sort of remark really necessary?
I could sure live without it.

>  Until a specification is
> presented I remain unconvinced that a specification is possible and, even
> if it is possible, that it will result in a language that is less kluky
> than one that avoids these issues.

I'm pretty sure an existince proof of the possibility
is easier than a proof that it's impossible. 1/2 ;-)

--
Dan Connolly, W3C http://www.w3.org/People/Connolly/
```
Received on Wednesday, 19 June 2002 16:11:09 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:56:45 UTC