- From: <jos.deroo.jd@belgium.agfa.com>
- Date: Fri, 29 Jun 2001 01:31:00 +0100
- To: phayes@ai.uwf.edu
- 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') >(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? >>(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]? -- Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/ ps I don't know yet the true nature of anonymous nodes...
Received on Thursday, 28 June 2001 19:31:11 UTC