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

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.

> 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".

If this is the case, adding the formula B to @allAboutCars, results in

	A union B |/= F

> 12345[color->red].
> 45678[color->blue].
> 
> at allAboutCars. Formally, being at allAboutCars means that all predicates
> and methods there have a unique prefix (the same for the same module). So,
> the above two being @allAboutCars really means that we have formulas like
> 
> 12345['$&^allAboutCars*^%color'->red].
> 45678['$&^allAboutCars*^%color'->blue].                         (*****)
> etc.
> 
> Adding 00007[color->yellow] to @allAboutCars means that B really is
> 
> 00007['$&^allAboutCars*^%color'->yellow]                        (******)
> 
> and now we have the set of formulas A union B.
> 
> Recall that A was that bunch of formulas (*****) plus those pair of rules.
> So, A union B is (*****), (******), and the rules (***)/(****).
> 
> Now we are making inference and what was a consequence of A is no longer a
> consequence of A union B.
> 
> 
> 
>>> Now, rule (***) fires, but (****) doesn't. So, we derive
>>>00007[color->yellow], but we don't derive 00007[color->black]. Therefore,
>>>
>>>        A union B |/= F
>>>
>>>so it is nonmonotonic.
>>>
>>>
>>>The same thing basically happens in your N3 example.
>>>
>>>There auto:specification is an attribute, which returns a set of objects
>>>(which would formally be treated as terms). Somewhere you will need to
>>>have a set of formulas (which will be part of the set A), which
>>>would say which specific cars have which specifications.
>>>
>>>So, if you have a car whose spec doesn't include color then you will derive
>>>{... auto:calor auto:black} for that car. But if you throw in another
>>>formula (our B above), which will give a color spec to that car then
>>>{ :car.auto:specification log:notIncludes {:car auto:color []}}
>>>will not be satisfied and so the rule will not fire.
>>
>>As I say, it seems to me that this is not exhibiting another set
>>of formulas B, but just considering a different interpretation of
>>the formulas A. In that interpretation, the premise is false and
>>the conclusion is false, yes, but this doesn't seem to demonstrate
>>non-monotonicity.

> No, see above. It is a union of A and B. It is precisely what
> nonmonotonicity means.

> ...
> 	--michael 
==========================================================
douglas foxvog	  doug.foxvog@deri.org	 +353 (91) 495 150
Digital Enterprise Research Institute (DERI)
National University of Ireland, Galway
Galway, Ireland				http://www.deri.ie
==========================================================

Received on Friday, 26 August 2005 09:48:03 UTC