- From: Miles Sabin <MSabin@interx.com>
- Date: Tue, 23 Jan 2001 13:24:05 -0000
- 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 UTC