From: Sandro Hawke <sandro@w3.org>

Date: Thu, 05 Sep 2002 11:00:55 -0400

Message-Id: <200209051500.g85F0tS14067@wadimousa.hawke.org>

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

Date: Thu, 05 Sep 2002 11:00:55 -0400

Message-Id: <200209051500.g85F0tS14067@wadimousa.hawke.org>

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

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. 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". 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. 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". 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}". 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. 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. -- sandro http://www.w3.org/People/Sandro/Received on Thursday, 5 September 2002 11:03:13 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Monday, 7 December 2009 10:53:09 GMT
*