From: Benjamin Grosof (bgrosof@mit.edu)
Date: 11/12/02
Hi Sandro (and all), At 06:34 PM 11/12/2002 -0500, Sandro Hawke wrote: >I said I'd write something to the list about this. > >There's a trick to making RDF rules be Horn-expressive instead of >merely datalog-expressive with only a slight change in the rules >language. We use this trick in cwm/n3, and I used it in some >unpublished pre-w3c work. I've mentioned it before (in proposals I >wouldn't exactly support any more) [1] [2], but I still haven't come >up with any proper references. I looked these two earlier postings over. I think they (esp. the second which I focus on here) contains some things that need clarifying technically . A key fact about FOL, including Horn FOL, to keep in mind is that in any implication, existentially quantifying a variable within the scope of (only) the antecedent is equivalent to pulling that variable out and universally quantifying it over the scope of the whole implication. E.g., forall x,y,z. (grandparent(x,z) <- parent(x,y) and parent(y,z) ) is equivalent to forall x,z. (grandparent(x,z) <- (exists y. (parent(x,y) and parent(y,z)) Cleary in your messages you would like to be able to represent the converse of the above, i.e., forall x,z. (grandparent(x,z) -> (exists y. (parent(x,y) and parent(y,z)) Formally, however, introducing an existential in the head is not allowed in Horn, so this goes beyond Horn. Your "style 2" does this. By contrast, your "style 1" is simply Horn (Datalog-ness issue aside), no more no less. Since style 2 can express style 1 as a special case, style 2 is strictly more powerful than Horn. Quite non-standard in your way of describing a "rule" (in both "styles") is to treat the *names* of quantified variables as significant *outside* of the scope of their quantification. By contrast, in FOL (and thus in its expressive fragments, including Horn and Description Logic), within the scope of a quantifier one can equivalently rewrite the variable names arbitrarily. Your intuition of correspondence between variables in an antecedent expression and variables in a consequent expression is, I believe, simply better viewed as universal quantification. Viewed separately, the two expressions are each what in FOL is simply called "open", i.e., they have variables in them. I don't really understand what you mean by saying that you're "deSkolemizing" other than at a rather hazy intuitive level. The existentially quantified variables in the consequent emerge only after carving out the universally quantified variables that (typically) also appear in the body. Maybe you can clarify this further? Benjamin >The idea is this: if an RDF rule is a pair of RDF graphs (the >body/antecedent and the head/consequent), with certain nodes/arcs in >the graph marked as variables (just like in DQL), then we only have >datalog rules. If, however, we also allow nodes/arcs in the >consequent to be marked as existential variables in the scope of the >consequent, we have Horn expressivity. > >To see why this is so, think about how Skolemizing turns existentials >into Skolem function terms, and then work it backwards, turning function >terms into existentials and "deSkolem" predicates. > >This is important to RDF/DAML-Rules, because without this trick, >people working with RDF/DAML (not having function terms) are likely to >be stuck unnecessarily datalog. RDF rules need not be any less >expressive than Horn rules. > > -- sandro > >[1] http://lists.w3.org/Archives/Public/www-rdf-logic/2001Mar/0075.html >[2] http://lists.w3.org/Archives/Public/www-rdf-rules/2001Sep/0054.html
This archive was generated by hypermail 2.1.4 : 11/12/02 EST