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')

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

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

--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

ps I don't know yet the true nature of anonymous nodes...

Received on Thursday, 28 June 2001 19:31:11 UTC