- From: pat hayes <phayes@ai.uwf.edu>
- Date: Tue, 3 Jul 2001 10:22:27 -0700
- To: Dan Connolly <connolly@w3.org>
- Cc: w3c-rdfcore-wg@w3.org
>[oops... I saw your message later in this thread >before I saw this one...] > >pat hayes wrote: >[...tangent about definite descripitons...] > > >This information from the inventory database clearly > > >provides a match (i.e. a proof, or the interesting > > >bits of one, anyway) for the > > >description of the book stated as a formula involving > > >an existentially quantified variable, ?x0. > > > > No, not a description; it just proves that a book exists which > > satisfies the existential. But since there might be several things > > that satisfy an existential, > >That's beside the point... > > > nothing follows about whether the > > bookseller's item#342323 actually IS the particular thing that you > > had in mind when writing your order. > >I don't have any particular thing in mind when I place such >an order. That's how orders work: "if you have any things >that meet these criteria, I'll pay you $35 for one of them." That's a universal sentence of you write it out. It has the form (forall (?x)(implies (meets-criteria ?x) (will-pay-for me you $35 ?x))) > > > (Not without some uniqueness > > assumption from somewhere.) So the bookseller is in the same position > > in either case. If he knows the thing is unique, he can figure out > > what you want; if he doesn't, he can't. > > > > Of course, if you had phrased your order not as an existential but as > > a universal , so that you say: "if it is a book and has author...and > > title ...., then I want it", > >Er... that's an existential, not a universal, right? No, its a universal, since it is an assertion you are making. > >A prolog query > author(X, "b"), title(X, "f e") >is a request to prove the theorem > > (exists (?x) (author ?x "b") (title ?x "f e)) >right? and the query results are proofs; i.e. substitutions >of the variables that show that it's satisfyable. Substitutions of universally quantified variables, right. > >That's how queries work, right? They're existential formulas, >and the job of a query engine is to give proofs, by >example, of the theorem. This is completely traditional, no? Yes, it is traditional and accurate *in FOL*, where the language has full Boolean expressivity (in particular, has negation), but RDF isn't FOL, so its not at all clear what an RDF query is supposed to be. With the interpretation you are giving, an RDF query has the logical force of a universal quantification, which goes beyond what is usually (?) taken to be the expressive power of RDF, as I understand it. Look, heres a way to put it. Divide variables into U-variables and E-variables. U-variables are: 1. Universally quantified in positive contexts (ie inside an even number of negations in an assertion or an odd number in a query) (where the LHS of an implication counts as a negation) 2. Existentially quantified in negative contexts (ie inside an odd number of negations in an assertion or an even number in a query) and E-variables are the others. Then U-variables are 'effectively universal' and E-variables are 'effectively existential', where 'effectively' indicates that the semantics and proof theory don't really distinguish between these cases. Skolemisation applies to E-variables, and U-variables are bound to new values during inference processing: they are the variables that it is valid to freely substitute terms for. >[[[ >Free variables in a query >are assumed to be existentially quantified. >]]] > >-- Knowledge Interchange Format >http://logic.stanford.edu/kif/dpans.html >Thu, 25 Jun 1998 22:31:37 GMT Yeh, and that is potentialy misleading. In this sense, a conjunction in a query is really a disjunction and vice versa, and skolemisation has to be done backwards. The point is that queries are essentially *negated*, but when you negate something with free variables, the free variables stay free. So to keep the intepretation of free variables (which are universal in assertions) consistent, they have to be thought of as existential in queries. But if you check out the actual semantics of KIF, there is no notion of 'query' defined. The way that traditional theorem-provers work is basically by negating the 'query' and then testing the combination for inconsistency. During the actual reasoning process, all U-variables are treated similarly. In a Gentzen sequent logic, 'queries' are on the RHS of the sequent and assertions on the LHS. All the inference rules apply to both sides but are exactly dual, so that conjunctions on the RHS are like disjunctions on the LH, universals on one side like existentials on the other, and so on. > > then the bookseller can figure out what > > you want. However, you might now get several books, unless you give > > enough of a description to pin down one uniquely. > >Several books might match my query, but I specify how many >I want in the order. > > > > >But it doesn't match/prove the formula where _:g0 > > >is replaced by the skolem constant > > ><http://skolem.example#432oj34oij2o3ijo23j> . > > > > Right. And it might not be it. On the other hand it is possible that > > those names corefer, ie > > (= http\:\/\/booksRus\.example\/inv2001\-06\-25\#item342323 > > <http://skolem.example#432oj34oij2o3ijo23j>) > > and if the bookseller could somehow conclude this (eg by knowing that > > only one thing satisfied the description) then he could get you the > > book you want from your order, skolemised or not. > > > > >So an RDF document with anonymous nodes is *not* > > >interchangeable with a skolemized version of that document. > > >Q.E.D. > > > > It is if everyone is using valid logical reasoning. > >No, I disagree. > >The bookseller can conclude that he has a book that >matches your description iff your description is stated >as an existential. If your description is skolemized, >there's no valid inference that allows him to conclude >that he's got a book that you want. No, if YOU describe your book using an existential, then the existential is not in the goal to be proved by the bookseller. Your example used an existential in the goal to be proved, which is like the use of a universal in an assertion. If he has an asserted existential he isnt in a position to infer that he's got a book you want, either. He isnt allowed to validly instantiate any of your existential variables (unless he knows enough to infer that they are unique, but then he could also infer that about your skolem name, since he knows exactly asmuch about that as he does about the possble values of your existentials.) > > >I think this is the important part of Pat's message > > >that I disagree with is: > > > > > > > RDF is supposed to > > > > consist of assertions, not equations, and they are pretty simple > > > > assertions of the logical form (V s o) . Those s's and o's are > > > > logical names = logical constants, ie they denote things, one thing > > > > each in a given interpretation. Now, logical names are *just* like > > > > existentially quantified variables where the quantifers are at the > > > > top level (the only level there is in RDF), ie not inside any > > > > universal quantifiers. > > > > > >The s's and o's would be just logical constants if we > > >left out anonymous/existentially-quantified terms. > > >But RDF does have such terms, as demonstrated above. > > >And the semantics of such terms is non-trivially > > >different from the semantics of constants: > > >an existentially quantified formula is satisfied > > >by an interpretation if there's *some* thing > > >you can bind the existential term to that makes > > >it work out. > > > > Yes, and that is exactly the truth conditions for a logical name, as > > well; it has to have a denotation that makes the sentences containing > > the name work out true. > >But it only has that denotation in *some* interpretations; >valid inference requires that *all* interpretations work. No, it has to have it an all interpretations that satisfy the antecedents, if we are talking about sentences that contain the name. If I assert (exists (?x)(foo ?x)) and if I assert (foo genid3452) knowing that nobody, including me, can possibly know anything else about genid3452 (because I just made the name up out of thin air and it is guranteed to be unique), then I have said the same thing, and you can infer the same things from it (apart from the completely useless fact that whatever it is, I am calling it 'genid3452' in the second case.) > > > >Skolemizing the formula reduces > > >the number of interpretations that satisify the > > >formula. > > > > No, it doesnt. Technically, if E is an existential sentence and E' is > > a skolemisation of it, then E and E' are actually in different > > logical languages, > >But what's going on in the implementations of RDF that >do this (i.e. emit generated URIs for anonymous terms, >as if these generated URIs were in the >document in the first place) is all happening in the >same language. In the strict logical sense, I think that isnt actually true. When a new name is generated, the logical langauge changes. Its a fine point, but this is one place where we may need to be rather careful. >So perhaps it's a misnomer to say that they're doing skolemization. Well, all that means is using a new name. There isnt any doubt that THAT is what is happening, right? > >[...model theory stuff that I sorta followed...] > >I don't think I want to go into that E/E' stuff until >I've seen your response to my clarification about >orders/queries being existentials. OK. BTW, I think that Frank Manola said it all right, as well. 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 Tuesday, 3 July 2001 13:27:20 UTC