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

[ thread turning hard left, towards greater precision; hang on... ]

> > 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.  [corrected]

Yes, I understand this.  My term "sufficiently-complete" was meant to
indicate to readers familiar with modus tollens, resolution, and other
common inference rules that I was aware there were such rules but
thought they would cloud the issue more than clarify it.

What I meant was that the logical reasoner would produce everything
the rules engine would produce _and possibly more_.  I'm sorry for not
saying that.

> > 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.

But you would agree with this:

   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) all the results you would get
   from a rules engine (and possibly more).

?

> > 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). 

That's exactly what I'm trying to settle here.  The meta-question is
how much we need to settle it, if the material conditional and a proof
rule are indistinguishable in some large set of situations.  Or to put
that differently, if Tim wants to think of log:implies as constructing
proof rules, can I define it as the material conditional without
actually causing any problems?

> > 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.

I believe TimBL consideres it to be a proof rule constructor, and I'm
exploring whether it wouldn't be better considered to be the material
conditional.  I think he prefers the proof-rule approach as being more
general (and probably also as more obvious to many prospective users
and implementors; and perhaps as higher performance).  I now beleive
it's only more general when you use it indirectly, as a kind of
meta-logic.  Doing that is fine, but it doesn't mean that the
rules-language is more expressive; rather it means it's enough less
expressive that you find yourself wanting to use it as a meta-logic to
define the stuff you really want.

> > 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.

Absolutely.  So a sound and complete FOL reasoner would output all
that cwm would output, and quite possibly more.  As long as the
language does not include negation, however, I doubt there would be
much of interest in that additional output.  I'd like to characterize
that more precisely at some point.

> > 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.

Let's say the inference rule data is going to be used as a rules by a
rules engine, and material conditional data is going to be used as
data by a rules engine using only modus ponens.   Will you get the
same output?

In other words

    for all formulas x, e(mp + r(n), x) = e(mp, f(n) & x)

where 

    n -- an n3 document containing only log:implies rules
    r(n) -- a set of rules produced from n by considering log:implies to 
            define rules
    f(n) -- a logical formula produced from n by considering
	    log:implies to be the material conditional
    mp -- the rule modus ponens
    res -- the resolultion rule (which is sound and complete for FOL)
    + -- operator to conjoin two sets of rules
    & -- operator to conjoin two logical formulas
    e(R, I) -- the set of formulas produced by some rules engine 
	       using rule R on input data I.   (Or perhaps I should
	       call this the closure of applying rules R on formula
	       I, to get away from performance and implementation
               issues.)  

This is not exactly what I meant in the previous message; I'd
forgotten the mp on the left.

I also assert using resultion and f(n), we would conclude everything we
would conclude from using r(n), and possibly more:

   for all formulas x, there exists formula y such that
         e(r(n), x) & y = e(res, f(n) & x)
	
(This gives me a fun idea for a cwm test: write resolution in n3, and
see what things I can get cwm to prove.   I bet I can get cwm to prove
this isn't the way to implement a fast theorem prover.  :-)

   -- sandro

Received on Thursday, 5 September 2002 13:53:51 UTC