- From: pat hayes <phayes@ai.uwf.edu>
- Date: Thu, 28 Jun 2001 10:11:22 -0500
- To: jos.deroo.jd@belgium.agfa.com
- Cc: w3c-rdfcore-wg@w3.org
>[...] > >>that's indeed a very good point about skolemization > >>in the case that 'we are not in the scope of a universal > >>quanitifer' we have indeed a full blown *constant* > >>but I think that in general you can not make that > >>assumption (your piece of RDF *could* fall in the > >>scope of many univerally quantified variables (I mean > >>when used by outside-core things) > > > >WHAT??!!!???? How??? (How can anything outside a document project a > >quantifier scope across that document??) > > > >That is an amazing idea, and suggests an entirely new picture of how > >the semantic web might work, but if we really think this is possible > >then we should get it clear ASAP, as it completely changes the ground > >rules. For example there is no such thing as an assertion, since > >anything might be only a subexpression of something outside the > >document. > >A SAP would help here (such a hot weather...) Hey, you should be in Florida, 98F and 100% humidity, even the buildings sweat. > >OK, let's take e.g. the following piece of RDF >(which is at http://www.agfa.com/w3c/n3/ext.n3) > >///// >:s0 :is [ :p1 :o1; :p2 :o2]. >:s0 :p3 :o3. >\\\\\ >and onother one (which is at http://www.agfa.com/w3c/n3/ext-rules.n3) > >///// > {{:u :is [ :p1 :x; :p2 :y]. :u :p3 :z} log:implies >{:u :is [ :p1 :x; :p2 :y; :p3 :z]}} a log:Truth; log:forAll :u, :x, :y, :z. >\\\\\ Just as an aside: that universal quantifier is scoped by the outer pair of { }, ie it is entirely inside the document http://www.agfa.com/w3c/n3/ext-rules.n3, right? >then the query (which is at http://www.agfa.com/w3c/n3/ext-query.n3) > >///// >{:s0 :is :z} log:forSome :z. >\\\\\ What indicates that this is a query? (Is there any syntactic distinction?) Not just a quibble, because in many usages, calling something a 'query' effectively inverts all its quantifiers, so that an existential in a query is like a universal in an assertion. If you are following this common convention, then the log:forSome, while logically correct, is potentially misleading: it is 'functionally' exactly like a universal, so that the :z variable can be bound to anything. (In Gentzen terminology, it is on the other side of the sequent, so all the intro/elimination rules are inverted. In LP terms, the goal is negated and then you test for unsatisfiability.) Notice it would be a logical error to skolemise an existential *in a query*; a query isn't being asserted. >will result in (which is at http://www.agfa.com/w3c/n3/ext-result.n3) > >///// > {:s0 :is [ :p1 :o1; :p2 :o2]. > :s0 :p3 :o3} log:implies >{:s0 :is [ :p1 :o1; :p2 :o2; :p3 :o3]}. > >:s0 :is [ :p1 :o1; :p2 :o2]. >\\\\\ > >so there is some kind of changed 'extension of objects' No, you are just doing conventional reasoning here, with universals in the axioms (assumptions) and existentials in the goals (queries, conclusions) , both of which mean that all variables can be freely matched to anything. All your quantifiers are 'universal' in this sense, and all their scopes are local to their documents; nothing projects or extends from one document into another, but since the variables are all universal, they can be bound to terms (names) occurring in other documents. (All of this assumes that all the documents are talking about the same universe, so it is kosher to just smurge together assertions from different sources and draw conclusions from them as thouh they were all in one document. This is probably too naive a perspective for the entire web; but that gets us into a minefield which is beyond the scope of this WG.) >(there must be some link with SKIF here) > >OK, we have identified an anonymous node by its content >in the sense of > a (not *the*) thing which has as 'least common' > certain descriptions >and it is kind of 'by value' (not 'by reference') >but is that a problem? I think that your use here of universal quantifiers goes way beyond RDF. All your variables are universal. Pat --------------------------------------------------------------------- IHMC (850)434 8903 home 40 South Alcaniz St. (850)202 4416 office Pensacola, FL 32501 (850)202 4440 fax phayes@ai.uwf.edu http://www.coginst.uwf.edu/~phayes
Received on Thursday, 28 June 2001 11:11:29 UTC