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

On Thu, 2005-08-25 at 16:30 -0400, Michael Kifer wrote:
> Dan Connolly <connolly@w3.org> wrote:
> >
> > On Thu, 2005-08-25 at 00:00 -0400, Michael Kifer wrote:
[...]
> > > Hi Dan,
> > > Welcome to the discussion! Yes, it is very important to get to the bottom
> > > of it so that everybody will start speaking the same language.
> > > 
> > > No, the above rule is nonmonotonic. If you add a color specification to
> > > that car then :car.auto:specification will now include a color
> > > specification and log:notIncludes will become false. Therefore 
> > >     :car auto:color auto:black
> > > will no longer be derived.
> > 
> > I don't understand. I understand monotonicity to mean
> > that if you can derive F from a set of formulas A,
> > then you can also derive it from the set A union B for
> > any set of formulas B.
> > 
> > You seem to be suggesting there's some set of formulas B
> > that when added to my A causes F to no longer hold.
> > 
> > Exactly what is that set of forumlas B? 
> > Feel free to answer using Flora-2 syntax if that's more convenient.
> > 
> > You say "If you add a color specification ..." which suggests that
> > B is something like...
> > 
> >   car auto:color auto:red.
> > 
> > but that doesn't falsify the premise:
> > 
> >  :car.auto:specification log:notIncludes {:car auto:color []}
> 
> I guess, I wasn't clear enough.
> 
> For you to show that your language is monotonic, you have to show that
> 
>    Forall A,B,F such that  A |= F implies A union B |= F            (*)

Yes, quite. We're clearly using the term 'monotonic' in exactly the
same way. Good...

> So, you single example didn't prove (*). To refute your main claim,
> I had to show the negation of (*), i.e., that
> 
>    Exist A,B,F such that   A |= F and  A union B |/= F              (**)
> 
> (|/= denotes "not entails").
> 
> So, I had to find A,B,F to demonstrate (**). I couldn't use your
> example directly, because that particular example didn't provide me with
> the appropriate A,B,F to demonstrate (**). (I only have to demo existence,
> i.e., find one example, while you have to show (*) for all examples!)
> So, I extended your example (or at least I thought that I did).
> 
> > Exactly what is that set of forumlas B? 
> > Feel free to answer using Flora-2 syntax if that's more convenient.
> 
> Thanks for giving me an easy way out :-)
> My example is indeed easier to use because it already has all the necessary
> formulas in it.
> 
> Let me repeat this example for easier reference:

Thanks for going slowly...

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

(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. )


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


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

> I should also say that it is dangerous for me to venture into making the
> above claims about N3, since, as far as I know, N3 doesn't have a formal
> logical semantics. So talking about logical entailment is taking too much
> liberty. But I think I have intuitive understanding of the intent and armed
> with the formal semantics of F-logic (which is close in spirit to N3) I
> feel I am making a convincing informal argument for nonmonotonicity of the
> informal semantics of N3.

The analogy between F-logic an N3 seems to work well enough in this
case, but I am not yet convinced that this example shows
nonmonotonicity. It still seems to me that you have to use
unscoped NAF to get nonmonotonicity.


[...] 
> > Monotonicity supports partial understanding...
[...]
> So, I don't buy the above argument of yours.

OK, well, I'd like to get to the bottom of this more clear
technical stuff about monotonicity first; perhaps I'll return
to the scalability discussion later...

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
D3C2 887B 0F92 6005 C541  0875 0F91 96DE 6E52 C29E

Received on Thursday, 25 August 2005 21:47:39 UTC