**From:** Dan Connolly (*[email protected]*)

**Date:** 11/30/01

**Next message:**Peter F. Patel-Schneider: "Re: querying DAML+OIL syntax"**Previous message:**Peter F. Patel-Schneider: "Re: Can one layer a DAML+OIL model theory on top of RDF?"**In reply to:**Peter F. Patel-Schneider: "Re: querying DAML+OIL syntax"**Next in thread:**Peter F. Patel-Schneider: "Re: querying DAML+OIL syntax"**Reply:**Peter F. Patel-Schneider: "Re: querying DAML+OIL syntax"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ] [ attachment ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

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

**Next message:**Peter F. Patel-Schneider: "Re: querying DAML+OIL syntax"**Previous message:**Peter F. Patel-Schneider: "Re: Can one layer a DAML+OIL model theory on top of RDF?"**In reply to:**Peter F. Patel-Schneider: "Re: querying DAML+OIL syntax"**Next in thread:**Peter F. Patel-Schneider: "Re: querying DAML+OIL syntax"**Reply:**Peter F. Patel-Schneider: "Re: querying DAML+OIL syntax"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ] [ attachment ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

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