- From: Pat Hayes <phayes@ai.uwf.edu>
- Date: Tue, 18 Sep 2001 18:51:50 -0500
- To: Sandro Hawke <sandro@w3.org>
- Cc: www-rdf-rules@w3.org
> > >Style 2: >> > >> > We say that any variables in the second formula which are not also >> > in the first formula remain as local existential variables. >> > >> > (1) EXISTS g1,g3 Grandparent(g1,g3) >> > (2) EXISTS g1,g2,g3 Parent(g1,g2) AND Parent(g2,g3) >> > >> > would become a rule like this: >> > >> > FORALL g1,g3 >> > Grandparent(g1,g3) >> > => >> > EXISTS g2 Parent(g1,g2) AND Parent(g2,g3) >> > >> > (This rule basically says that if two things have a grandparent >> > relationship, there is a third thing and they have a transitive >> > parent relationship through that third thing.) >> > >> > This may well not be full Horn logic, but I believe it's more >> > expressive than Style 1, >> >> Yes, it is, since it has existentials inside the scope of universals, >> which isn't expressible in RDF. > >You didn't directly address whether this is as expressive as Horn >rules. Well, it is Horn rules restricted to the binary case, right? So the issue is whether that reduction is universal. Having conjunctions in the conclusion is harmless.... I think. > My argument goes something like this: > >(1) We can rewrite any conjunction which uses n-ary relations as a > conjunction using just 2-ary relations, if we have local > existential variables. > > ... AND p(a,b,c) AND ... >===> > ... AND (EXISTS c1 p1(c1,a) AND p2(c1,b) AND p3(c1,c)) AND ... That is OK, as long as you are talking about a simple conjunction (as in RDF). But a rule is often thought of as an implication, and so this construction doesn't apply to it so directly. Im not sure quite what you are suggesting about how to handle rules this way. > >(2) We can rewrite any function term in a conjunction without > functions terms, if we have local existential variables. > > ... AND p(f(g(a))) AND ... >===> > ... AND (EXISTS fval,gval p(gval) AND > val(f,fval,gval) AND > val(g,gval,a)) AND ... > > where "val" is some arbitrary otherwise-unused relation (which > will actually have to get split like in step 1 to be 2-ary). This treats a function just like a relation, which is fine as long as you are not depending on the specifically functional nature, ie its having a single value; to express that, you will need to put a universal quantifier inside those existentials, which will generate more skolem functions when they occur in a query (since queries have to be skolemised 'backwards'), and you will be going in circles. Like Peter says, these reduction results tend to be very sensitive and need to be stated carefully. In particular, queries and assertions are often duals, and reductions rarely apply to both cases uniformly. The classical approach is to think of queries as negated and think of the entire inference process as finding a contradiction. That is a very 'logical' viewpoint which many find unnatural, but it does make all the logical reductions very clear :-) 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, 18 September 2001 19:51:57 UTC