Re: Is n3 a rules language or a logic language?

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 Research

Received on Thursday, 5 September 2002 12:00:08 UTC