From: Miles Sabin <MSabin@interx.com>

Date: Tue, 23 Jan 2001 13:24:05 -0000

Message-ID: <23CF4BF2C499D411907E00508BDC95E116FB88@ntmews_01.interx.com>

To: www-rdf-logic@w3.org

Date: Tue, 23 Jan 2001 13:24:05 -0000

Message-ID: <23CF4BF2C499D411907E00508BDC95E116FB88@ntmews_01.interx.com>

To: www-rdf-logic@w3.org

pat hayes wrote, > However, your question raises another, related, issue: > according to several members of the group which developed > RDF, the 'graph model' of a set of RDF triplets is intended > itself to be *the* model (in the sense from model theory) of > those triplets. It follows that all RDF models of any RDF > ontology (that could be stored on any web page, at any rate) > must be not only countable, but finite. Hmm ... I don't see that. It doesn't seem to follow from the (admittedly vague) sketch of the graph model in rdfms: I don't see any restrictions on the cardinality of the class of vertices, other that implied by the cardinality of the set of URIs; and I don't see any restrictions on the cardinality of the set of edges leaving a given vertex, again apart from the URI constraint. And, if Brian McBrides response to my earlier question about the cannonical URIs corresponding to rdf:_1 etc. is correct, we can easily construct an RDF/XML document which requires a countably infinite model, <rdf:Description aboutEachPrefix="http://www.w3.org/1999/02/22-rdf-syntax#_"> <s:Type>Membership Property</s:Type> </rdf:Description> makes an assertion about each of rdf:_1, rdf:_2 etc. > Now, since the finite-model restriction is not expressible in > first-order (or any complete semi-decideable) logic, this would > appear to indicate that RDF must have a semantics which > has no semidecision procedure (and hence no proof procedure.) Hmm ... well, as things stand, core RDF has no _proof_ procedure for the simple reason that it has no inference rules. Even so, if there _were_ a finite model restriction we would have something approximating to soundness, completeness, and a finitary decision procedure: every finite chunk of RDF/XML would correspond to some finite graph model; every finite graph model would correspond to some finite chunk of RDF/XML; and we could check for the presence or absence of a given assertion by simple enumeration (which is the closest we can get to a decision procedure in a language without inference rules). To be sure the finite model condition wouldn't be expressible in RDF/XML, but it would be expressible in the metalanguage used to construct the model, assuming that were strong enough. In any case, given the example I gave above of an RDF/XML doc which requires a countably infinite model, there'd better _not_ be a finite-model restriction. Cheers, Miles -- Miles Sabin InterX Internet Systems Architect 5/6 Glenthorne Mews +44 (0)20 8817 4030 London, W6 0LJ, England msabin@interx.com http://www.interx.com/Received on Tuesday, 23 January 2001 08:24:43 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Monday, 7 December 2009 10:52:38 GMT
*