Re: [ontolog-forum] The Open world assumption shoe does not always fit

Pat,

Any rules used by a NAF reasoner can be converted to default rules
and vice-versa.

JS>> The issue of nonmonotonic reasoning is important for many practical
 >> applications, and I'd like to mention a version that I recommended in
 >> my knowledge representation book.  The method is based on prioritized
 >> defaults, as developed by Benjamin Grosof.

PH> As this thread was originally about NAF, how would one use this
 > method to do NAF-style reasoning?  It appears to be about default
 > reasoning, which is not exactly the same (though both are, indeed,
 > non-monotonic.)

I'll start with Ray Reiter's original version of default logic.  He
started with a classical implication, such as

    (Ax)P(x) -> Q(x).

Then he added a special predicate beta(x), which states the normal or
default condition.  His rules have the following form:

    (Ax)(P(x) & consistent(beta(x)) -> Q(x).

In many applications, beta and Q may be the same predicate.

One could call Reiter's beta(x) a *normality* condition.  John McCarthy
introduced an *abnormality* condition, which may be considered the
negation of beta(x).  By introducing a negation, Reiter's rule could
be written:

    (Ax)(P(x) & consistent(~abnormal(x))) -> Q(x).

In FOL, ~abnormal(x) is consistent if and only if abnormal(x) is not 
provable.  Therefore, the default rule can also be written

    (Ax)(P(x) & ~provable(abnormal(x))) -> Q(x).

Since this has the form of a negation as failure, it can be processed
by a NAF-style reasoner.  Therefore, Reiter's default rules can be
converted to a form that can be used by NAF.  Alternatively, we could
reverse the steps to convert NAF rules to default rules.

To answer the question "How would one use this method [with a lattice of
theories] to do NAF-style reasoning?", I suggest the following method:

  1. Start with the theory T that consists of all the axioms, but with
     every NAF operator replaced with a classical negation sign.

  2. Monitor the NAF inference engine to check for any step that fails
     to prove some statement p.  If that step assumes ~p, then add ~p
     to the theory T (or some previously modified version of T).

  3. Step #2 has the effect of moving through the lattice of theories
     by specializing T with added assertions ~p1, ~p2, ..., ~pN for
     some number N of applications of NAF to derive a new theory T'.

  4. That new theory T' is a purely classical theory from which the
     same conclusion could be derived by purely classical rules.

This demonstrates how a theorem prover for NAF (or default logic)
could be used to revise a theory T to enable it to prove the same
conclusion that was derived by a nonmonotonic reasoner.

One might argue that this method is parasitic on a theorem prover
that uses a nonmon logic.  Why take the trouble to use this method
for belief revision, since it presupposes a nonmon theorem prover?

The answer is that a nonmon theorem prover can be viewed as a method
for walking through the lattice of theories in order to find one
that is suitable for the current application.  That is exactly what
a belief revision method does, but a belief revision method saves
the resulting theory because it might be useful for other applications.

This is a point that Peter Gärdenfors made:  nonmon logic and belief
revision are "two sides of the same coin."  By recognizing the close
connection, it is possible to increase the toolkit of nonmon reasoning
with a broader collection of useful techniques.

John

Received on Saturday, 5 July 2008 11:37:23 UTC