Re: querying DAML+OIL syntax

From: Peter F. Patel-Schneider (pfps@research.bell-labs.com)
Date: 11/30/01 

From: Dan Connolly <connolly@w3.org>
Subject: Re: querying DAML+OIL syntax
Date: Thu, 29 Nov 2001 22:40:56 -0600

> "Peter F. Patel-Schneider" wrote:
> > 
> > From: Pat Hayes <phayes@ai.uwf.edu>
> > 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?

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?

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


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

peter

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