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