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

Michael Kifer wrote:
> 
> Inference rule is a useful way to think of it at an intuitive level.
> However, the only version of CWA that is defined as an inference rule that
> I know of is NAF. Not what is being called NAF in this discussion thread,
> but the real NAF, as in Prolog.
> 
> All the other popular versions of CWA (well-founded, stable,
> circumscription) use model-theoretic definitions or axiomatic.

I stand corrected: I had Clark's NAF in mind.

> Then you are checking whether S3 still entails F, and sure enough it does.
> So, you conclude it is monotonic.

Point taken: I tried so hard to hide the assert that I did not notice it 
myself!

> But here you have "monotonicity" for
> formulas of a certain kind (the same problem as Dan had), not for all
> formulas. As far as I recall, according to so called Gabbay's postulates,
> *every* *non*monotonic logic also has the property that if S |= F then
> S+F+something |= F.
> In any case, the most popular CWA flavors (the well-founded and stable
> models) do have the above property.
> So, your argument in the use case doesn't establish anything as far as
> monotonicity goes.

I fear that it had more to do with the ostrich's postulate than 
Gabbay's. Something like: S |= F, but S + B |\= F? No problem: just 
ignore B! (What do you tell me, S |= F is non-monotonic nonetheless?)

What? Me? Foolish?

> What we should do is to remove the clause that NAF is out of scope and
> remove the reference to monotonicity. Then let the WG deal with it.

I could leave with that, but for the fear of that being Pandora's box...

Christian

Received on Thursday, 1 September 2005 09:05:33 UTC