From: Harold Boley (boley@informatik.uni-kl.de)
Date: 11/13/02
Sandro Hawke wrote: . . . > 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. Interestingly we are close to Dale Miller again, who did Lambda-Prolog: http://www.cse.psu.edu/~dale/papers/jsc92.pdf > 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). Robert Kowalski employed a similar 'flattening' for user-defined functions (and possibly also for Skolem functions). In Relfun I employ both kinds, but just keep the explicit equality instead of introducing new predicates. Notice that we are now in a Datalog with equality, anyway. . . . > To remind ourselves of the point here: RDF graphs are more expressive > than FOL atomic sentences. Yes, because their bNodes logically introduce existential quantifiers. In slide 6 of "RuleML Meets RDF" (http://www.ruleml.org/rdf/ruleml-rdf.pdf) I will thus need to find a formulation even weaker than "RDF-like triples" next to the sublanguage 'urc-bin-data-ground-fact'. Also, in RuleML we need to think harder about introducing explicit (existential) quantifiers, as long asked for by Drew McDermott. The label "RDF triples" could then be put next to the sublanguage 'existential-conjunctive urc-bin-data-fact' (no longer 'ground' because of the existential variables). > The logic-function terms and n-ary > predicates in FOL are essentially just syntactic sugar; See above. > 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. Datalog and Horn logic without equality. > 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. Well, ignoring the Skolem function issue for a moment, the 'existential- conjunctive' power of RDF triples will also move RDF rules to a more expressive position in the sublanguage hierarchy. But again, 'simulating' Skolem functions by existentially quantified variables at the same time puts us into a FOL with equality. > 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. "RDF rules" is a much less well-defined term than "RDF triples", and in RuleML we are happy to reclassify RDF rules into the most appropriate position in the hierarchy once we understand them better. As I hinted at in a different thread, it should be helpful to exchange our experience with rule engines such as cwm/n3 and Mandarax/RuleML or j-DREW/RuleML. Harold
This archive was generated by hypermail 2.1.4 : 11/13/02 EST