ontolog-forum
[Top] [All Lists]

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

 To: Pat Hayes semanticweb@xxxxxxxxxxxxxxx, semantic_web@xxxxxxxxxxxxxxxx, welty@xxxxxxxxxx, "[ontolog-forum]" , public-semweb-lifesci hcls "John F. Sowa" Sat, 05 Jul 2008 07:36:38 -0400 <486F5CC6.2080307@xxxxxxxxxxx>
 ```Pat,    (01) Any rules used by a NAF reasoner can be converted to default rules and vice-versa.    (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 NAF-style reasoning? It appears to be about default > reasoning, which is not exactly the same (though both are, indeed, > non-monotonic.)    (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 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.    (014) 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:    (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/ontolog-forum/ Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/ Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx Shared Files: http://ontolog.cim3.net/file/ Community Wiki: http://ontolog.cim3.net/wiki/ To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (025) ```
 Current Thread Re: [ontolog-forum] The Open world assumption shoe does not always fit, John F. Sowa Re: [ontolog-forum] The Open world assumption shoe does not always fit, Pat Hayes Re: [ontolog-forum] The Open world assumption shoe does not always fit, John F. Sowa <=