- From: Dan Connolly <connolly@w3.org>
- Date: Wed, 03 May 2000 17:01:27 -0500
- To: www-rdf-interest@w3.org
Dan Brickley wrote: > > Jan W writes... > > http://www.swi.psy.uva.nl/projects/SWI-Prolog/packages/sgml/online.html > > > > P.s.s. What about a standard or at least reserved naming schema for > > anonymous resources? I'm now using <Type>__<N>, with is nice > > for debugging. We also see genid<N>, but none of this is > > reserved! > > I've been thinking about this a fair bit lately. Me too. My thoughts haven't jelled, but see the "<!-- @@hmm... what subject to use for an anonymous node?" comment in http://www.w3.org/XML/2000/04rdf-parse/rdfp.xsl $Id: rdfp.xsl,v 1.4 2000/04/29 06:44:12 connolly Exp $ I was inspired when somebody (TimBL, I think) said that RDF already has existential quantification (in addition to conjunctions: multiple properties are generally considered to be 'and'ed together). So... > If I write (assume some namespace declarations with the RDF namespace > imported as 'web:', and that top level is a typedNode)... > > <Wordnet:Photo> > <image:depicts> > <Wordnet:Person> > <abc:personalMbox web:resource="mailto:danbri@w3.org"/> > </Wordnet:Person> > </image:depicts> > <ecom:buyOnline web:resource="http://example.com/shoppingcart/checkout?items=photo323423"/> > <dc:description>...etc</dc:description> > </Wordnet:Photo> > > In this serialized RDF, I'm mentioning some resource of rdf:type Exactly! "For some resource of rdf:type..." is, by another name, \exists X ... > My strawman suggestion is (a) that we adopt a convention of using URIs of > the form var:2342534647647476456456 for such situations, and (b) that such > identifiers are serving as named placeholders much like variables, and > that this analogy might be worth exploring further. These variables should be seen as skolem constants (i.e. 0-adic skolem functions). If you have any uinversally quantified variables surrounding the anonymous nodes, you have to capture those as arguments to the skolem function. "When an existential quantifier is being eliminated from a fact that contains free variables, or when the existential quantifier occurs in the scope of a universal quantifier, the quantified variable must be replaced by a term involving a Skolem function applied to the free and universally quantified variables. For example, the fact \A x (x < bigger(x)) can be obtained by eliminating the existential quantifier from \A x \E y (x < y) and replacing y by bigger(x). See the fix command and the generalization proof method. " -- LP, the Larch Prover -- Skolem constants and functions http://www.sds.lcs.mit.edu/spd/larch/LP/glossary/skolem.html (courtesy of google... http://www.google.com/search?q=skolem+existential) -- Dan Connolly, W3C http://www.w3.org/People/Connolly/
Received on Wednesday, 3 May 2000 18:01:32 UTC