RE: Expressiveness of RDF as Rule Conclusion Language (was Re: W hat is an RDF Query? )

> Can we work in both directions at the same time?   I imagine both
> inference rules and implications being useful, perhaps in somewhat
> different application spaces.

> Can someone give me a test case which shows where the difference is?

First, notice that the concept of an inference (or derivation) rule 
is more fundamental than that of an implication, because
a) (as I have already poited out) there are logics without an 
   implication connective in their object language, but which 
   still have a well-defined notion of a non-logical inference 
   rule (or sequent)
b) a genuine implication expresses inferability/derivability 
   in the object language, i.e. it is based on the deduction
   theorem (infer P -> Q if Q can be inferred from P, or, 
   symbolically, if P |- Q, resp. the sequent P => Q holds).
So, why choose a less fundamental concept (implication) for
obtaining derivations in RDF instead of its underlying more
fundamental concept inference/derivation rule? Just because
we are more used to the idea of manipulating implicational 
formulas than to manipuate a true rule set?

Second, if we deal with implications, then one would expect
that they may be arbitrarily nested, as all logical formulas
may be. But this is not the case: typical rule systems, and
virtually all practically implemented ones, do not allow for
nested arrows (this possibility is only investigated in 
"intuitionistic logic programs").

Third, this distinction is also related to the set of 
connectives admitted in the rule language. Whenever negation 
is involved in a computational formalism, we have the situation 
that it will most probably not be classical negation, since
classical negation is normally neither needed nor affordable
in such a setting (especially the tertium non datur isn't
needed and isn't affordable). Negation, in a computational 
formalism, takes either the form of negation-as-failure (which
may be viewed as classical negation under a preferential model
semantics, such as minimal or stable models), or the form of
strong negtion (a negation that does not satisfy the tertium
non datur, and need not satisfy the ex contradictione sequitor
quodlibet). Without classical logic (and classical negation),
we no longer have the equivalence of an implication with the
corresponding (non-logical) inference rule.

Okay, you may defer this clarification (that a rule is not
an implication) by making the syntactical restriction
of admitting only conjunctive (or even atomic) formulas in
rule bodies. In such a severely limited rule lnaguage, rules 
are indeed equivalent to first-degree (non-nested) implications 
in all kinds of sensible logics. But such a castrated rule
formalism will not live long. Users will soon cry for extensions
such as negation and various kinds of qualifications (valid
time, belief time, lineage, etc.). And then you have to realize
that rules are not implications.

> ... I do see how a logic program (or n3 logic RDF graph)
> could be treated as expressing a set of inference methods, it seems
> clear to me that both a pure logic program and an n3 logic graph are
> intended to be treated as logical formulas, and processed via
> generalized modus ponens.   

Real systems cannot be limited to "pure logic programs" (which are 
a purely academic concept). Real logic programs do need negation
(and much more).

-Gerd

Received on Friday, 5 October 2001 08:11:25 UTC