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

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.


	--michael

Received on Saturday, 27 August 2005 01:33:35 UTC