Is n3 a rules language or a logic language?

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 UTC