Re: querying DAML+OIL syntax

From: Dan Connolly ([email protected])
Date: 11/30/01 

"Peter F. Patel-Schneider" wrote:
> 
> From: Dan Connolly <[email protected]>
> Subject: Re: querying DAML+OIL syntax
> Date: Thu, 29 Nov 2001 22:40:56 -0600
> 
> > "Peter F. Patel-Schneider" wrote:
> > >
> > > From: Pat Hayes <[email protected]>
> > > Subject: Re: querying DAML+OIL syntax
> > > Date: Thu, 29 Nov 2001 19:44:07 -0600
> > >
> > > > >
> > > > >Untouchable - should not make it into the model theory
> > > >
> > > > Why?
> >
> > indeed, why?
> >
> > > > (Because they use constructions defined by rdf:parseType??)
> >
> > The rdf:parseType="daml:collection" is only syntactic sugar;
> > any expression that can be written with it can
> > also be written without it, using only daml:first,
> > daml:rest, and daml:nil. It has zero effect on the model theory.
> >
> > > To be more precise, perhaps.
> > >
> > > The above constructs are DAML+OIL syntax and should not generate
> > > relationships in the model theory.
> >
> > No, they're constants in the DAML+OIL vocabulary... a vocabulary
> > of URIs which can be used in RDF syntax.
> >
> > >  For example (using a much nicer syntax)
> > >
> > >         (unionOf a (intersectionOf b c))
> > >
> > > should not result in a unionOf relationship in the model theory.
> >
> > Umm... I'm not sure I understand your syntax; is that
> > a functional term or an atom? i.e. does it mean
> > "the union of a and ..." or
> > "a is the union of ..."?
> >
> > I'll assume the former.
> 
> Yes, functional term.
> 
> > > Why?  Well, if it did then how could you get an entailment between
> > >
> > >         A = (unionOf a (intersectionOf b c))
> > >
> > > and
> > >
> > >         B = (intersectionOf (unionOf a b) (unionOf b c))
> >
> > In the obvious way, no?
> >
> > I assume you mean that
> >       X in (unionOf a (intersectionOf b c))
> > should entail
> >       X in (intersectionOf (unionOf a b) (unionOf a c))
> >
> > I assume the (unionOf b c) term was a typo and you meant (unionOf a c).
> > Otherwise, there is no entialment.
> 
> Yes, a typo.  Sorry.
> 
> > Then... let's write these expressions using only 2-place predicates,
> > conjunction, and existential quantification. (i.e. in RDF triples)
> >
> > A= ... becomes:
> >
> > (exists (?uaibc ?liabc ?libc ?ibc ?lbc ?lc)
> >  (and
> >   (type X ?uaibc)
> >   (unionOf ?uaibc ?laibc)
> >   (first ?laibc a) (rest ?laibc ?libc)
> >   (first ?libc ?ibc) (rest ?libc nil)
> >   (intersectionOf ?ibc ?lbc)
> >   (first ?lbc b)
> >   (rest ?lbc ?lc)
> >   (first ?lc c)
> >   (rest ?lc nil) ))
> >
> > B= becomes...
> >
> > (exists (?iabbc ...)
> >  (and
> >   (type X ?iuabubc)
> >   (intersectionOf ?iuabubc ?luabubc)
> >   (first ?luabubc ?uab) (rest ?luabubc ?lubc)
> >   (first ?lubc ?ubc) (rest ?lubc nil)
> >   (unionOf ?uab ?lab)
> >   (first ?lab a) (rest ?lab ?lb) (first ?lb b) (rest ?lb nil)
> >   (unionOf ?ubc ?lbc)
> >   (first ?lbc b) (rest ?lbc ?lc) (first ?lc c) (rest ?lc c)
> >  ) )
> > The argument for entailment follows straightforwardly:
> > from (type X ?uaibc) and (unionOf ?uaibc ?laibc)
> > we know (from the DAML unionOf-axiom-1, or the
> > corresponding bit from the model theoretic semantics)
> > that there's some ?c2 so that X is in ?c2 and ?c2 is in the list ?laibc.
> > So ?c2 is either a or ?ibc. If ?c2 is a, then
> > X is in a, so it's in the union of a with b, i.e. ?uab,
> > and it's in ?ubc, so it's in their intersection,
> > namely ?iuabubc.
> >
> > If ?c2 is ?ibc, blah blah blah and the result
> > follows again.
> >
> > Hence, by proof by cases, QED.
> 
> I do not believe that this entailment follows at all, even fixing the typos.
> 
> In the second formula you have two unionOf relationships.  How does the
> first formula entail them when it only has one unionOf relationship?

Which part of "The argument for ... QED" do you not buy?
I can elaborate in arbitrary detail, I suppose.

> To make the non-entailment even clearer, try your exercise with
> 
>         A in (unionOf C D)
> 
> and
> 
>         A in (unionOf C D E)
> 
> The second will result in a three-element list.  How can that follow from
> the first, which only has a two-element list?

again, by unionOf-axiom-1; that is: if A in (unionOf C D)
then exists ?c2 such that A in ?c2 and ?c2 in (list C D). OK so far?

?c2 in (list C D) means ?c2 is C or ?C2 is D (by
the definitions of first/rest/nil).

[I trust you'll allow me to use ?c2 both as an
existentially quantified variable
name and as its skolem constant, since there's no
ambiguity.]

Case 1: If ?c2 is C, then we have
	(first (list C D E) C)
hence
	(item C (list C D E))
hence
	A in C and (item  C (list C D E))
hence, by unionOf-axiom-1,
	A in (untionOf C D E)

Case 2: If ?c2 turns out to be D, the argument is analagous.

Hence, it works out in either case, QED.


> 
> > i.e. in the same way that RDF and RDFS share
> > an interpretation structure, but RDFS-satisfaction
> > is more constrained than RDF-satisfaction,
> > DAML+OIL satisfaction is more constrained
> > than RDFS-satisfaction (there are more
> > axioms in the theory).
> 
> > This seems so straightforward that I can't understand
> > where Peter is coming from. What am I missing?
> 
> I think that you are missing lots here.   To prove entailment, you have
> to show that all the predications from the second formula are true in all
> models of the first.

I have done just that, no?

I realize my arguments are written in proof-theoretci style;
but they have obvious analogs in model-theoretic style, no?

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

This archive was generated by hypermail 2.1.4 : 04/02/02 EST