From: Dan Connolly <connolly@w3.org>

Date: Thu, 25 Aug 2005 16:46:59 -0500

To: Michael Kifer <kifer@cs.sunysb.edu>

Cc: public-rule-workshop-discuss@w3.org

Message-Id: <1125006419.16011.59.camel@dirk>

Date: Thu, 25 Aug 2005 16:46:59 -0500

To: Michael Kifer <kifer@cs.sunysb.edu>

Cc: public-rule-workshop-discuss@w3.org

Message-Id: <1125006419.16011.59.camel@dirk>

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 C29EReceived on Thursday, 25 August 2005 21:47:39 GMT

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