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

Date: Thu, 25 Aug 2005 18:09:37 -0400

To: Dan Connolly <connolly@w3.org>

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

Message-Id: <20050825220937.C46AACB5D3@kiferserv.kiferhome.com>

Date: Thu, 25 Aug 2005 18:09:37 -0400

To: Dan Connolly <connolly@w3.org>

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

Message-Id: <20050825220937.C46AACB5D3@kiferserv.kiferhome.com>

Dan Connolly <connolly@w3.org> wrote: > > 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. 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. ) 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 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. > > 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. Unscoped NAF doesn't exist (only implicitly scoped NAF exists), so according to you nonmonotonicity doesn't exist :-) > > [...] > > > 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... Looks like a good plan. --michaelReceived on Thursday, 25 August 2005 22:09:50 GMT

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