- From: pat hayes <phayes@ai.uwf.edu>
- Date: Tue, 3 Jul 2001 10:22:27 -0700
- To: jos.deroo.jd@belgium.agfa.com
- Cc: w3c-rdfcore-wg@w3.org
>[...] > >>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? > >its scope is the outer pair of { } >document scope would be > this log:forAll :u, :x, :y, :z. > > >>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?) > >you are right, there is no syntactic distinction >it's just that such documents should not be 'asserted' > > >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, > >we follow that 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. > >right, we don't assert and should not skolemise an existential *in a >query* and maybe look for a syntactic distinction > > >>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. > >They *could* have a name, but we just don't care about giving them >a name, but instead infer with terms represented as descriptions >and we think those terms *could* stand for 'some things' (certainly >not for 'all things') The point is that if you have an inference process that instantiates a variable by some kind of matching, then that process is valid only if the variable being instantiated is effectively universal (ie is a U-variable, cf my earlier reply to Dan C.) What it gets instantiated TO might well be an existential, but that is a different issue. > >(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.) > >Well, if we can make 'sound arguments' out of that 'smurge together' >what would be wrong about that? Nothing, as long as there is some guarantee that they are valid. Its a delicate issue, this one. I mention it only to mark it as something that will need more attention later, it is probably outside the WG scope. > > >>(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. > >also the variable [ a :Person; :hairColor :black]? If it is in a query, yes. Pat Hayes --------------------------------------------------------------------- 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 Tuesday, 3 July 2001 13:26:50 UTC