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

>[...]
> >>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?
>
>its scope is the outer pair of { }
>document scope would be
>  this log:forAll :u, :x, :y, :z.
>
> >>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?)
>
>you are right, there is no syntactic distinction
>it's just that such documents should not be 'asserted'
>
> >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,
>
>we follow that 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.
>
>right, we don't assert and should not skolemise an existential *in a
>query* and maybe look for a syntactic distinction
>
> >>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.
>
>They *could* have a name, but we just don't care about giving them
>a name, but instead infer with terms represented as descriptions
>and we think those terms *could* stand for 'some things' (certainly
>not for 'all things')

The point is that if you have an inference process that instantiates 
a variable by some kind of matching, then that process is valid only 
if the variable being instantiated is effectively universal (ie is a 
U-variable, cf my earlier reply to Dan C.) What it gets instantiated 
TO might well be an existential, but that is a different issue.

> >(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.)
>
>Well, if we can make 'sound arguments' out of that 'smurge together'
>what would be wrong about that?

Nothing, as long as there is some guarantee that they are valid. Its 
a delicate issue, this one. I mention it only to mark it as something 
that will need more attention later, it is probably outside the WG 
scope.

>
> >>(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.
>
>also the variable [ a :Person; :hairColor :black]?

If it is in a query, yes.

Pat Hayes

---------------------------------------------------------------------
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 Tuesday, 3 July 2001 13:26:50 UTC