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

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?



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

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


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.

> 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

>       What does it prove? Nothing.

It demonstrates that there is a useful notion of SNAF that
is monotonic.

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

Received on Saturday, 27 August 2005 21:57:19 UTC