W3C home > Mailing lists > Public > public-rule-workshop-discuss@w3.org > August 2005

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

From: Michael Kifer <kifer@cs.sunysb.edu>
Date: Sat, 27 Aug 2005 18:33:23 -0400
To: Dan Connolly <connolly@w3.org>
Cc: public-rule-workshop-discuss@w3.org
Message-Id: <20050827223323.7E5BCCB5D3@kiferserv.kiferhome.com>


Dan Connolly <connolly@w3.org>:
>
> On Fri, 2005-08-26 at 21:32 -0400, Michael Kifer wrote:
> > 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?
> 
> 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?
> 
> I haven't written it out in detail, but is there some doubt that it's
> straightforward to do? Is section 7.1 Simple Entailment Rules
> of RDF Semantics insufficiently precise?
> Is there some doubt that one or more of the implementations of RDF
> graph match could be translated into KIF?


I am not sure it can be, because the number of formulas is infinite.
But this and the function symbol issues are peripheral (just doubts).
The main thing is the modus ponens issue, which you are still confused
about. See below.


> > > 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"?
> 
> 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?
> 
> I thought it was clear enough in prose, but if you like...
> 
>  (forall (?sym)
>    (=> (word ?sym)
>        (exists (?f)
>           (and (sentence ?f)
>                (= (lookup ?sym) ?f )
>             ) ) ) )
> 
> lookup is not formally constrained in any way other than
> its domain and range. Let's see.. the range is actually
> smaller than all KIF sentences; it's just the KIF
> sentences that are analagous to RDF graphs as I described
> above. I hope that's clear enough, though if necessary
> I can write it out long-hand in KIF.

I am a little nervous about this axiom, since it says that every symbol
encodes some formula. You have a quoting mechanism (so that you can talk
about terms being sentences) and then you are also requiring that, for
every symbol, lookup(sym) is also a quoted formula. I need to think what
the consequences of this might be, but I'll leave it at that, since it is
not that important to our discussion.


> > > 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."
> 
> Yes.
> 
> > 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.
> 
> Thanks...
> 
> > 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.
> 
> Well, rather let's fix it so that the set A' is both the rule...
> 
>   (=> (simply-entails-c (lookup 'car-specification)
>             '(exists (?v) (holds auto-color car ?v)) )
>       (holds auto-color car black) )
> 
> 	(simply-entails-c (lookup 'car-specification)
> 		 '(exists (?v) (holds auto-color car ?v)) 
> 
> and the antecedent.
> 
> Still just modus ponens...
> 
> > 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
> 
> 
> Didn't you just show that this is not the case for F-Logic?

Modus ponens is a basic inference rule, which is true in F-logic, Prolog,
and other LP systems.

> It seemed quite clear in your message of Thu, 25 Aug 2005 18:09:37 -0400
> http://lists.w3.org/Archives/Public/public-rule-workshop-discuss/2005Aug/0072.html


No, Dan. The argument in that message is nothing of the kind.
There was no modus ponens whatsoever.

There was a set S (I am changing the name to avoid confusion with the above
symbol A):

2 rules, one with a SNAF
several facts

There was a conclusion F, such that

     S |= F.

Note: |= here is NOT due to modus ponens!

There was also a set B of facts (just 1 fact), such that

     S + B |/=F

Where is modus ponens here?

> If we take A' = A union (= A F), i.e. the rule and the premise,
> that reduces to...
> 
>    Forall B:  A' |= F implies A' union B |= F
> 
> which which is pretty close to the definition of monotonicity that we
> agreed to earlier.

You forgot again: To show monotonicity you must establish the above
property FOR ALL FORMULAS, not just for formulas of a particular form.


> > 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.
> 
> I hope I have addressed those two issues above.
> 
> >    3. You have exhibited a bunch of formulas that have a property that
> >       holds true both in monotonic and nonmonotonic logics.
> 
> Your earlier message seems to demonstrate quite clearly that this is
> not the case.
> http://lists.w3.org/Archives/Public/public-rule-workshop-discuss/2005Aug/0072.html

It doesn't demonstrate anything of the kind that you attributed to it.
Modus ponens wasn't an issue there and it has nothing to do with what you
are trying to establish.


> >       What does it prove? Nothing.
> 
> It demonstrates that there is a useful notion of SNAF that
> is monotonic.

I need to see another demonstration. What you wrote above is not a valid
demonstration.


	--michael  
Received on Saturday, 27 August 2005 22:33:27 GMT

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