[Top] [All Lists]

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

To: Pat Hayes <phayes@xxxxxxx>
Cc: semanticweb@xxxxxxxxxxxxxxx, semantic_web@xxxxxxxxxxxxxxxx, welty@xxxxxxxxxx, "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>, public-semweb-lifesci hcls <public-semweb-lifesci@xxxxxx>
From: "John F. Sowa" <sowa@xxxxxxxxxxx>
Date: Sat, 05 Jul 2008 07:36:38 -0400
Message-id: <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)

<Prev in Thread] Current Thread [Next in Thread>