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

From: Dan Connolly <connolly@w3.org>
Subject: Re: malformed OWL KBs (was Re: proposal for last session of July	face-to-face (new issues?))
Date: 19 Jun 2002 15:11:16 -0500

> 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?

No.  Why should X and Y denoting distinct elements of the domain be a part
of what I said?  If had meant two distinct firsts, I would have said so.

> >  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.

Well then, I await an explanation showing that a list with a missing part
does not lead to complications.

> > > > 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.

What about the case where there is no given LHS or no given RHS, or two or
more of either?

> > > 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.

And here we have lists again, just slightly disguised.  What happens if
this construction is malformed in any of the ways that a list can be
malformed?

> > > (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?)

Well, not really, but a well-formed spec is one that actually correctly
defines everything in it.  For example, if one uses induction over
potentially infinite constructions, then one has to be very careful, as
things that one might think are well defined may not turn out to be.  This
can be very complex, particularly if one wants to retain properties like
compactness.

> >  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.

Well suppose that one designs a specification that looks great on paper,
and that has all the desirable properties.  However, if the specfication
has no realization, e.g., there are no interpretations, then the
specification is not worth very much.

> >  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.

Then why did you refer to them in your reply?

> >  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.

A potentially false analogy, then.

> >  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.
> > > contradiction. 
> > > 
> > > > 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.

Well who is going to do the work?  I'm sure not!  

> >  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 ;-)

Agreed, but I'm sure not proposing to prove that it is impossible.  Going
forward along this path requires not only a proof that the path is possible
but also a concrete specification.

> -- 
> Dan Connolly, W3C http://www.w3.org/People/Connolly/
> 

peter

Received on Wednesday, 19 June 2002 16:44:52 UTC