From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>

Date: Thu, 05 Sep 2002 11:59:42 -0400 (EDT)

Message-Id: <20020905.115942.113951766.pfps@research.bell-labs.com>

To: sandro@w3.org

Cc: www-rdf-rules@w3.org, timbl@w3.org

Date: Thu, 05 Sep 2002 11:59:42 -0400 (EDT)

Message-Id: <20020905.115942.113951766.pfps@research.bell-labs.com>

To: sandro@w3.org

Cc: www-rdf-rules@w3.org, timbl@w3.org

From: Sandro Hawke <sandro@w3.org> Subject: Is n3 a rules language or a logic language? Date: Thu, 05 Sep 2002 11:00:55 -0400 > In trying to understand TimBL's intended semantics for n3, I've found > two different ways of looking at the language. I think they correspond > to it being considerd (1) a rules language or (2) a logic language. > > Informally, the question is whether "p implies q" should be understood > as (1) "if you have p in your collection of true statements, you may > add q to your collection of true statements", or (2) "you should know > that if ever p is true, q is also true". > > The first is an inference rule, properly written as "p |- q" or > p > --- > q > and the second is a logic sentence using the "material conditional" or > "implication" logical connective, variously written as > p=>q > p->q > p [a curve looking kind of like a backwards C] q > > In a rules language, "p implies q" (p |- q) tells you what you can do, > while in a logic language, "p implies q" (p -> q) tells you a general > fact. The general fact may be used according to some rules to produce > other facts. I believe that the situation is more complex than this. There is a distinction to be made between statements in a logic and the meaning of such statements. As I understand it, the material conditional is a statement in a logic, so one can say things like: ( p implies q ) or ( r implies s ) On the other hand, a rule of inference is part of the meaning of logic, generally part of a proof theory for the logic. So, for example, modus ponens is a rule of inference, written in one style of writing rules of inference as a , a implies b -------------- b This should be read as ``If you have concluded a, and you have concluded that a implies b, then you can conclude b.'' On the other hand a --- b is a different rule of inference, which should be read as ``If you have concluded a then you can conclude b.'' There is a connection between the two that roughly goes as follows. If you have concluded that a implies b, then if you conclude a you can also conclude b. However, this derived rule does *not* carry the entire meaning of a implies b. For example, most proof systems that include modus ponens also include modus tolens, a proof rule that looks like not b, a implies b ------------------ not a > A logical reasoner knowing one particular rule (which I think is > "modus ponens": A, A->B |- A) will do the same thing given "p->q" as a > rules engine would if it were given "p |- q". In fact, a reasoner > using any other sound and sufficiently-complete set of inference rules > would act the same given "p->q" as a rules engine would with "p |- q". This is definitely not true. A rules engine with p |- q will not conclude anything from not q whereas a complete reasoner for the propositional calculus will conclude not b from not a and a implies b. > More generally, if you turn the "|-" into "->" in any collection of > rules, and feed the rules to a reasoner using at least modus ponens, > the reasoner will produce (eventually) the same results as the rules > engine. Again, not true. > Let's apply this to n3. cwm is a rules engine; TimBL thinks of > log:implies as constructing a rule. For example, he is happy to write > > # n3 example 1 > { :a :b :c } > log:implies > { { :d :e :f } > log:implies > { :g :h :i } > }. > > and describe that as one rule which, if triggered by the presence of > ":a :b :c" will cause the addition of a second rule. That second > rule, if triggered by the presense of ":d :e :f" will cause the > addition of ":g :h :i". Here one of the problems with N3. There is no indication in N3 of whether log:implies is supposed to be material implication, a proof rule, or some other logical connective (such as, for example, some sort of relevance implication). > On the other hand, if we treat log:implies as a logical implication > operator, it's clear you can rewrite the sentence above as: > > # n3 example 2 > { :a :b :c. :d :e :f } > log:implies > { :g :h :i } > > which has the same final effect. (You might worry the inner rule > will only be inferred in the rules-style, not in the logic-style. > That's not really true; a reasoner using sufficiently-complete > inference rules would also infer from example 2, given ":a :b :c" that > "{:d :e :f} log:implies {:g :h :i}". Again this depends on what the meaning of log:implies is. > Is there any way to distinguish what cwm does from what a sound and > complete FOL reasoner would do with the same inputs? I don't think > so. I do not know how cwm works. However, my guess is that it is incomplete with respect to the propositional calculus. > If one were using such a reasoner, one might be tempted to add > negation to the language (because there's no additional cost), which > could be interesting and useful. But that's a different issue. > > My conclusion is this: we can treat log:implies as either creating an > inference rule ( |- ) or as the material conditional ( -> ); from the > outside no one will be able to tell the difference. Not true, or, at least, not true without the presence of some other machinery. > -- sandro http://www.w3.org/People/Sandro/ > Peter F. Patel-Schneider Bell Labs ResearchReceived on Thursday, 5 September 2002 12:00:08 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 20:49:37 UTC
*