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

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.

Also, let (lookup SYMBOL) be some function that takes a (quoted)
symbol and returns some formula expression.

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.

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  

right?


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

Received on Friday, 26 August 2005 22:51:37 UTC