From: Sandro Hawke ([email protected])
Date: 11/12/02
Benjamin writes:
> 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
> ))
right.
> 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))
yep.
> 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.
I agree the form is not Horn clausal, but I think it is equivalent.
The existential I'm allowing in the head would come right back out,
leaving you with only Horn clauses, if you clausified the formula. So
the expressiveness is the same.
> 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 totally agree with you. Back when I wrote that, I thought perhaps
bNodes were more acceptable to the community than universally
quantified variables, so that maybe we could sneak in (er, gracefully
introduce) rules using only bNodes as variable. I now think that's a
bad idea.
> 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?
Maybe. :-)
The typical procedure for converting an FOL sentence into clausal
form begins:
1. Rewrite => using ~ and |
2. Move ~ inwards
3. Rename variables to be distinct through the sentence
4. Move quantifiers left
5. Skolemize: remove existential quantifiers by replacing the
variables with new functions, parameterized by all
universals to their left.
...
So there's a kind of duality between existentially quantified
variables and functions. Skolemizing is converting all existential
variables to being function terms; deSkolemizing is converting all
function terms to be existentially quantified variables.
If you think of f(x,y) as denoting the thing which is mapped to by f
from the pair <x,y>, it makes perfect sense to involve that "thing"
in a predicate. We can imaging such a predicate, pf, defined
pf(z,x,y) <=> z=f(x,y)
Maybe we can call pf the "Skolem Predicate" of f (or maybe it has some
existing name in the literature). To deSkolemize a formula, getting
rid of all functions, we convert it as 1-4 above, then rewrite each
literal (atomic sentence or negated atomic sentence) containing a
function term as an existentially quantified formula containing the
conjunction of the Skolem predicate formula(s) and the literal with
the function term(s) replaced by the newly introduced variable(s).
For example...
... & ~p(a, b, f(a), g(c, d)) & ...
turns into
... & exists e1 e2 (
~p(a, b, e1, e2) &
pf(e1, a) &
pg(e2, c, d)
) & ...
I think I've got that right. In any case, it should be enough to show
what I mean.
As you pointed out on the call, pf and pg need to be defined with some
kind of uniqueness rule, like
all x y z ( p(x,y) & p(z, y) => x=z )
This actually makes a nice example of when you want to use the
equivalence you meantioned at the start of the message. If we want to
make it a biconditional, we need to move y's quantification inside:
all x z (
exists y ( p(x,y) & p(z, y) )
<=>
x=z
)
...although I guess that's only true if f were a total function; to
handle that more carefully, we should do something with the domain of
f:
all x z (
exists y ( p(x,y) & p(z, y) )
<=>
inDomainOf_f(x) & x=z
)
The details are going to require more thought than I'm capable of
right now.
To remind ourselves of the point here: RDF graphs are more expressive
than FOL atomic sentences. The logic-function terms and n-ary
predicates in FOL are essentially just syntactic sugar; they can be
converted into RDF by using additional predicates and triples (modulo
the function's many-to-one mapping quality, which requires additional
expressivity to encode).
The presence of logic functions is usually seen as the distinguishing
feature between datalog and Horn logic, but that's only a true
division when we're looking at clausal form sentences. In
characterizing RDF rules as UR-Centered-Bin-Datalog, it looks like
you've incorrectly let RDF's lack of logic functions make you think
RDF rules have to be no more expressive than datalog. Puting it under
datalog makes RDF rules fit nicely in your hierarchy, but it gives us
a less powerful system than we (cwm/n3 users at least) want.
(Ah the silly contortions of working with RDF.... :-)
-- sandro
This archive was generated by hypermail 2.1.4 : 11/12/02 EST