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