- From: Tim Berners-Lee <timbl@w3.org>
- Date: Tue, 10 Sep 2002 11:16:14 -0400
- To: Sandro Hawke <sandro@w3.org>
- Cc: www-rdf-rules@w3.org
I like your exposition of the difference and the way you conclude that there i sno real difference when seen from the outside. And what is seen from the outside is, on the web, often what matters. I see a log:implies statement as being an assertion. I see cwm as only one way of using such assertion implication as rules. In practice many n3 files I write are written on the understanding that they will be used in a particular way, for example by merging them with data, finding the deductive closure, and filtering out things from the result. And using them differently doesn't produce the needed results. But in this case, the rules and the data are all used as true statements. So any other system could reuse them validly. I think the concept of a difference between a rule and a statement is a trap. Like the difference (argued to bits on the list from time to time!) between entailment and implication. The fact is that you can take one logic in which something occurs as an axiom, expressed as an entailment, and convert the same data into another logic in which there is a general axiom for an implication operator, and then the same information originally in an axiom is expressed as a a ground fact using implication. Within a logic, the difference is fundamental. But when you share the data on the web, the meaning is the same. Tim On Thursday, September 5, 2002, at 11:00 AM, Sandro Hawke wrote: > 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 Tuesday, 10 September 2002 11:16:16 UTC