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

From: Dan Connolly <connolly@w3.org>
Subject: Re: proposal for last session of July face-to-face (new issues?)
Date: 19 Jun 2002 12:49:22 -0500

> On Wed, 2002-06-19 at 10:03, Peter F. Patel-Schneider wrote: 
> > From: Dan Connolly <connolly@w3.org>
> > Subject: Re: proposal for last session of July face-to-face (new issues?)
> > Date: 19 Jun 2002 09:29:02 -0500
> > 
> > > On Wed, 2002-06-19 at 09:05, Peter F. Patel-Schneider wrote:
> > > [...]
> > > > These leave three portions of OWL unspecified:
> > > > 
> > > > M1 What is an OWL KB in triple form, and, more importantly, what
> > > >    collections of triples are not OWL KBs?
> > > 
> > > I expect all collections of triples are OWL KBs; that's
> > > the way I read the DAML+OIL Note. It looks like a
> > > new issue belongs on our issues list.
> > 
> > Well if all collections of triples are OWL KBs then there are some 
> > problems.
> 
> Yes; there's no free lunch... 
> 
> > 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.  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.

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

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

oneOf would certainly be difficult.

> (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.  You would also
probably have to do a lot more work to show that your specification was
realizeable.  The kinds of things that could crop up include infinite lists
that cover everything in an otherwise-recognizable category, thus leading
to non-compactness.

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

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

> > > Dan Connolly, W3C http://www.w3.org/People/Connolly/
> > 
> > Peter F. Patel-Schneider
> > Bell Labs Research
> -- 
> Dan Connolly, W3C http://www.w3.org/People/Connolly/

Peter F. Patel-Schneider
Bell Labs Research

Received on Wednesday, 19 June 2002 14:45:40 UTC