From: Wagner, G.R. <G.R.Wagner@tm.tue.nl>

Date: Fri, 5 Oct 2001 14:11:19 +0200

Message-ID: <511BB18E82E9D11188230008C724064602D9DE02@tmex1.tm.tue.nl>

To: "'Sandro Hawke '" <sandro@w3.org>, "'Drew McDermott '" <drew.mcdermott@yale.edu>

Cc: "'www-rdf-rules@w3.org '" <www-rdf-rules@w3.org>

Date: Fri, 5 Oct 2001 14:11:19 +0200

Message-ID: <511BB18E82E9D11188230008C724064602D9DE02@tmex1.tm.tue.nl>

To: "'Sandro Hawke '" <sandro@w3.org>, "'Drew McDermott '" <drew.mcdermott@yale.edu>

Cc: "'www-rdf-rules@w3.org '" <www-rdf-rules@w3.org>

> 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). -GerdReceived on Friday, 5 October 2001 08:11:25 UTC

*
This archive was generated by hypermail 2.4.0
: Friday, 17 January 2020 22:46:14 UTC
*