W3C home > Mailing lists > Public > public-rule-workshop-discuss@w3.org > August 2005

Re: SNAF, NAF, and monotonicity [was: Comments on * DRAFT * Rules...]

From: Michael Kifer <kifer@cs.sunysb.edu>
Date: Tue, 30 Aug 2005 15:51:51 -0400
To: Christian de Sainte Marie <csma@ilog.fr>
Cc: Dan Connolly <connolly@w3.org>, public-rule-workshop-discuss@w3.org
Message-Id: <20050830195151.CAF4ECB5D3@kiferserv.kiferhome.com>


> 
> Michael Kifer wrote:
> > 
> > There was a set S (I am changing the name to avoid confusion with the above
> > symbol A):
> > 
> > 2 rules, one with a SNAF
> > several facts
> > 
> > There was a conclusion F, such that
> > 
> >      S |= F.
> > 
> > Note: |= here is NOT due to modus ponens!
> > 
> > There was also a set B of facts (just 1 fact), such that
> > 
> >      S + B |/=F
> 
> Could it be that the misunderstanding comes from how you think of the 
> CWA? (Forgive me if I misuse formal notation below: I hope that the 
> intended meaning remains clear)

CWA, monotonicity, etc., are very well-defined and understood concepts.
I think of them exactly as they are defined and the same way as people who
are familiar with the field think of them.

I am not trying to put anybody down by saying this. What I am saying is
that there is no need for guesswork, handwaving, etc. All this is
well-known and really simple as long as you take some time to study the
issues.

Please refer to the mini-tutorial that Dieter sent around a few days
ago. It is a good place to start.

> If you think of CWA as an inference rule (like modus ponens), you get
> 
> CWA: rule with SNAF and several facts |= some negated facts {~Fi}
> 
> Modus Ponens: other rule and several facts + {~Fi} |= F
> 
> So that, really, S |= {~Fi} + F
> 
> Now, if you add {Fi} to S, you cannot infer {~Fi] anymore, and without 
> them, you cannot infer F anymore:
> 
> S + {Fi} |\= F

S/NAF can be informally thought as an inference rule (a good way to
introduce the concept), but formally this is always defined
model-theoretically. So, the above doesn't make much sense to me.
Consequences are not determined by a sequence of inference rules.


> Now, if you think of CWA as a property of the world (to be closed, I 
> mean) for which SNAF is an indicator, then


Which means what?


> S really is:
> 2 rules, one with classical negation (you do not need SNAF anymore once 
> you make everything explicit)
> several facts
> {~Fi}
> 
> then, you have
> 
> Modus Ponens: S |= F
> 
> but you do not have S + {Fi} |\= F, because S + {Fi} is inconsistent.

If you have complete knowledge of the world, i.e., know all positive and
negative facts, then there is nothing to discuss. This is plain classical
logic, and it HAS NOTHING TO DO WITH CWA.

If we had complete knowledge of the world then there would need to be fewer
logicians around and CWA would not even get on anybody's mind.  The whole
problem is due to the fact that negative facts are typically not known and
there is often a need to infer them based on the available incomplete
knowledge.

> I do not claim that the second interpretation is correct: I just wonder 
> whether this is not what Dan really had in mind when he challenged your 
> addition of OO7car being yellow in S to prove nonmonotonicity?

The issue was that he failed to prove monotonicity and even explain his
notion of "SNAF".

1. To prove monotonicity, one has to show that FOR ALL kinds of formulas
   A,B,C in the language, A |= C implies A+B |= C.

2. He showed (1) only for ONE KIND of formulas.
   Worse, for this particular kind of formulas the above property holds for
   EVERY NONMONOTONIC system as well. So, this didn't demonstrate anything.

Regarding his challenge of the addition of OO7car, he mistakenly thought
that my example (in another message) contradicted property (2) above.
The excerpt (from my msg) that you are quoting at the top of your message
explains why this is not the case.


> At least, I believe this is what I had in mind when I introduced the 
> farfeluesque notion of "bounded monotonicity": in the same way like you 
> need not take into account facts out of the scope of my SNAF if you need 
> only reason within that closed world (and thus you do not need 
> nonmonotonic inference), you can safely reason monotonically if you know 
> that you stay within the bounds where your world is monotonic (yes, this 
> look a lot like a definition of nonmonotonicity, but it is not, really: 
> if I am born, do queries and draw inferences from a database and then 
> die before any change affects that DB - within the bounds of that DB 
> monotonicity -, then, for all practical purposes, that DB is monotonic, 
> as far as I am concerned).

Again, the notion of monotonicity is well-defined and well-established.
Database query languages are nonmonotonic according to the
established definition of nonmonotonicity (which was repeated numerous
times on this list, including this very message). There can be no
difference of opinion about it.

Regarding your paragraph above, I would have answered it in a more concrete
way, if I could only understand it...


> Once again, I am not trying to say that bounded monotonicity makes sense 
> or whatever.
> 
> I am just wondering if we would not all agree that we need not care 
> about nonmonotonicity as long as the interchange language provides a way 
> to make clear the scope (of NAF, and of other nonmonotonicity-generating 
> operations, if there are any and they are required): the applications 
> that want to use the retrieved rules have to care about it, if they want 
> to reason outside that scope.


We don't need to care about anything. We just need to understand what the
issues are and be aware of simple things that have been known for decades.

This whole thread started because the draft charter contained several
contradictions. Clearly, it is not healthy to base one's work on a document
that is internally contradictory. All we did was to point this out.


	--michael  



> And, yes: I am perfectly aware that, maybe, none of this makes sense :-)
> 
> Christian
> 
> 
> 
Received on Tuesday, 30 August 2005 19:52:04 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Tuesday, 8 January 2008 14:16:23 GMT