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

Date: Fri, 26 Aug 2005 21:32:37 -0400

To: Dan Connolly <connolly@w3.org>

Cc: doug.foxvog@deri.org, public-rule-workshop-discuss@w3.org

Message-Id: <20050827013237.7F545CB5D3@kiferserv.kiferhome.com>

Date: Fri, 26 Aug 2005 21:32:37 -0400

To: Dan Connolly <connolly@w3.org>

Cc: doug.foxvog@deri.org, public-rule-workshop-discuss@w3.org

Message-Id: <20050827013237.7F545CB5D3@kiferserv.kiferhome.com>

Dan, You are confusing yourself further and further. See below. > On Fri, 2005-08-26 at 12:57 -0400, Michael Kifer wrote: > [...] > > > 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, > > Well, up to a point. But evidently F-Logic and N3 work differently > in this regard. > > > 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 was confused about how F-Logic works. I'm still studying the @ > construct in F-Logic, but it doesn't seem to be analagous > to log:includes/log:notIncludes after all. > > Leaving N3 aside, perhaps I can show what I mean by > monotonic SNAF using KIF, i.e. ordinary first-order > logic plus quoting. > > Consider a relation on (quoted) formulas: > > (simply-entails F1 F2) > > where F1 and F2 are (quoted) KIF expressions that are > analagous to RDF graphs/formulas, i.e. they > look like > > (exists (b1 b2 b3 ...) > (and (holds p1 s1 o1) > (holds p2 s1 o2) > ... > ) ) > > or in the case of no existentials, just > (and (holds p1 s1 o1) > (holds p2 s1 o2) > ... > ) > > or in the case of just one conjunct, just > (holds p1 s1 o1) > > and simply-entails is defined as per section 7.1 Simple Entailment Rules > of RDF Semantics > http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#dt-simple-entailment > > That is the formula F2 can be obtained from F1 by some combination > of erasure... > > (simply-entails '(and (holds price book1 10) (holds title book1 "abc")) > '(holds price book1 10) ) > > and existential introduction: > > (simply-entails '(holds location fred texas) > '(exists (?somewhere) (holds location fred ?somewhere)) > > and variable renaming, and re-ordering the conjuncts in an and. > > I'm glossing over the fact that "location" isn't quite a URI > for clarity. Strictly speaking, it would be something > like http\:\/\/example\/vocab\#location . > > > > This simply-entails relation is clearly an ordinary computable relation, > just like string matching or testing whether one number is a factor > of another. (It's called "graph match" in any number of RDF > implementations). > > Then consider simply-entails-c , the complement of simply-entails. > It's also computable: compute simply-entails and negate it. Here is confusion #1. Are you talking about a "relation", i.e., what exists in interpretations, or a "predicate"? What is simply-entails-c: a relation or a predicate? If it is a relation then it has no business being in a formula, which you wrote down below. If it is a predicate, then you would need to axiomatize it so that it would have the behavior you want. Where is your axiomatization? > Also, let (lookup SYMBOL) be some function that takes a (quoted) > symbol and returns some formula expression. Confusion #2: Is lookup a "function" as you stated or a "function symbol"? If it is a function, it has no business being in the formula that you wrote down below. If it is a function symbol, you have to provide axiomatization so that it would behave the way you want. Where is your axiomatization? > Now I can write my rule about car color defaults as: > > (=> (simply-entails-c (lookup 'car-specification) > '(exists (?v) (holds auto-color car ?v)) ) > (holds auto-color car black) ) > > > The (lookup 'car-specification) term denotes some expression > in each interpretation; either that expression does simply-entail > '(exists (?v) (holds auto-color car ?v)) > or it doesn't. To "add another statement" to the formula > expression we get when we look up 'car-specification is > to consider a different interpretation of the lookup function. Not sure which interpretations you are talking about, but I assume you are talking about "first-order interpretations." You are quite right that in some interpretations (simply-entails-c (lookup 'car-specification) '(exists (?v) (holds auto-color car ?v)) would be true and in some false. Let's move on. > Let A be > (simply-entails-c (lookup 'car-specification) > '(exists (?v) (holds auto-color car ?v)) > and F be > (holds auto-color car black) > > Then clearly we have > Forall B A |= F implies A union B |= F Absolutely! What you didn't notice is that actually A |/=F, so the above is vacuously true (an implication with a false premise). Obviously, this holds in nonmon logics as well. Let's try to fix this. You may have forgotten the rule, which you wrote earlier: (=> A F). Fair enough. Let AA = A union that forgotten rule, (=> A F). Then clearly AA |= F. Now, if you look carefully, what you have is A union (=> A F) |= F A modus ponens. No quarrel from me. But this is also true in nonmonotonic logics. That is, Forall A,B,F: A union (=> A F) |= F implies A union (=> A F) union B |= F This is just a direct consequence of the definition of an interpretation. (I believe, this is also true for proof-theoretic nonmon logics -- need to check Gabbay's postulates -- but this is not important for the current discussion.) > right? To the extent that you haven't shown anything: 1. You can't formalize what simply-entails-c really is. 2. You can't explain what lookup is. 3. You have exhibited a bunch of formulas that have a property that holds true both in monotonic and nonmonotonic logics. What does it prove? Nothing. --michaelReceived on Saturday, 27 August 2005 01:33:35 GMT

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