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

From: Sandro Hawke <sandro@w3.org>
Subject: Re: Is n3 a rules language or a logic language? 
Date: Thu, 05 Sep 2002 13:51:31 -0400

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

Hmm.  I missed the implications of ``sufficiently complete''.  

Reading it this way you appear to be saying that any reasoner that does
only this sort of reasoning will only do this sort of reasoning.  I don't
view this as particularly insightful.

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

What you are saying is that p |- q is a sound inference rule in a theory
that includes p implies q.  Granted.


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

Yes, but this is *very* different from what you said before.

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

No, as stated above.

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

Agreed.

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

As N3 includes some sort of negation (or, at least some versions of N3 do),
the difference is noticable.

One way of characterizing rules of inference is to show that they are sound
and complete with respect to some a syntax and a model theory.
Characterizing rules of inferences as sound is somewhat useful, but not
very useful, as there are many rule of inference that are sound, but
useless.  (Consider rules of inferences with no premises and a particular
tautology as the conclusion.)

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

No.  Not even for a rules engine that works more-or-less as one might
expect.  Let's say that a rule engine takes a collection of formulae as
input and generates a collection of formulae as output.  The rules engine
works internally by testing to see if the premises of a rule appear among
the formulae, and, if so, adds the consequences of the rule to the
formulae.  Moreover, the rules engine can't stop until no unrun rules
remain.

Now in the former case the rule engine can produce an empty collection of
formulae as a result (given an empty collection as input) whereas in the
latter case will always include the conditional in its 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.)  

These can be different.

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

I don't think that this works as resolution is only refutation-complete.

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

peter

Received on Thursday, 5 September 2002 14:26:05 UTC