Pat, (01)
Any rules used by a NAF reasoner can be converted to default rules
and viceversa. (02)
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. (03)
PH> As this thread was originally about NAF, how would one use this
> method to do NAFstyle reasoning? It appears to be about default
> reasoning, which is not exactly the same (though both are, indeed,
> nonmonotonic.) (04)
I'll start with Ray Reiter's original version of default logic. He
started with a classical implication, such as (05)
(Ax)P(x) > Q(x). (06)
Then he added a special predicate beta(x), which states the normal or
default condition. His rules have the following form: (07)
(Ax)(P(x) & consistent(beta(x)) > Q(x). (08)
In many applications, beta and Q may be the same predicate. (09)
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: (010)
(Ax)(P(x) & consistent(~abnormal(x))) > Q(x). (011)
In FOL, ~abnormal(x) is consistent if and only if abnormal(x) is not
provable. Therefore, the default rule can also be written (012)
(Ax)(P(x) & ~provable(abnormal(x))) > Q(x). (013)
Since this has the form of a negation as failure, it can be processed
by a NAFstyle 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. (014)
To answer the question "How would one use this method [with a lattice of
theories] to do NAFstyle reasoning?", I suggest the following method: (015)
1. Start with the theory T that consists of all the axioms, but with
every NAF operator replaced with a classical negation sign. (016)
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). (017)
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'. (018)
4. That new theory T' is a purely classical theory from which the
same conclusion could be derived by purely classical rules. (019)
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. (020)
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? (021)
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. (022)
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. (023)
John (024)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontologforum/
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontologforum/
Unsubscribe: mailto:ontologforumleave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontologforum@xxxxxxxxxxxxxxxx (025)
