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

doug.foxvog@deri.org wrote:
> Michael Kifer wrote:
> > Dan Connolly <connolly@w3.org> wrote:> 
> >>On Thu, 2005-08-25 at 16:30 -0400, Michael Kifer wrote:
> >>[...] 
> >>>    We assume that the info about the cars (over which we are going to
> >>>    close off) is in module allAboutCars and the facts there have the form
> >>>
> >>>    12345:car[color->red].
> >>>    45678:car[color->blue].
> >>>    ...
> >>>
> >>>    The 12345 thing is supposed to be the vehicle id number or something.
> >>>    The first fact says that 12345 is an object in class car and the attribute
> >>>    color has the value red, etc.
> >>>
> >>>    The above info on cars could be on some Web site, for example.
> >>>
> >>>    Now, to express N3's
> >>>	this log:forAll :car.
> >>>	{ :car.auto:specification log:notIncludes {:car auto:color []}}
> >>>	    => {:car auto:color auto:black}.
> >>>
> >>>    one would write something like this:
> 
> >>>    ?X[realColor->?Color] :- ?X[color->?Color]@allAboutCars.      (***)
> >>>    ?X[realColor->black] :- not ?X.color[]@allAboutCars.          (****)
> 
> >>>    The first rule says that if the module allAboutCars has an explicit color
> >>>    for a car, then it is the real color of that car. You don't have this rule
> >>>    in your N3 example, but of course it is easy to add.
> 
> >>>    The second rule says that if allAboutCars says nothing about a particular
> >>>    car's color then its color is black. This is a counterpart of your default
> >>>    rule, which involves log:notIncludes.
> >>>
> >>>Now, let us assume that all the above formulas constitute the set A in (**).
> >>>
> >>>Let's suppose 00007 is a car on the allAboutCars site, for which no color
> >>>information is available. Let 00007[color->black] be our formula F in (**).
> >>>
> >>>Because allAboutCars says nothing about the color of 00007, we conclude
> >>>that 00007.color[] is false (00007.color[] means that there is some value
> >>>for the color attr in object 00007. We didn't find any, so it's
> >>>false).
> >>
> >>Are you abbreviating there? I would think we conclude that
> >> 00007.color[]@allAboutCars
> >>is false.
> 
> > Yes, 00007.color[]@allAboutCars. Sorry for the typo.
> 
> >>(aside: In any case, in N3, the negation is not separated from the
> >>question of whether 00007.color[] occurs in allAboutCars.
> >>In N3, the notIncludes relation between syntactic formulas is just
> >>like stringNotMatch operation on strings or a notDivisorOf operation
> >>on integers; it's a decideable/computable recursive function. )
> 
> Thus a notIncludes relation cannot be asserted as part of the set of
> formulas.  It is outside the language for describing Set A.


Just for the record: the above (aside: ...) was written by Dan, not me.
I agree with you that logically this is meaningless.


> > I would be more comfortable if this all were defined more formally.
> > I gave my best shot at informally talking about informal semantics of N3,
> > but we cannot really argue about logical properties of a language that
> > hasn't been given a model theoretic semantics.
> 
> >>> Therefore, we derive 00007[color->black] using the rule
> >>>(****). (The rule (***) doesn't fire, since its premise is false.)
> >>>Therefore,
> >>>
> >>>        A |= F
> >>>
> >>>Now, let B be 00007[color->yellow], which we would like to add to the
> >>>allAboutCars site.
> 
> >>add to the site? You mean change what @allAboutCars denotes? To do
> >>that is to consider a different interpretation of the formula(s) A,
> >>not to consider an additional set of formulas B.
> 
> > No. We have a bunch of formulas
> 
> This seems to be where the argument lies.  Dan is considering 
> @allAboutCars to be a set of formulas, while Michael is considering it
> to be a bunch of formulas (or possibly a container of or a pointer to a
> bunch of formulas) that happen to exist in a logical world.  Not knowing
> N3, i can't judge whose interpretation is correct.
> 
> Mathematical sets are unchanging: one cannot add something to a set and
> still have the same set.  Monotonicity is about adding formulas to a
> logical world.
> 
> If @ is merely a namespace identifier, it wouldn't be a reference to a
> set, merely a method of abbreviation.  It seems unlikely to me that N3
> fixes in stone any namespace as soon as an "@" sign is used to indicate
> it.  Again, with the caveat that i don't know N3, it seems that Michael
> is correct, and adding the formula B does not "change what @allAboutCars
> denotes".

No, I think Dan and I mean the same thing, but uses the words "set" and
"bunch" informally. I think Dan was confused as to what "inference" means
in nonmonotonic logics (judging by his remark that I was using two different
interpretations for the set of formulas A).

I think Dieter's mini-tutorial, which he sent earlier, (and Gerd's
additions) should help understand the issue. Just to make everybody bored,
I would like to add yet another clarification to that tutorial.

   As Dieter/Gerd explained,
   In FOL  A |= F means that F is true in EVERY model of A.

   In a nonmonotonic logic, every formula in the language (which typically
   is a strict syntactic subset of FOL, not the whole FOL) has an
   associated set of "canonic" or "intended" (terminology varies) models.
   So, in such a logic,  A |= F means that
      F is true in every model in IntendedModels(A).

   Now, here is the IMPORTANT PART:  In FOL, if A is a subset of B then
   AllModels(A) is a superset of AllModels(B) -- a property that is
   responsible for the monotonicity of inference.

   In CONTRAST, in nonmon logics,  IntendedModels(A) don't have any particular
   relationship with IntendedModels(B). They can be sub/supersets, or they
   may be disjoint -- anything goes.

   For instance, the intended model of

      p(?X) :- q(?X)

   is one where everything is false.
   The IM of

      p(?X) :- q(?X).
      q(a).

   is one where q(a), p(a) are true and everything else is false.
   These two models are different and hence their IntendedModels sets are
   disjoint.

   This is precisely what happened in the example we were discussing with Dan
   (the same example about car colors expressed both in N3 and Flora-2).

   Originally, we were considering whether

        A |= 000007[color->black]@allAboutCars                        (1)

   It turned out that if we look at the intended model of A then
   000007[color->black]@allAboutCars was true, so the above entailment (1)
   is correct in that logic. Then we considered whether

        A union B |= 000007[color->black]@allAboutCars                (2)

   Here, the intended model of A union B was different from the intended
   model of A alone. It so happens that in the intended model of A union B
   the statement 000007[color->black]@allAboutCars is false and, therefore,
   the entailment (2) is incorrect. So, the inference based on SNAF falls
   precisely under the standard definition of nonmonotonic reasoning.

Hope this helps.


	--michael

Received on Friday, 26 August 2005 16:58:49 UTC