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

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

>  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