Re: querying DAML+OIL syntax

From: Dan Connolly (connolly@w3.org)
Date: 11/29/01 

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

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

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

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

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