Re: deSkolemizing to get Horn-expressivity with RDF rules

From: Benjamin Grosof (
Date: 11/12/02

  • Next message: Sandro Hawke: "Re: deSkolemizing to get Horn-expressivity with RDF rules"
    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,
         forall x,z.  (grandparent(x,z) -> (exists y.  (parent(x,y) and 
    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 
    in the consequent emerge only after carving out the universally quantified 
    that (typically) also appear in the body.
    Maybe you can clarify this further?
    >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

    This archive was generated by hypermail 2.1.4 : 11/12/02 EST