Re: nature of anon resource [was Re: log:forSome]

>[...]
> >>that's indeed a very good point about skolemization
> >>in the case that 'we are not in the scope of a universal
> >>quanitifer' we have indeed a full blown *constant*
> >>but I think that in general you can not make that
> >>assumption (your piece of RDF *could* fall in the
> >>scope of many univerally quantified variables (I mean
> >>when used by outside-core things)
> >
> >WHAT??!!!???? How??? (How can anything outside a document project a
> >quantifier scope across that document??)
> >
> >That is an amazing idea, and suggests an entirely new picture of how
> >the semantic web might work, but if we really think this is possible
> >then we should get it clear ASAP, as it completely changes the ground
> >rules. For example there is no such thing as an assertion, since
> >anything might be only a subexpression of something outside the
> >document.
>
>A SAP would help here (such a hot weather...)

Hey, you should be in Florida, 98F and 100% humidity, even the buildings sweat.

>
>OK, let's take e.g. the following piece of RDF
>(which is at http://www.agfa.com/w3c/n3/ext.n3)
>
>/////
>:s0 :is [ :p1 :o1; :p2 :o2].
>:s0 :p3 :o3.
>\\\\\
>and onother one (which is at http://www.agfa.com/w3c/n3/ext-rules.n3)
>
>/////
>  {{:u :is [ :p1 :x; :p2 :y]. :u :p3 :z} log:implies
>{:u :is [ :p1 :x; :p2 :y; :p3 :z]}} a log:Truth; log:forAll :u, :x, :y, :z.
>\\\\\

Just as an aside: that universal quantifier is scoped by the outer 
pair of { }, ie it is entirely inside the document 
http://www.agfa.com/w3c/n3/ext-rules.n3, right?

>then the query (which is at http://www.agfa.com/w3c/n3/ext-query.n3)
>
>/////
>{:s0 :is :z} log:forSome :z.
>\\\\\

What indicates that this is a query? (Is there any syntactic distinction?)

Not just a quibble, because in many usages, calling something a 
'query' effectively inverts all its quantifiers, so that an 
existential in a query is like a universal in an assertion. If you 
are following this common convention, then the log:forSome, while 
logically correct, is potentially misleading: it is 'functionally' 
exactly like a universal, so that the :z variable can be bound to 
anything. (In Gentzen terminology, it is on the other side of the 
sequent, so all the intro/elimination rules are inverted. In LP 
terms, the goal is negated and then you test for unsatisfiability.) 
Notice it would be a logical error to skolemise an existential *in a 
query*; a query isn't being asserted.

>will result in (which is at http://www.agfa.com/w3c/n3/ext-result.n3)
>
>/////
> {:s0 :is [ :p1 :o1; :p2 :o2].
>  :s0 :p3 :o3} log:implies
>{:s0 :is [ :p1 :o1; :p2 :o2; :p3 :o3]}.
>
>:s0 :is [ :p1 :o1; :p2 :o2].
>\\\\\
>
>so there is some kind of changed 'extension of objects'

No, you are just doing conventional reasoning here, with universals 
in the axioms (assumptions) and existentials in the goals (queries, 
conclusions) , both of which mean that all variables can be freely 
matched to anything. All your quantifiers are 'universal' in this 
sense, and all their scopes are local to their documents; nothing 
projects or extends from one document into another, but since the 
variables are all universal, they can be bound to terms (names) 
occurring in other documents.

(All of this assumes that all the documents are talking about the 
same universe, so it is kosher to just smurge together assertions 
from different sources and draw conclusions from them as thouh they 
were all in one document. This is probably too naive a perspective 
for the entire web; but that gets us into a minefield which is beyond 
the scope of this WG.)

>(there must be some link with SKIF here)
>
>OK, we have identified an anonymous node by its content
>in the sense of
>  a (not *the*) thing which has as 'least common'
>  certain descriptions
>and it is kind of 'by value' (not 'by reference')
>but is that a problem?

I think that your use here of universal quantifiers goes way beyond 
RDF. All your variables are universal.

Pat

---------------------------------------------------------------------
IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax
phayes@ai.uwf.edu 
http://www.coginst.uwf.edu/~phayes

Received on Thursday, 28 June 2001 11:11:29 UTC