You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
3946 lines
228 KiB
3946 lines
228 KiB
<?xml version="1.0" encoding="utf-8"?>
|
|
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
|
|
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
|
|
|
|
<html lang="en" xml:lang="en" xmlns="http://www.w3.org/1999/xhtml">
|
|
<head>
|
|
<meta name="generator"
|
|
content="HTML Tidy for Linux/x86 (vers 1st March 2002), see www.w3.org" />
|
|
|
|
<title>RDF Semantics</title>
|
|
<meta http-equiv="Content-Type"
|
|
content="text/html; charset=utf-8" />
|
|
<meta name="cvsid"
|
|
content="$Id: Overview.html,v 1.9 2004/02/10 15:29:28 sandro Exp $" />
|
|
<style type="text/css">
|
|
/*<![CDATA[*/
|
|
code {font-family: monospace }
|
|
a.termref:visited, a.termref:link {font-family: sans-serif;
|
|
font-style: normal;
|
|
color: black;
|
|
background-color: #ffffcc;
|
|
text-decoration: none }
|
|
.RFC2119 { font-size: small; font-weight: bolder; }
|
|
.newstuff { }
|
|
.newerstuff { }
|
|
.semantictable {background-color: #FFFFAA}
|
|
.ruletable {background-color: #DDDDFF}
|
|
.othertable {background-color: #FDFDFD}
|
|
.title {font-size: small; font-weight: bolder;}
|
|
/*]]>*/
|
|
</style>
|
|
|
|
|
|
|
|
<link rel="stylesheet" type="text/css"
|
|
href="http://www.w3.org/StyleSheets/TR/W3C-REC" />
|
|
</head>
|
|
|
|
<body>
|
|
|
|
<div class="head"> <a href="http://www.w3.org/"> <img
|
|
src="http://www.w3.org/Icons/w3c_home" alt="W3C" height="48"
|
|
width="72" /></a>
|
|
<h1 id="htitle">RDF Semantics </h1>
|
|
<h2>W3C Recommendation 10 February 2004</h2>
|
|
|
|
|
|
|
|
|
|
<dl>
|
|
<dt >This Version:</dt>
|
|
<dd><a
|
|
href="http://www.w3.org/TR/2004/REC-rdf-mt-20040210/">http://www.w3.org/TR/2004/REC-rdf-mt-20040210/</a></dd>
|
|
<dt>Latest Version:</dt>
|
|
<dd><a
|
|
href="http://www.w3.org/TR/rdf-mt/">http://www.w3.org/TR/rdf-mt/</a></dd>
|
|
<dt>Previous Version:</dt>
|
|
<dd><a href="http://www.w3.org/TR/2003/PR-rdf-mt-20031215/">http://www.w3.org/TR/2003/PR-rdf-mt-20031215/</a></dd>
|
|
<dt>Editor:</dt>
|
|
<dd><a href="http://www.ihmc.us/users/user.php?UserID=42">Patrick Hayes</a> (IHMC)<
|
|
<a href="mailto:phayes@ihmc.us">phayes@ihmc.us</a>></dd>
|
|
<dt>Series Editor</dt>
|
|
<dd><a href="http://www-uk.hpl.hp.com/people/bwm/">Brian McBride</a> (Hewlett
|
|
Packard Labs)<<a
|
|
href="mailto:bwm@hplb.hpl.hp.com">bwm@hplb.hpl.hp.com</a>></dd>
|
|
</dl>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<p>Please refer to the <a
|
|
href="http://www.w3.org/2001/sw/RDFCore/errata#rdf-mt"><strong>errata</strong></a>
|
|
for this document, which may include some normative corrections.</p>
|
|
|
|
<p>See also <a href="http://www.w3.org/2001/sw/RDFCore/translation/rdf-mt">translations</a>.</p>
|
|
|
|
<p class="copyright"><a
|
|
href="http://www.w3.org/Consortium/Legal/ipr-notice#Copyright">Copyright</a>
|
|
© 2004 <a href="http://www.w3.org/"><acronym
|
|
title="World Wide Web Consortium">W3C</acronym></a><sup>®</sup>
|
|
(<a href="http://www.csail.mit.edu/"><acronym title="Massachusetts Institute of Technology">MIT</acronym></a>,
|
|
<a href="http://www.ercim.org/"><acronym
|
|
title="European Research Consortium for Informatics and Mathematics">
|
|
ERCIM</acronym></a>, <a href="http://www.keio.ac.jp/">Keio</a>),
|
|
All Rights Reserved. W3C <a
|
|
href="http://www.w3.org/Consortium/Legal/ipr-notice#Legal_Disclaimer">
|
|
liability</a>, <a
|
|
href="http://www.w3.org/Consortium/Legal/ipr-notice#W3C_Trademarks">
|
|
trademark</a>, <a
|
|
href="http://www.w3.org/Consortium/Legal/copyright-documents">document
|
|
use</a> and <a
|
|
href="http://www.w3.org/Consortium/Legal/copyright-software">software
|
|
licensing</a> rules apply.</p>
|
|
</div>
|
|
<hr />
|
|
<h2 id="abstract">Abstract</h2>
|
|
<p>This is a specification of a precise semantics, <span >and
|
|
corresponding complete systems of inference rules,</span> for the Resource Description
|
|
Framework (RDF) and RDF Schema (RDFS).</p>
|
|
|
|
<div class="status">
|
|
|
|
<h2 class="nonum">
|
|
<a id="status" name="status">Status of this Document</a>
|
|
</h2>
|
|
|
|
|
|
<!-- Start Status-Of-This-Document Text -->
|
|
|
|
<p>This document has been reviewed by W3C Members and other interested
|
|
parties, and it has been endorsed by the Director as a <a
|
|
href="http://www.w3.org/2003/06/Process-20030618/tr.html#RecsW3C">W3C
|
|
Recommendation</a>. W3C's role in making the Recommendation is to
|
|
draw attention to the specification and to promote its widespread
|
|
deployment. This enhances the functionality and interoperability of
|
|
the Web.</p>
|
|
|
|
<p>This is one document in a <a
|
|
href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#section-Introduction">set
|
|
of six</a> (<a
|
|
href="http://www.w3.org/TR/2004/REC-rdf-primer-20040210/">Primer</a>,
|
|
<a
|
|
href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/">Concepts</a>,
|
|
<a
|
|
href="http://www.w3.org/TR/2004/REC-rdf-syntax-grammar-20040210/">Syntax</a>,
|
|
<a
|
|
href="http://www.w3.org/TR/2004/REC-rdf-mt-20040210/">Semantics</a>,
|
|
<a
|
|
href="http://www.w3.org/TR/2004/REC-rdf-schema-20040210/">Vocabulary</a>,
|
|
and <a
|
|
href="http://www.w3.org/TR/2004/REC-rdf-testcases-20040210/">Test
|
|
Cases</a>) intended to jointly replace the original Resource
|
|
Description Framework specifications, <a
|
|
href="http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/">RDF Model and Syntax (1999
|
|
Recommendation)</a> and <a
|
|
href="http://www.w3.org/TR/2000/CR-rdf-schema-20000327/">RDF Schema
|
|
(2000 Candidate Recommendation)</a>. It has been developed by the <a
|
|
href="http://www.w3.org/2001/sw/RDFCore/">RDF Core Working Group</a>
|
|
as part of the <a href="http://www.w3.org/2001/sw/">W3C Semantic Web
|
|
Activity</a> (<a href="http://www.w3.org/2001/sw/Activity">Activity
|
|
Statement</a>, <a
|
|
href="http://www.w3.org/2002/11/swv2/charters/RDFCoreWGCharter">Group
|
|
Charter</a>) for publication on 10 February 2004.
|
|
</p>
|
|
|
|
<p>Changes to this document since the <a
|
|
href="http://www.w3.org/TR/2003/PR-rdf-mt-20031215/"
|
|
shape="rect">Proposed Recommendation Working Draft</a> are detailed in
|
|
the <a href="#changes" shape="rect">change log</a>. </p>
|
|
|
|
<p> The public is invited to send comments to <a
|
|
href="mailto:www-rdf-comments@w3.org">www-rdf-comments@w3.org</a> (<a
|
|
href="http://lists.w3.org/Archives/Public/www-rdf-comments/">archive</a>)
|
|
and to participate in general discussion of related technology on <a
|
|
href="mailto:www-rdf-interest@w3.org"
|
|
shape="rect">www-rdf-interest@w3.org</a> (<a
|
|
href="http://lists.w3.org/Archives/Public/www-rdf-interest/"
|
|
shape="rect">archive</a>). </p>
|
|
|
|
<p>A list of <a href="http://www.w3.org/2001/sw/RDFCore/impls">
|
|
implementations</a> is available.</p>
|
|
|
|
<p>The W3C maintains a list of <a href="http://www.w3.org/2001/sw/RDFCore/ipr-statements"
|
|
rel="disclosure">any patent disclosures related to this work</a>.</p>
|
|
|
|
<p><em>This section describes the status of this document at the time of its
|
|
publication. Other documents may supersede this document. A list of current W3C
|
|
publications and the latest revision of this technical report can be found in
|
|
the <a href="http://www.w3.org/TR/">W3C technical reports index</a> at
|
|
http://www.w3.org/TR/.</em></p>
|
|
|
|
<!-- End Status-Of-This-Document Text -->
|
|
|
|
</div>
|
|
|
|
|
|
<h2 id="contents">Table of Contents</h2>
|
|
<p class="toc"><a href="#prelim">0. Introduction</a><a href="#intro"> </a><br />
|
|
<a href="#intro">0.1 Specifying a formal semantics: scope and limitations</a><br />
|
|
<a href="#graphsyntax">0.2 Graph Syntax</a><br />
|
|
<a href="#graphdefs">0.3 Graph Definitions</a><br />
|
|
<a href="#sinterp">1. Interpretations </a><br />
|
|
<a href="#technote">1.1 Technical Note (Informative)</a><br />
|
|
<a href="#urisandlit">1.2 URI references, Resources and Literals</a><br />
|
|
<a href="#interp">1.3 Interpretations</a><br />
|
|
<a href="#gddenot">1.4 Denotations of Ground Graphs</a><br />
|
|
<a href="#unlabel">1.5 Blank nodes as Existential variables</a><br />
|
|
<a href="#entail">2. Simple Entailment between RDF graphs </a><br />
|
|
<a href="#vocabulary_entail">2.1 Vocabulary interpretations and vocabulary entailment</a><br />
|
|
<a href="#InterpVocab">3. Interpreting the RDF vocabulary </a><br />
|
|
<a href="#RDFINTERP">3.1 RDF Interpretations</a><br />
|
|
<a href="#rdf_entail">3.2 RDF Entailment</a><br />
|
|
<a href="#ReifAndCont">3.3 Reification, Containers, Collections and rdf:value</a><br />
|
|
<a href="#Reif">3.3.1 Reification</a><br />
|
|
<a href="#Containers">3.3.2 RDF Containers</a><br />
|
|
<a href="#collections">3.3.3 RDF Collections</a><br />
|
|
<a href="#rdfValue">3.3.4 rdf:value</a><br />
|
|
<a href="#rdfs_interp">4. Interpreting the RDFS Vocabulary</a><br />
|
|
<a href="#RDFSINTERP">4.1 RDFS Interpretations</a><br />
|
|
<a href="#ExtensionalDomRang">4.2 Extensional Semantic Conditions (Informative)</a><br />
|
|
<a href="#literalnote">4.3 A Note on rdfs:Literal</a><br />
|
|
<a href="#rdfs_entailment">4.4 RDFS Entailment</a><br />
|
|
<a href="#dtype_interp">5. Interpreting Datatypes</a><br />
|
|
<a href="#DTYPEINTERP">5.1 Datatyped Interpretations</a><br />
|
|
<a href="#D_entailment">5.2 D-Entailment</a><br />
|
|
<a href="#MonSemExt">6. Monotonicity of Semantic Extensions</a><br />
|
|
<a href="#rules">7. Entailment Rules (Informative)</a><br />
|
|
<a href="#simpleRules">7.1 Simple Entailment Rules</a><br />
|
|
<a href="#RDFRules">7.2 RDF Entailment Rules</a><br />
|
|
<a href="#RDFSRules">7.3 RDFS Entailment Rules</a><br />
|
|
<a href="#RDFSExtRules">7.3.1 Extensional Entailment Rules</a><br />
|
|
<a href="#DtypeRules">7.4 Datatype Entailment Rules</a><br />
|
|
<a href="#prf">Appendix A. Proofs of lemmas (Informative)</a><br />
|
|
<a href="#gloss">Appendix B. Glossary (Informative)</a><br />
|
|
<a href="#ack">Appendix C. Acknowledgements</a><br />
|
|
<a href="#refs">References</a><br />
|
|
<a href="#change">Appendix D. Change Log (Informative)</a></p>
|
|
<h2><a name="prelim" id="prelim">0. Introduction</a> </h2>
|
|
|
|
<h3><a name="intro" id="intro">0.1 Specifying a formal semantics:
|
|
scope and limitations</a></h3>
|
|
|
|
|
|
<p>RDF is an assertional language intended to be used to express <a
|
|
href="#glossProposition" class="termref">propositions</a> using precise formal
|
|
vocabularies, particularly those specified using RDFS [<cite><a href="#ref-rdf-vocabulary">RDF-VOCABULARY</a></cite>],
|
|
for access and use over the World Wide Web, and is intended to provide a basic
|
|
foundation for more advanced assertional languages with a similar purpose. The
|
|
overall design goals emphasise generality and precision in expressing propositions
|
|
about any topic, rather than conformity to any particular processing model:
|
|
see the <a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/">RDF Concepts document</a> [<cite><a
|
|
href="#ref-rdf-concepts">RDF-CONCEPTS</a></cite>] for more discussion. </p>
|
|
<p>Exactly what is considered to be the 'meaning' of an <a
|
|
href="#glossAssertion" class="termref">assertion</a> in RDF or RDFS in some
|
|
broad sense may depend on many factors, including social conventions, comments
|
|
in natural language or links to other content-bearing documents. Much of this
|
|
meaning will be inaccessible to machine processing and is mentioned here only
|
|
to emphasize that the <a href="#glossFormal"
|
|
class="termref">formal</a> <a href="#glossSemantic"
|
|
class="termref">semantics</a> described in this document is not intended to
|
|
provide a full analysis of 'meaning' in this broad sense; that would be a large
|
|
research topic. The semantics given here restricts itself to a <a href="#glossFormal"
|
|
class="termref">formal</a> notion of meaning which could be characterized
|
|
as the part that is common to all other accounts of meaning, and can be captured
|
|
in mechanical <a
|
|
href="#glossInference" class="termref">inference</a> rules. </p>
|
|
<p>This document uses a basic technique called <a href="#glossModeltheory"
|
|
class="termref">model theory</a> for specifying the semantics of a formal
|
|
language. Readers unfamiliar with model theory may find the <a href="#gloss">glossary</a>
|
|
in appendix B helpful; throughout the text, uses of terms in a technical sense
|
|
are linked to their glossary definitions. Model theory assumes that the language
|
|
refers to a '<a href="#glossWorld"
|
|
class="termref">world</a>', and describes the minimal conditions that a world
|
|
must satisfy in order to assign an appropriate meaning for every expression
|
|
in the language. A particular <a
|
|
class="termref" href="#glossWorld" >world</a> is called an <i><a
|
|
href="#glossInterpretation" class="termref">interpretation</a>,</i> so that
|
|
<a href="#glossModeltheory" class="termref">model theory</a> might be better
|
|
called 'interpretation theory'. The idea is to provide an abstract, mathematical
|
|
account of the properties that any such interpretation must have, making as
|
|
few assumptions as possible about its actual nature or intrinsic structure,
|
|
thereby retaining as much generality as possible. The chief utility of a formal
|
|
semantic theory is not to provide any deep analysis of the nature of the things
|
|
being described by the language or to suggest any particular processing model,
|
|
but rather to provide a technical way to determine when inference processes
|
|
are <a href="#glossValid"
|
|
class="termref">valid</a>, i.e. when they preserve truth. This provides the
|
|
maximal freedom for implementations while preserving a globally coherent notion
|
|
of meaning.</p>
|
|
<p>Model theory tries to be <a href="#glossMetaphysical"
|
|
class="termref">metaphysically</a> and <a href="#glossOntological"
|
|
class="termref">ontologically</a> neutral. It is typically couched in the
|
|
language of set theory simply because that is the normal language of mathematics
|
|
- for example, this semantics assumes that names denote things in a <i>set</i>
|
|
IR called the '<a
|
|
href="#glossUniverse" class="termref">universe</a>' - but the use of set-theoretic
|
|
language here is not supposed to imply that the things in the universe are set-theoretic
|
|
in nature. Model theory is usually most relevant to implementation via the notion
|
|
of <a
|
|
href="#glossEntail" class="termref">entailment</a>, described later, which
|
|
makes it possible to define <a href="#glossValid"
|
|
class="termref">valid</a> <a href="#glossInference"
|
|
class="termref">inference</a> rules.</p>
|
|
<p>An alternative way to specify a semantics is to give a translation from RDF
|
|
into a formal logic with a <a href="#glossModeltheory" class="termref">model
|
|
theory</a> already attached, as it were. This 'axiomatic semantics' approach
|
|
has been suggested and used previously with various alternative versions of
|
|
the target logical language [<cite><a
|
|
href="#ref-ConKla">Conen&Klapsing</a></cite>] [<cite><a
|
|
href="#ref-MarSaa">Marchiori&Saarela</a></cite>] [<cite><a
|
|
href="#ref-daml-axiomat">McGuinness&al</a></cite>]. Such a translation
|
|
for RDF and RDFS is also given in the L<sub>base</sub> specification [<cite><a href="#ref-Lbase">LBASE</a></cite>].
|
|
The axiomatic semantics style has some advantages for machine processing and
|
|
may be more readable, but in the event that any axiomatic semantics fails to
|
|
conform to the model-theoretic semantics described in this document, the model
|
|
theory should be taken as normative. </p>
|
|
<p>There are several aspects of meaning in RDF which are ignored by this semantics;
|
|
in particular, it treats URI references as simple names, ignoring aspects of
|
|
meaning encoded in particular URI forms [<cite><a href="#ref-2369">RFC 2396</a></cite>]
|
|
and does not provide any analysis of time-varying data or of changes to URI
|
|
references. It does not provide any analysis of <a href="#glossIndexical"
|
|
class="termref">indexical</a> uses of URI references, for example to mean
|
|
'this document'. Some parts of the RDF and RDFS vocabularies are not assigned
|
|
any formal meaning, and in some cases, notably the reification and container
|
|
vocabularies, it assigns less meaning than one might expect. These cases are
|
|
noted in the text and the limitations discussed in more detail. RDF is an assertional
|
|
<a href="#glossLogic"
|
|
class="termref">logic</a>, in which each triple expresses a simple <a href="#glossProposition" class="termref">proposition</a>.
|
|
This imposes a fairly strict <a href="#glossMonotonic"
|
|
class="termref">monotonic</a> discipline on the language, so that it cannot
|
|
express closed-world assumptions, local default preferences, and several other
|
|
commonly used <a
|
|
href="#glossNonmonotonic" class="termref">non-monotonic</a> constructs.</p>
|
|
|
|
|
|
<p><a id="DefSemanticExtension" name="DefSemanticExtension"></a> Particular uses
|
|
of RDF, including as a basis for more expressive languages such as DAML+OIL
|
|
[<cite><a href="#ref-daml">DAML</a></cite>] and OWL [<cite><a
|
|
href="#ref-owl">OWL</a></cite>], may impose further semantic conditions in
|
|
addition to those described here, and such extra semantic conditions can also
|
|
be imposed on the meanings of terms in particular RDF vocabularies.<a name="RDFSemanticExtension" id="RDFSemanticExtension"></a>
|
|
Extensions or dialects of RDF which are obtained by imposing such extra semantic
|
|
conditions may be referred to as <i>semantic extensions</i> of RDF. Semantic
|
|
extensions of RDF are constrained in this recommendation using the keywords
|
|
<strong title="MUST in RFC 2119 context" class="RFC2119">MUST</strong> , <strong title="MUST NOT in RFC 2119 context" class="RFC2119">MUST
|
|
NOT</strong>, <strong title="SHOULD in RFC 2119 context" class="RFC2119">SHOULD</strong>
|
|
and <strong title="MAY in RFC 2119 context" class="RFC2119">MAY</strong> of
|
|
[<cite><a href="#ref-2119">RFC 2119</a></cite>]. Semantic extensions of RDF
|
|
<strong title="MUST in RFC 2119 context" class="RFC2119">MUST</strong> conform
|
|
to the semantic conditions for simple interpretations described in <a href="#interp">sections
|
|
1.3</a> <a href="#gddenot"> and 1.4</a> <a href="#unlabel">and 1.5</a> and those
|
|
for RDF interpretations described in <a href="#RDFINTERP">section 3.1</a> of
|
|
this document. Any name for entailment in a semantic extension <strong title="SHOULD in RFC 2119 context" class="RFC2119">SHOULD</strong>
|
|
be indicated by the use of a <a href="#vocabulary_entail" class="termref">vocabulary
|
|
entailment</a> term. The semantic conditions imposed on an RDF semantic extension
|
|
<strong title="MUST in RFC 2119 context" class="RFC2119">MUST</strong> define
|
|
a notion of <a href="#vocabulary_entail" class="termref">vocabulary entailment</a>
|
|
which is <a href="#glossValid"
|
|
class="termref">valid</a> according to the model-theoretic semantics described
|
|
in the normative parts of this document; except that if the semantic extension
|
|
is defined on some syntactically restricted subset of <a href="#defgraph" class="termref">RDF
|
|
graphs</a>, then the semantic conditions need only apply to this subset. Specifications
|
|
of such syntactically restricted semantic extensions <strong title="MUST in RFC 2119 context" class="RFC2119">MUST</strong>
|
|
include a specification of their syntactic conditions which are sufficient to
|
|
enable software to distinguish unambiguously those <a href="#defgraph" class="termref">RDF
|
|
graphs</a> to which the extended semantic conditions apply. Applications based
|
|
on such syntactically restricted semantic extensions <strong title="MAY in RFC 2119 context" class="RFC2119">MAY</strong>
|
|
treat <a href="#defgraph" class="termref">RDF graphs</a> which do not conform
|
|
to the required syntactic restrictions as syntax errors.</p>
|
|
<p>An example of a semantic extension of RDF is RDF Schema [<cite><a href="#ref-rdf-vocabulary">RDF-VOCABULARY</a></cite>],
|
|
abbreviated as RDFS, the semantics of which are defined in later parts of this
|
|
document. RDF Schema imposes no extra syntactic restrictions.</p>
|
|
|
|
<h3><a name="graphsyntax" id="graphsyntax">0.2 Graph
|
|
Syntax</a></h3>
|
|
|
|
|
|
<p>Any semantic theory must be attached to a syntax. This semantics is defined
|
|
as a mapping on the <a
|
|
href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#section-Graph-syntax">abstract
|
|
syntax</a> of RDF described in the RDF concepts and abstract syntax document
|
|
[<cite><a href="#ref-rdf-concepts">RDF-CONCEPTS</a></cite>]. This document uses
|
|
the following terminology defined there: <a
|
|
href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#section-Graph-URIref"><em>URI
|
|
reference</em></a>, <a
|
|
href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#section-Graph-Literal"><em>
|
|
literal</em></a>, <a
|
|
href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#section-Graph-Literal"><em>plain
|
|
literal</em></a>, <a
|
|
href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#section-Graph-Literal"><em>typed
|
|
literal</em></a>, <a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#dfn-rdf-XMLLiteral"><em>XML
|
|
literal</em></a>, <a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#XMLLiteral-value-space">
|
|
<em>XML value,</em></a> <a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#section-rdf-graph"><em>node</em></a>,
|
|
<a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#section-blank-nodes"><em>blank
|
|
node</em></a>, <a
|
|
href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#xtocid103646"><em>triple</em></a>
|
|
<span >and <a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#section-Graph-syntax"><em>RDF
|
|
graph</em></a></span>. Throughout this document we use the term 'character string'
|
|
or 'string' to refer to a sequence of Unicode characters, and 'language tag'
|
|
in the sense of RFC 3066, c.f. <a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#section-Graph-Literal">section
|
|
6.5</a> in [<cite><a href="#ref-rdf-concepts">RDF-CONCEPTS</a></cite>]. Note
|
|
that strings in an RDF graph <strong title="SHOULD in RFC 2119 context" class="RFC2119">SHOULD</strong>
|
|
be in Normal Form C. </p>
|
|
<p >This document uses the <a
|
|
href="http://www.w3.org/TR/rdf-testcases/#ntriples">N-Triples</a> syntax described
|
|
in the RDF test cases document [<cite><a href="#ref-rdf-tests">RDF-TESTS</a></cite>]
|
|
to describe <a href="#defgraph" class="termref">RDF graphs</a>. This notation
|
|
uses a <a
|
|
href="http://www.w3.org/TR/rdf-testcases/#bNode">node identifier</a> (nodeID)
|
|
convention to indicate blank nodes in the triples of a graph. <a id="nodeIDnote"
|
|
name="nodeIDnote"></a> While node identifiers such as '<code>_:xxx</code>'
|
|
serve to identify blank nodes in the surface syntax, these expressions are not
|
|
considered to be the label of the graph node they identify; they are not names,
|
|
and do not occur in the actual graph. In particular, the <a href="#defgraph" class="termref">RDF
|
|
graphs</a> described by two <a
|
|
href="http://www.w3.org/TR/rdf-testcases/#ntriples">N-Triples documents</a>
|
|
which differ only by re-naming their node identifiers will be understood to
|
|
be <a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#section-graph-equality">equivalent</a>
|
|
.<span > <a name="lcc7R1" id="lcc7R1"></a>This re-naming convention should be
|
|
understood as applying only to whole documents, since re-naming the node identifiers
|
|
in part of a document may result in a document describing a different <a href="#defgraph" class="termref">RDF
|
|
graph</a>. </span></p>
|
|
<p>The N-Triples syntax requires that URI references be given in full,
|
|
enclosed in angle brackets. In the interests of brevity, the
|
|
imaginary URI scheme 'ex:' is used to provide illustrative examples. To
|
|
obtain a more realistic view of the normal appearance of the
|
|
N-Triples syntax, the reader should imagine this replaced with
|
|
something like '<code>http://www.example.org/rdf/mt/artificial-example/</code>'.
|
|
The QName prefixes
|
|
<code>rdf:</code>, <code>rdfs:</code> and <code>xsd:</code> are defined
|
|
as follows:</p>
|
|
|
|
<p>Prefix <code>rdf:</code> namespace URI:
|
|
<code>http://www.w3.org/1999/02/22-rdf-syntax-ns#</code></p>
|
|
|
|
<p>Prefix <code>rdfs:</code> namespace URI:
|
|
<code>http://www.w3.org/2000/01/rdf-schema#</code></p>
|
|
|
|
<p>Prefix <code>xsd:</code> namespace URI:
|
|
<code>http://www.w3.org/2001/XMLSchema#</code></p>
|
|
|
|
<p>Since QName syntax is not legal N-Triples syntax, and in the
|
|
interests of brevity and readability, examples use the convention
|
|
whereby a QName is used without surrounding angle brackets to
|
|
indicate the corresponding URI reference enclosed in angle brackets, e.g.
|
|
the triple</p>
|
|
|
|
<p><code><ex:a> rdf:type rdfs:Class .</code></p>
|
|
|
|
<p>should be read as an abbreviation for the N-Triples syntax</p>
|
|
|
|
<p><code><ex:a>
|
|
<http://www.w3.org/1999/02/22-rdf-syntax-ns#type>
|
|
<http://www.w3.org/2000/01/rdf-schema#Class> .</code></p>
|
|
<p >In stating general semantic conditions, single characters
|
|
or character sequences without a colon indicate an arbitrary name, blank node,
|
|
character string and so on. The exact meaning will be specified in context.</p>
|
|
<h3><a name="graphdefs" id="graphdefs">0.3 Graph
|
|
Definitions</a></h3>
|
|
|
|
|
|
<p><a name="defgraph" id="defgraph">An <span > <a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#dfn-rdf-graph"><em>RDF
|
|
graph</em></a></span>, or simply a <em>graph</em>, is a set of RDF triples.</a></p>
|
|
<p><a name="defsubg" id="defsubg">A <i>subgraph</i> of an RDF graph is a subset
|
|
of the triples in the graph.</a> A triple is identified with the singleton set
|
|
containing it, so that each triple in a graph is considered to be a subgraph.
|
|
A <em>proper</em> subgraph is a proper subset of the triples in the graph. </p>
|
|
|
|
|
|
<p><a name="defgd" id="defgd">A <em>ground</em> RDF graph is one with no blank
|
|
nodes.</a></p>
|
|
|
|
|
|
<p><a name="defname" id="defname">A <em>name</em> is a URI reference or a literal.</a>
|
|
These are the expressions that need to be assigned a meaning by an <a href="#glossInterpretation"
|
|
class="termref">interpretation</a>. Note that a typed literal <span >comprises</span>
|
|
two <a href="#defname" class="termref">name</a>s: itself and its internal type
|
|
URI reference. </p>
|
|
<p><a name="defvocab" id="defvocab"></a> A set of <a href="#defname" class="termref">name</a>s
|
|
is referred to as a <i>vocabulary</i>. The vocabulary <em>of</em> a graph is
|
|
the set of names which occur as the subject, predicate or object of any triple
|
|
in the graph. Note that URI references which occur only inside typed literals
|
|
are not required to be in the vocabulary of the graph.</p>
|
|
<p><a name="definst" id="definst"> Suppose that M is a mapping from a set of blank
|
|
nodes to some set of literals, blank nodes and URI references; then any graph obtained
|
|
from a graph G by replacing some or all of the blank nodes N in G by M(N) is
|
|
an <em>instance</em> of G.</a> Note that any graph is an instance of itself,
|
|
<span >an instance of an instance of G is an instance of G,</span>
|
|
and if H is an instance of G then every triple in H is an instance of some triple
|
|
in G.</p>
|
|
<p><a name="definstvoc" id="definstvoc">An instance <i>with respect to a vocabulary</i>
|
|
V </a>is an <a href="#definst" class="termref">instance</a> in which all the
|
|
<a href="#defname" class="termref">name</a>s in the instance that were substituted
|
|
for blank nodes in the original are <a href="#defname" class="termref">name</a>s
|
|
from V.</p>
|
|
<p><a name="defpropinst" id="defpropinst">A <i>proper</i> instance</a> of a graph
|
|
is an instance in which a blank node has been replaced by a name, or two blank
|
|
nodes in the graph have been mapped into the same node in the instance. </p>
|
|
<p >Any instance of a graph in which a blank node is mapped to a new blank node
|
|
not in the original graph is an instance of the original and also has it as
|
|
an instance, and this process can be iterated so that any 1:1 mapping between
|
|
blank nodes defines an instance of a graph which has the original graph as an
|
|
instance. Two such graphs, each an instance of the other but neither a proper
|
|
instance, which differ only in the identity of their blank nodes, are considered
|
|
to be <a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#section-graph-equality">equivalent</a>.
|
|
We will treat such equivalent graphs as identical; this allows us to ignore
|
|
some issues which arise from 're-naming' nodeIDs, and is in conformance with
|
|
the <a href="#nodeIDnote" class="termref">convention</a> that blank nodes have
|
|
no label. Equivalent graphs are mutual instances with an invertible instance
|
|
mapping.</p>
|
|
<p ><span ><a id="deflean"
|
|
name="deflean">An RDF graph is <em>lean</em> if it has no instance which is
|
|
a proper subgraph of the graph.</a> Non-lean graphs have internal redundancy
|
|
and express the same content as their lean subgraphs. For example, the graph</span></p>
|
|
<p ><code><ex:a> <ex:p> _:x .<br />
|
|
_:y <ex:p> _:x .</code></p>
|
|
<p >is not <a
|
|
href="#deflean" class="termref">lean</a>, but</p>
|
|
<p ><code><ex:a> <ex:p> _:x .<br />
|
|
_:x <ex:p> _:x .</code></p>
|
|
<p >is <a
|
|
href="#deflean" class="termref">lean</a>. </p>
|
|
<p> <a name="defmerge" id="defmerge"></a> A
|
|
<em>merge</em> of a set of RDF graphs is defined as follows. If the graphs in
|
|
the set have no blank nodes in common, then the union of the graphs is a merge;
|
|
if they do share blank nodes, then it is the union of a set of graphs that is
|
|
obtained by replacing the graphs in the set by equivalent graphs that share
|
|
no blank nodes. This is often described by saying that the blank nodes have
|
|
been 'standardized apart'. It
|
|
is easy to see that any two merges are equivalent, so we will refer to <em>the</em>
|
|
merge, following the convention on equivalent graphs.
|
|
Using the convention on equivalent graphs and identity, any graph in the original
|
|
set is considered to be a subgraph of the merge. </p>
|
|
<p>One does not, in general, obtain the merge of a set of graphs by concatenating
|
|
their corresponding <a
|
|
href="http://www.w3.org/TR/rdf-testcases/#ntriples">N-Triples</a> documents
|
|
and constructing the graph described by the merged document. If some of the
|
|
documents use the same node identifiers, the merged document will describe a
|
|
graph in which some of the blank nodes have been 'accidentally' identified.
|
|
To merge <a
|
|
href="http://www.w3.org/TR/rdf-testcases/#ntriples">N-Triples</a> documents
|
|
it is necessary to check if the same nodeID is used in two or more documents,
|
|
and to replace it with a distinct nodeID in each of them, before merging the
|
|
documents. Similar cautions apply to merging graphs described by RDF/XML documents
|
|
which contain nodeIDs, see <a
|
|
href="http://www.w3.org/TR/2002/WD-rdf-syntax-grammar-20021108/">RDF/XML
|
|
Syntax Specification (Revised)</a> [<cite><a href="#ref-rdf-syntax">RDF-SYNTAX</a></cite>].</p>
|
|
<h2><a id="sinterp" name="sinterp"> 1. Interpretations</a> </h2>
|
|
|
|
|
|
<h3><a name="technote" id="technote">1.1 Technical note (Informative)</a></h3>
|
|
<p>RDF does not impose any logical restrictions on the domains and ranges of properties;
|
|
in particular, a property may be applied to itself. When <a href="#glossClass" class="termref">classes</a>
|
|
are introduced in RDFS, they may contain themselves. Such 'membership loops'
|
|
might seem to violate the axiom of foundation, one of the axioms of standard
|
|
(Zermelo-Fraenkel) set theory, which forbids infinitely descending chains of
|
|
membership. However, the semantic model given here distinguishes properties
|
|
and classes considered as objects from their <a id="defexten"
|
|
name="defexten"><i>extensions</i> - the sets of object-value pairs which satisfy
|
|
the property, or things that are 'in' the class</a> - thereby allowing the extension
|
|
of a property or class to contain the property or class itself without violating
|
|
the axiom of foundation. In particular, this use of a class extension mapping
|
|
allows classes to contain themselves. For example, it is quite OK for (the extension
|
|
of) a 'universal' class to contain the class itself as a member, a convention
|
|
that is often adopted at the top of a classification hierarchy. (If an extension
|
|
contained itself then the axiom would be violated, but that case never arises.)
|
|
The technique is described more fully in [<cite><a
|
|
href="#ref-HayMen">Hayes&Menzel</a></cite>].</p>
|
|
<p>In this respect, RDFS differs from many conventional ontology frameworks such
|
|
as UML which assume a more structured hierarchy of individuals, sets of individuals,
|
|
etc., or which draw a sharp distinction between data and meta-data. However,
|
|
while RDFS does not assume the existence of such structure, it does not prohibit
|
|
it. RDF allows membership loops, but it does not mandate their use for all parts
|
|
of a user vocabulary. If this aspect of RDFS is found worrying, then it is possible
|
|
to restrict oneself to a subset of RDF graphs which do not contain any such
|
|
'loops' of class membership or property application while retaining much of
|
|
the expressive power of RDFS for many practical purposes, <span >and semantic
|
|
extensions may impose syntactic conditions which forbid such looped constructions.
|
|
</span></p>
|
|
<p>The use of the explicit extension mapping also makes it possible for two properties
|
|
to have exactly the same values, or two classes to contain the same instances,
|
|
and still be distinct entities. This means that RDFS classes can be considered
|
|
to be rather more than simple sets; they can be thought of as 'classifications'
|
|
or 'concepts' which have a robust notion of identity which goes beyond a simple
|
|
<a href="#glossExtensional"
|
|
class="termref">extensional</a> correspondence. This property of the <a href="#glossModeltheory" class="termref">model
|
|
theory</a> has significant consequences in more expressive languages built on
|
|
top of RDF, such as OWL [<cite><a
|
|
href="#ref-owl">OWL</a></cite>], which are capable of expressing identity
|
|
between properties and classes directly. This '<a href="#glossIntensional" class="termref">intensional</a>'
|
|
nature of classes and properties is sometimes claimed to be a useful property
|
|
of a descriptive language, but a full discussion of this issue is beyond the
|
|
scope of this document.</p>
|
|
|
|
<p>Notice that the question of whether or not a class contains itself as a member is quite different
|
|
from the question of whether or not it is a subclass of itself. All classes are subclasses of themselves.</p>
|
|
|
|
<p>Readers who are familiar with conventional logical semantics may find it useful
|
|
to think of RDF as a version of existential binary relational logic in which
|
|
relations are first-class entities in the universe of quantification. Such a
|
|
logic can be obtained by encoding the relational atom R(a,b) into a conventional
|
|
logical syntax, using a notional three-place relation Triple(a,R,b); the basic
|
|
semantics described here can be reconstructed from this intuition by defining
|
|
the extension of y as the set {<x,z> : Triple(x,y,z)} and noting that
|
|
this would be precisely the denotation of R in the conventional Tarskian model
|
|
theory of the original form R(a,b) of the relational atom. This construction
|
|
can also be traced in the semantics of the L<sub>base</sub> axiomatic description
|
|
[<cite><a href="#ref-Lbase">LBASE</a></cite>].</p>
|
|
|
|
|
|
|
|
<h3><a name="urisandlit" id="urisandlit">1.2 URI references, Resources and
|
|
Literals</a>.</h3>
|
|
|
|
<p>This document does not take any position on the way that URI references
|
|
may be composed from other expressions, e.g. from relative URIs or QNames;
|
|
the semantics simply assumes that such lexical issues have been
|
|
resolved in some way that is globally coherent, so that a single
|
|
URI reference can be taken to have the same meaning wherever it occurs.
|
|
Similarly, the semantics has no special provision for tracking
|
|
temporal changes. It assumes, implicitly, that URI references have the
|
|
same meaning <em>whenever</em> they occur. To provide an adequate
|
|
semantics which would be sensitive to temporal changes is a
|
|
research problem which is beyond the scope of this document.</p>
|
|
|
|
<p>The semantics does not assume any particular relationship
|
|
between the denotation of a URI reference and a document or Web
|
|
resource which can be retrieved by using that URI reference in an HTTP
|
|
transfer protocol, or any entity which is considered to be the
|
|
source of such documents. Such a requirement could be added as a
|
|
semantic extension, but the formal semantics described here makes
|
|
no assumptions about any connection between the denotations of
|
|
URI references and the uses of those URI references in other protocols.</p>
|
|
<p >The semantics treats all RDF <a href="#defname" class="termref">name</a>s
|
|
as expressions which denote. The things denoted are called 'resources', following
|
|
[<cite><a
|
|
href="#ref-2369">RFC 2396</a></cite>], but no assumptions are made here about
|
|
the nature of <a href="#glossResource"
|
|
class="termref">resources</a>; 'resource' is treated here as synonymous with
|
|
'entity',<span > i.e. as a generic term for anything in the
|
|
universe of discourse. </span> </p>
|
|
<p >The different syntactic forms of <a href="#defname" class="termref">name</a>s
|
|
are treated in particular ways. URI references are treated simply as logical
|
|
constants. Plain literals are considered to denote themselves, so have a fixed
|
|
meaning. The denotation of a typed literal is the value mapped from its enclosed
|
|
character string by the datatype associated with its enclosed type. RDF assigns
|
|
a particular meaning to literals typed with <code>rdf:XMLLiteral</code>, <a href="#defXMLdatatype" class="termref">described
|
|
</a> in <a href="#InterpVocab" class="termref">section 3</a>. </p>
|
|
<h3><a name="interp" id="interp">1.3 Interpretations</a></h3>
|
|
|
|
|
|
<p>The basic intuition of model-theoretic semantics is that asserting a sentence
|
|
makes a claim about the <a href="#glossWorld"
|
|
class="termref">world</a>: it is another way of saying that the world is,
|
|
in fact, so arranged as to be an <a
|
|
href="#glossInterpretation" class="termref">interpretation</a> which makes
|
|
the sentence true. In other words, an assertion amounts to stating a <i>constraint</i>
|
|
on the <i>possible</i> ways the world might be. Notice that there is no presumption
|
|
here that any assertion contains enough information to specify a single unique
|
|
interpretation. It is usually impossible to assert enough in any language to
|
|
completely constrain the interpretations to a single possible world, so there
|
|
is no such thing as 'the' unique interpretation of an RDF graph.
|
|
In general, the larger an RDF graph is - the more it says about the world -
|
|
then the smaller the set of interpretations that an <a href="#glossAssertion"
|
|
class="termref">assertion</a> of the graph allows to be true - the fewer the
|
|
ways the world could be, while making the asserted graph true of it.</p>
|
|
|
|
<p>The following definition of an interpretation is couched in
|
|
mathematical language, but what it amounts to intuitively is that
|
|
an interpretation provides just enough information about a possible
|
|
way the world might be - a 'possible world' - in order to fix the
|
|
truth-value (true or false) of any ground RDF triple. It does this
|
|
by specifying for each URI reference, what it is supposed to be a name of;
|
|
and also, if it is used to indicate a property, what values that
|
|
property has for each thing in the <a href="#glossUniverse"
|
|
class="termref">universe</a>; and if it is used to indicate a
|
|
<a href="#defDatatype" class="termref">datatype</a>, that the <a href="#defDatatype" class="termref">datatype</a> defines a mapping between
|
|
lexical forms and datatype values. This is just enough information
|
|
to fix the truth-value of any <a href="#defgd"
|
|
class="termref">ground</a> triple, and hence any ground RDF
|
|
graph. (Non-ground
|
|
graphs are considered in the following section.) Note that if any of
|
|
this information were omitted, it would be possible for some <a
|
|
href="#glossWellformed" class="termref">well-formed</a> triple to
|
|
be left without a determinate value; and also that any other
|
|
information - such as the exact nature of the things in the <a
|
|
href="#glossUniverse" class="termref">universe</a> - would,
|
|
regardless of its intrinsic interest, be irrelevant to the actual
|
|
truth-values of any triple.</p>
|
|
|
|
|
|
<p>All interpretations will be relative to a set of <a href="#defname" class="termref">name</a>s,
|
|
called the vocabulary of the interpretation; so that one should speak, strictly,
|
|
of an interpretation of an RDF vocabulary, rather than of RDF itself. Some interpretations
|
|
may assign special meanings to the symbols in a particular vocabulary. Interpretations
|
|
which share the special meaning of a particular vocabulary will be named for
|
|
that vocabulary, e.g. '<a href="#rdfinterpdef" class="termref">rdf-interpretation</a>s',
|
|
'<a href="#rdfsinterpdef" class="termref">rdfs-interpretation</a>s', etc. An
|
|
interpretation with no particular extra conditions on a vocabulary (including
|
|
the RDF vocabulary itself) will be called a <i>simple</i> interpretation, or
|
|
simply an interpretation. </p>
|
|
|
|
|
|
<p>RDF uses several forms of literal. The chief semantic characteristic of literals
|
|
is that their meaning is largely determined by the form of the string they contain.
|
|
Plain literals, without an embedded type URI reference, are always interpreted
|
|
as referring to themselves: either a character string or a pair consisting of
|
|
a character string and a <a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#section-Graph-Literal" class="termref">language
|
|
tag</a>; in either case, the character string is referred to as the "literal
|
|
character string". In the case of typed literals, however, the full specification
|
|
of the meaning depends on being able to access <a href="#defDatatype" class="termref">datatype</a>
|
|
information which is external to RDF itself. A full discussion of the meaning
|
|
of typed literals is described in <a href="#dtype_interp">section 5</a> , where
|
|
a special notion of datatype interpretation is introduced. Each interpretation
|
|
defines a mapping IL from typed literals to their interpretations. Stronger
|
|
conditions on IL will be defined as the notion of 'interpretation' is extended
|
|
in later sections. </p>
|
|
<p>Throughout this document, precise semantic conditions will be set out in tables
|
|
which state semantic conditions, tables containing true assertions and <a href="#glossValid"
|
|
class="termref">valid</a> inference rules, and tables listing syntax, which
|
|
are distinguished by background color. These tables, taken together, amount
|
|
to a formal summary of the entire semantics. Note that the semantics of RDF
|
|
does not depend on that of RDFS. The full semantics of RDF is defined in sections
|
|
<a href="#sinterp">1</a> and <a href="#InterpVocab">3</a> ; the full semantics
|
|
of RDFS in sections <a href="#sinterp">1</a>, <a href="#InterpVocab">3</a> and
|
|
<a href="#rdfs_interp">4</a>.</p>
|
|
<div class="title">Definition of a simple interpretation.</div>
|
|
<table border="1" summary="definition of a simple interpretation">
|
|
<tr>
|
|
<td class="semantictable"><p>A <i>simple</i> <em>interpretation</em> I of a vocabulary V is
|
|
defined by:</p>
|
|
<p>1. A non-empty set IR of resources, called the domain or universe
|
|
of I.</p>
|
|
<p>2. <span >A set IP, called the set of properties of I.</span></p>
|
|
<p>3. A mapping IEXT from IP into the powerset of IR x IR i.e. the
|
|
set of sets of pairs <x,y> with x and y in IR .</p>
|
|
<p>4. A mapping IS from URI references in V into (IR union IP)</p>
|
|
<p>5. A mapping IL from typed literals in V into IR.</p>
|
|
<p >6. A distinguished subset LV of IR, called the set of literal values,
|
|
which contains all the plain literals in V</p></td>
|
|
</tr>
|
|
</table>
|
|
<p>IEXT(x), called
|
|
the <a href="#defexten" class="termref"><i>extension</i></a> of x, is a
|
|
set of pairs which identify the arguments for which the property is true,
|
|
that is, a binary
|
|
relational extension.
|
|
This trick of distinguishing a relation as an object from its
|
|
relational extension allows a property to occur in its own
|
|
extension, as <a href="#technote" class="termref">noted earlier</a>.</p>
|
|
<p>The assumption that LV is a subset of IR amounts to saying that literal values
|
|
are thought of as real entities that 'exist'. This amounts to saying that literal
|
|
values are resources. However, this does not imply that literals should be identified
|
|
with URI references. Note that LV may contain other items in addition to plain
|
|
literals. There is a technical reason why the range of IL is IR rather than
|
|
restricted to LV. When interpretations take account of <a href="#defDatatype" class="termref">datatype</a>
|
|
information, it is syntactically possible for a typed literal to be internally
|
|
inconsistent, and such ill-typed literals are required to denote a <em>non</em>-literal
|
|
value, as <a href="#illformedliteral" class="termref">explained</a> in <a href="#dtype_interp" class="termref">section
|
|
5</a>.</p>
|
|
<p>The next sections define how an interpretation of a vocabulary determines the
|
|
truth-values of any RDF graph, by a recursive definition of the denotation -
|
|
the semantic "value" - of any RDF expression in terms of those of its immediate
|
|
subexpressions. These apply to all subsequent semantic extensions. RDF has two
|
|
kinds of denotation: <a href="#defname" class="termref">name</a>s denote things
|
|
in the universe, and sets of triples denote truth-values. </p>
|
|
<h3><a name="gddenot" id="gddenot">1.4 Denotations of Ground
|
|
Graphs</a></h3>
|
|
|
|
|
|
<p>The denotation of a ground RDF graph in I is given recursively by the following
|
|
rules, which extend the interpretation mapping I from <a href="#defname" class="termref">name</a>s
|
|
to ground graphs. These rules (and extensions of them given later) work by defining
|
|
the denotation of any piece of RDF syntax E in terms of the denotations of the
|
|
immediate syntactic constituents of E, hence allowing the denotation of any
|
|
piece of RDF to be determined by a kind of syntactic recursion.</p>
|
|
<p>In this table, and throughout this document, the equality sign = indicates
|
|
identity and angle brackets <x,y> are used to indicate an ordered pair
|
|
of x and y. RDF graph syntax is indicated using the notational conventions of
|
|
the <a
|
|
href="http://www.w3.org/TR/rdf-testcases/#ntriples">N-Triples</a> syntax described
|
|
in the RDF test cases document [<cite><a href="#ref-rdf-tests">RDF-TESTS</a></cite>]:
|
|
literal strings are encloded within double quote marks, language tags indicated
|
|
by the use of the <code>@</code> sign, and triples terminate with a 'code dot'
|
|
<code>.</code> . </p>
|
|
|
|
<div class="title">Semantic conditions for ground graphs.</div>
|
|
<table cellpadding="5" border="2" summary="semantic conditions for RDF graphs">
|
|
<tbody>
|
|
<tr>
|
|
|
|
<td class="semantictable">if E is a plain literal "aaa" in V
|
|
then I(E) = aaa</td>
|
|
</tr>
|
|
<tr>
|
|
|
|
<td class="semantictable">if E is a plain literal "aaa"<code>@</code>ttt
|
|
in V then I(E) = <aaa, ttt></td>
|
|
</tr>
|
|
|
|
<tr>
|
|
|
|
|
|
<td class="semantictable">if E is a typed literal in V then I(E) = IL(E)</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
|
|
<td class="semantictable">if E is a URI reference in V then I(E) = IS(E)</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
|
|
<td class="semantictable"><p>if E is a ground triple s p o<code>.</code>
|
|
then I(E) = true if </p>
|
|
<p>s, p and o are in V, <span >I(p) is in IP and</span> <I(s),I(o)>
|
|
is in IEXT(I(p))</p>
|
|
<p>otherwise I(E)= false.</p></td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td class="semantictable">if E is a ground RDF graph then I(E) = false if I(E') =
|
|
false for some triple E' in E, otherwise I(E) =true.</td>
|
|
</tr>
|
|
</tbody>
|
|
</table>
|
|
|
|
<p>If the vocabulary of an RDF graph contains names that are not in the vocabulary
|
|
of an interpretation I - that is, if I simply does not give a semantic value
|
|
to some <a href="#defname" class="termref">name</a> that is used in the graph
|
|
- then these truth-conditions will always yield the value false for some triple
|
|
in the graph, and hence for the graph itself. Turned around, this means that
|
|
any assertion of a graph implicitly asserts that all the <a href="#defname" class="termref">name</a>s
|
|
in the graph actually refer to something in the world. The final condition implies
|
|
that an empty graph (an empty set of triples) is trivially true.</p>
|
|
<p>Note that the denotation of plain literals is always in LV; <span >and that
|
|
those of the subject and object of any true triple must be in IR; so any URI
|
|
reference which occurs in a graph both as a predicate and as a subject or object
|
|
must denote something in the intersection of IR and IP in any interpretation
|
|
which satisfies the graph.</span></p>
|
|
|
|
|
|
<p>As an illustrative example, the following is a small interpretation for the
|
|
artificial vocabulary {<code>ex:a</code>,<code> ex:b</code>,<code> ex:c</code>,
|
|
<code>"whatever"</code>, <code>"whatever"^^ex:b</code>}.
|
|
Integers are used to indicate the non-literal 'things' in the universe. This
|
|
is not meant to imply that interpretations should be interpreted as being about
|
|
arithmetic, but more to emphasize that the exact nature of the things in the
|
|
universe is irrelevant. <span >LV can be any set satisfying the semantic conditions.</span>
|
|
(In this and subsequent examples the greater-than and less-than symbols are
|
|
used in several ways: following mathematical usage to indicate abstract pairs
|
|
and n-tuples; following N-Triples syntax to enclose URI references, and also
|
|
as arrowheads when indicating mappings.)</p>
|
|
<p>IR = LV union{1, 2}</p>
|
|
<p>IP={1}</p>
|
|
|
|
<p>IEXT: 1<code>=></code>{<1,2>,<2,1>}</p>
|
|
<p>IS: <code>ex:a=></code>1, <code>ex:b=></code>1, <code>ex:c=></code>2</p>
|
|
<p>IL: <code>"whatever"^^ex:b</code> <code>=></code>2 </p>
|
|
|
|
<div class="c1">
|
|
<p><img src="RDFSemanticsFigure1.jpg"
|
|
alt="A drawing of the domains and mappings described in the text"
|
|
/><br />
|
|
<b>Figure 1</b>: An example of an interpretation. Note, this is
|
|
not a picture of an RDF graph.<br />
|
|
The figure does not show the infinite number of members of
|
|
LV.</p>
|
|
</div>
|
|
<p>This interpretation makes these triples true:</p>
|
|
|
|
<p><code> <ex:a> <ex:b> <ex:c>
|
|
.</code></p>
|
|
|
|
<p><code> <ex:c> <ex:a> <ex:a>
|
|
.</code></p>
|
|
|
|
<p><code> <ex:c> <ex:b> <ex:a>
|
|
.</code></p>
|
|
|
|
<p><code> <ex:a> <ex:b>
|
|
"whatever"^^<ex:b> .</code></p>
|
|
|
|
<p>For example, I(<code><ex:a> <ex:b> <ex:c>
|
|
.</code>) = true if
|
|
<I(<code>ex:a</code>),I(<code>ex:c</code>)> is in
|
|
IEXT(I(<code><ex:b></code>)), i.e. if <1,2> is in
|
|
IEXT(1), which is {<1,2>,<2,1>} and so does contain
|
|
<1,2> and so I(<code><ex:a <ex:b> ex:c></code>)
|
|
is true.</p>
|
|
<p>The truth of the fourth <span >triple</span> is a consequence of the rather
|
|
idiosyncratic interpretation chosen here for typed literals.</p>
|
|
<p>In this interpretation IP is a subset of IR; this will be typical of RDF semantic
|
|
interpretations, but is not required. </p>
|
|
|
|
<p>It makes these triples false:</p>
|
|
|
|
<p><code> <ex:a> <ex:c> <ex:b>
|
|
.</code></p>
|
|
|
|
<p><code> <ex:a> <ex:b> <ex:b>
|
|
.</code></p>
|
|
|
|
<p><code> <ex:c> <ex:a> <ex:c>
|
|
.</code></p>
|
|
|
|
<p><code> <ex:a> <ex:b> "whatever"
|
|
.</code></p>
|
|
|
|
|
|
<p>For example, I(<code><ex:a> <ex:c> <ex:b> .</code>) = true
|
|
if <I(<code>ex:a</code>), I(<code><ex:b></code>)>, i.e.<1,1>,
|
|
is in IEXT(I(<code>ex:c</code>)); but I(<code>ex:c</code>)=2 which is not in
|
|
IP, so IEXT is not defined on 2, so the condition fails and I(<code><ex:a>
|
|
<ex:c> <ex:b> .</code>) = false.</p>
|
|
<p>It also makes all triples containing a plain literal false, since the property
|
|
extension does not have any pairs containing a plain literal.</p>
|
|
<p>To emphasize; this is only one possible interpretation of this vocabulary;
|
|
there are (infinitely) many others. For example, if this interpretation were
|
|
modified by attaching the property extension to 2 instead of 1, none of the
|
|
above triples would be true.</p>
|
|
<p>This example illustrates that any interpretation which maps any URI reference
|
|
which occurs in the predicate position of a triple in a graph to something not
|
|
in IP will make the graph false. </p>
|
|
|
|
<h3><a name="unlabel" id="unlabel">1.5. Blank Nodes as Existential
|
|
Variables</a></h3>
|
|
|
|
|
|
<p>Blank nodes are treated as simply indicating the existence of a thing, without
|
|
using, or saying anything about, the name of that thing. (This is not the same
|
|
as assuming that the blank node indicates an 'unknown' URI reference; for example,
|
|
it does not assume that there is any URI reference which refers to the thing.
|
|
The discussion of <a
|
|
href="#glossSkolemization" class="termref">Skolemization</a> in <a href="#prf">appendix
|
|
A</a> is relevant to this point.)</p>
|
|
<p>An interpretation can specify the truth-value of a graph containing blank nodes.
|
|
This will require some definitions, as the theory so far provides no meaning
|
|
for blank nodes. Suppose I is an interpretation and A is a mapping from some
|
|
set of blank nodes to the universe IR of I, and define I+A to be an extended
|
|
interpretation which is like I except that it uses A to give the interpretation
|
|
of blank nodes. Define blank(E) to be the set of blank nodes in E. Then the
|
|
above rules can be extended to include the two new cases that are introduced
|
|
when blank nodes occur in the graph:</p>
|
|
|
|
<div class="title">Semantic conditions for blank nodes.</div>
|
|
<table cellpadding="5" border="2" summary="Semantic conditions for blank nodes">
|
|
<tbody>
|
|
<tr>
|
|
|
|
<td class="semantictable">If E is a blank node and A(E) is defined then
|
|
[I+A](E) = A(E)</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td class="semantictable">If E is an RDF graph then I(E) = true if [I+A'](E) =
|
|
true for some mapping A' from blank(E) to IR, otherwise
|
|
I(E)= false.</td>
|
|
</tr>
|
|
</tbody>
|
|
</table>
|
|
<p class="termref">Notice that this does not change the definition of an interpretation;
|
|
it still consists of the same values IR, IP, IEXT, IS, LV and IL. It simply
|
|
extends the rules for defining denotations under an interpretation, so that
|
|
the same interpretation that provides a truth-value for ground graphs also assigns
|
|
truth-values to graphs with blank nodes, even though it provides no denotation
|
|
for the blank nodes themselves. Notice also that the blank nodes themselves
|
|
are perfectly well-defined entities; they differ from other nodes only in not
|
|
being assigned a denotation by an interpretation, reflecting the intuition that
|
|
they have no 'global' meaning (i.e. outside the graph in which they occur).</p>
|
|
|
|
|
|
<p><a name="bnodeExample" id="bnodeExample"></a>For example, the graph defined
|
|
by the following triples is false in the interpretation shown in figure 1:</p>
|
|
|
|
<p> <code> _:xxx <ex:a> <ex:b> .</code></p>
|
|
|
|
<p><code> <ex:c> <ex:b> _:xxx .</code></p>
|
|
|
|
<p>since if A' maps the blank node to 1 then the first triple is
|
|
false in I+A', and if it maps it to 2 then the second triple is
|
|
false.</p>
|
|
|
|
<p>Note that each of these triples, if thought of as a single
|
|
graph, would be true in I, but the whole graph is not; and that if
|
|
a different nodeID were used in the two triples, indicating that
|
|
the RDF graph had two blank nodes instead of one, then A' could map
|
|
one node to 2 and the other to 1, and the resulting graph would be
|
|
true under the interpretation I.</p>
|
|
|
|
<p>This effectively treats all blank nodes as having the same meaning as existentially
|
|
quantified variables in the RDF graph in which they occur, and which have the
|
|
scope of the entire graph. In terms of the N-Triples syntax, this amounts to
|
|
the convention that would place the quantifiers just outside, or at the outer
|
|
edge of, the N-Triples document corresponding to the graph. This in turn means
|
|
that there is a subtle but important distinction in meaning between the operation
|
|
of forming the union of two graphs and that of forming the <a href="#defmerge" class="termref">merge</a>.
|
|
The simple union of two graphs corresponds to the conjunction ( 'and' ) of all
|
|
the triples in the graphs, maintaining the identity of any blank nodes which
|
|
occur in both graphs. This is appropriate when the information in the graphs
|
|
comes from a single source, or where one is derived from the other by means
|
|
of some <a href="#glossValid"
|
|
class="termref">valid</a> inference process, as for example when applying
|
|
an inference rule to add a triple to a graph. Merging two graphs treats <span >the
|
|
blank nodes in each graph as being existentially quantified in that graph</span>,
|
|
so that no blank node from one graph is allowed to stray into the scope of the
|
|
other graph's surrounding quantifier. This is appropriate when the graphs come
|
|
from different sources and there is no justification for assuming that a blank
|
|
node in one refers to the same entity as any blank node in the other. </p>
|
|
<h2><a name="entail" id="entail">2. Simple Entailment between RDF graphs</a> </h2>
|
|
<p>Following conventional terminology, I <a
|
|
id="defsatis" name="defsatis"></a><i>satisfies</i> E if I(E)=true, and a set
|
|
S of RDF graphs <a id="defentail"
|
|
name="defentail"></a><em>(simply)</em> <a href="#glossEntail"
|
|
class="termref"><em>entails</em></a> <span >a graph</span> E if every interpretation
|
|
which satisfies every member of S also satisfies E. In later sections these
|
|
notions will be adapted to other classes of interpretations, but throughout
|
|
this section 'entailment' should be interpreted as meaning simple entailment.
|
|
</p>
|
|
|
|
<p>Entailment is the key idea which connects model-theoretic
|
|
semantics to real-world applications. As noted earlier, making an
|
|
assertion amounts to claiming that the world is an interpretation
|
|
which assigns the value true to the assertion. If A entails B, then
|
|
any interpretation that makes A true also makes B true, so that an
|
|
assertion of A already contains the same "meaning" as an assertion
|
|
of B; one could say that the meaning of B is somehow contained in,
|
|
or subsumed by, that of A. If A and B entail each other, then they
|
|
both "mean" the same thing, in the sense that asserting either of
|
|
them makes the same claim about the world. The interest of this
|
|
observation arises most vividly when A and B are different
|
|
expressions, since then the relation of entailment is exactly the
|
|
appropriate semantic license to justify an application inferring or
|
|
generating one of them from the other. Through the notions of
|
|
satisfaction, entailment and validity, formal semantics gives a
|
|
rigorous definition to a notion of "meaning" that can be related
|
|
directly to computable methods of determining whether or not
|
|
meaning is preserved by some transformation on a representation of
|
|
knowledge.</p>
|
|
|
|
<p><a id="defvalid" name="defvalid">Any process which constructs a
|
|
graph E from some other graph(s) S is said to be <em>(simply)
|
|
valid</em> if S entails E </a><span >in every case</span>,
|
|
otherwise <em>invalid.</em> Note
|
|
that being an invalid process does not mean that the conclusion is
|
|
false, and being <a href="#glossValid"
|
|
class="termref">valid</a> does not guarantee truth. However, validity
|
|
represents the best guarantee that any assertional language can
|
|
offer: if given true inputs, it will never draw a false conclusion
|
|
from them.</p>
|
|
<p>This section gives a few basic results about simple entailment and <a href="#glossValid"
|
|
class="termref">valid</a> <a href="#glossInference"
|
|
class="termref">inference</a>. Simple entailment can be recognized by relatively
|
|
simple syntactic comparisons. The two basic forms of simply valid inference
|
|
in RDF are, in logical terms, the inference from (P and Q) to P, and the inference
|
|
from foo(baz) to (exists (?x) foo(?x)).</p>
|
|
|
|
|
|
<p>These results apply only to simple entailment, not to the extended notions
|
|
of entailment introduced in later sections. Proofs, all of which are straightforward,
|
|
are given in <a href="#prf" class="termref">appendix A</a>, which also describes some other
|
|
properties of entailment which may be of interest.</p>
|
|
<p><strong>Empty Graph Lemma.</strong> The empty set of triples is entailed by
|
|
any graph, and does not entail any graph except itself. <a href="#emptygraphlemmaprf" class="termref">[Proof]</a></p>
|
|
<p><a name="subglem" id="subglem"><strong>Subgraph Lemma.</strong></a> A graph
|
|
entails all its <a
|
|
href="#defsubg" class="termref">subgraphs</a>. <a href="#subglemprf" class="termref">[Proof]</a></p>
|
|
<p><a name="instlem" id="instlem"><strong>Instance Lemma.</strong></a> A graph
|
|
is entailed by any of its <a
|
|
href="#definst" class="termref">instances</a>.<a href="#instlemprf" class="termref">[Proof]</a></p>
|
|
<p >The relationship between merging and entailment is simple,
|
|
and obvious from the definitions:</p>
|
|
<p><a name="mergelem" id="mergelem"><strong>Merging lemma.</strong></a> The merge
|
|
of a set S of RDF graphs is entailed by S, and entails every member of S. <a href="#mergelemprf" class="termref">[Proof]</a></p>
|
|
|
|
<p>This means that a set of graphs can be treated as <a
|
|
href="#glossEquivalent" class="termref">equivalent</a> to its
|
|
merge, i.e. a single graph, as far as the <a
|
|
href="#glossModeltheory" class="termref">model theory</a> is
|
|
concerned. This can
|
|
be used to simplify the terminology somewhat: for example, the definition
|
|
of
|
|
S entails E, above, can be paraphrased by saying that S entails E when every
|
|
interpretation which satisfies S also
|
|
satisfies E.</p>
|
|
<p >The <a href="#bnodeExample" >example</a> given in section 1.5 shows that it is not the case, in general,
|
|
that the simple union of a set of graphs is entailed by the set.</p>
|
|
<p>The main result for simple RDF inference is:</p>
|
|
<p><a name="interplemma" id="interplemma"><strong>Interpolation Lemma.</strong>
|
|
S entails a graph E if and only if a subgraph of S is an instance of E.</a><a href="#interplemmaprf" class="termref">[Proof]</a></p>
|
|
<p>The interpolation lemma completely characterizes simple RDF entailment in syntactic
|
|
terms. To tell whether a set of RDF graphs entails another, <span >check that
|
|
there is some instance of the entailed graph which is a subset of the merge
|
|
of the original set of graphs</span>. Of course, there is no need to actually
|
|
construct the merge. If working backwards from the <a
|
|
href="#glossConsequent" class="termref">consequent E</a>, an efficient technique
|
|
would be to treat blank nodes as variables in a process of subgraph-matching,
|
|
allowing them to bind to 'matching' <a href="#defname" class="termref">name</a>s
|
|
in the <a href="#glossAntecedent"
|
|
class="termref">antecedent</a> graph(s) in S, i.e. those which may entail
|
|
the <a href="#glossConsequent"
|
|
class="termref">consequent</a> graph. The interpolation lemma shows that this
|
|
process is <a href="#glossValid"
|
|
class="termref">valid</a>, and is also <a href="#glossComplete"
|
|
class="termref">complete</a> if the subgraph-matching algorithm is. The existence
|
|
of <a href="#glossComplete"
|
|
class="termref">complete</a> subgraph-checking algorithms also shows that
|
|
RDF entailment is decidable, i.e. there is a terminating algorithm which will
|
|
determine for any finite set S and any graph E, whether or not S entails E.</p>
|
|
<p>Such a variable-binding process would only be appropriate when applied to the
|
|
<em>conclusion</em> of a proposed entailment. This corresponds to using the
|
|
document as a goal or a query, in contrast to asserting it, i.e. claiming it
|
|
to be true. If an RDF document is asserted, then it would be invalid to bind
|
|
new values to any of its blank nodes, since the resulting graph might not be
|
|
entailed by the assertion.</p>
|
|
<p>The interpolation lemma has an immediate consequence a criterion for non-entailment:</p>
|
|
<p><a name="Anonlem1" id="Anonlem1"><strong>Anonymity lemma.</strong></a> Suppose
|
|
E is a <a href="#deflean"
|
|
class="termref">lean</a> graph and E' is a proper instance of E. Then E does
|
|
not entail E'.<a href="#Anonlem1prf" class="termref">[Proof]</a></p>
|
|
<p>Note again that this applies only to simple entailment, not to the vocabulary
|
|
entailment relationships defined in rest of the document.</p>
|
|
|
|
<p>Several basic properties of entailment follow directly from the above definitions
|
|
and results but are stated here for completeness sake:</p>
|
|
<p><strong><a name="monotonicitylemma" id="monotonicitylemma"></a>Monotonicity
|
|
Lemma</strong>. Suppose S is a subgraph of S' and S entails E. Then S' entails
|
|
E.<a href="#monotonicitylemmaprf" class="termref">[Proof]</a></p>
|
|
<p>The property of finite expressions always being derivable from a finite set
|
|
of antecedents is called <em>compactness</em>. Semantic theories which support
|
|
non-compact notions of entailment do not have corresponding computable inference
|
|
systems.</p>
|
|
<p><strong><a name="compactlemma" id="compactlemma"></a>Compactness Lemma</strong>.
|
|
If S entails E and E is a finite graph, then some finite subset S' of S entails
|
|
E.</p>
|
|
<h3><a name="vocabulary_entail" id="vocabulary_entail"></a><span >2.1
|
|
Vocabulary interpretations and vocabulary entailment</span></h3>
|
|
<p >Simple interpretations and simple entailment capture the semantics of RDF
|
|
graphs when no attention is paid to the particular meaning of any of the names
|
|
in the graph. To obtain the full meaning of an RDF graph written using a particular
|
|
vocabulary, it is usually necessary to add further semantic conditions which
|
|
attach stronger meanings to particular URI references and typed literals in
|
|
the graph. Interpretations which are required to satisfy extra semantic conditions
|
|
on a particular vocabulary will be generically referred to as <em>vocabulary
|
|
interpretations</em>. Vocabulary entailment means entailment with respect to
|
|
such vocabulary interpretations. These stronger notions of interpretation and
|
|
entailment are indicated by the use of a namespace prefix, so that we will refer
|
|
to <em>rdf-entailment</em>, <em>rdfs-entailment</em> and so on in what follows.
|
|
In each case, the vocabulary whose meaning is being restricted, and the exact
|
|
conditions associated with that vocabulary, are spelled out in detail. </p>
|
|
<h2><a name="InterpVocab" id="InterpVocab">3. Interpreting the RDF Vocabulary</a> </h2>
|
|
<h3><a name="RDFINTERP" id="RDFINTERP">3.1 RDF Interpretations</a></h3>
|
|
|
|
<p ><a name="defRDFV" id="defRDFV"></a>The <em>RDF vocabulary, </em>rdfV, is a
|
|
set of URI references in the <code>rdf:</code> namespace:</p>
|
|
|
|
<div class="c1">
|
|
|
|
<table border="1" summary="rdf vocabulary">
|
|
<tbody>
|
|
<tr>
|
|
<td class="othertable"><strong>RDF vocabulary</strong></td>
|
|
</tr>
|
|
|
|
<tr>
|
|
|
|
<td class="othertable"> <code>rdf:type</code> <code>rdf:Property
|
|
rdf:XMLLiteral rdf:nil rdf:List rdf:Statement rdf:subject rdf:predicate
|
|
rdf:object rdf:first rdf:rest rdf:Seq rdf:Bag rdf:Alt rdf:_1 rdf:_2
|
|
... rdf:value</code></td>
|
|
</tr>
|
|
</tbody>
|
|
</table>
|
|
<p><a name="defXMLdatatype" id="defXMLdatatype"></a><a href="#rdfinterpdef" class="termref">rdf-interpretation</a>s
|
|
impose extra semantic conditions on <a href="#defRDFV" class="termref">rdfV</a>
|
|
and on typed literals with the type <code>rdf:XMLLiteral</code>, which is
|
|
referred to as the RDF built-in datatype. This datatype is <a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#section-XMLLiteral">fully
|
|
described</a> in the <i><a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/">RDF
|
|
Concepts and Abstract Syntax</a></i> document [<cite><a href="#ref-rdf-concepts">RDF-CONCEPTS</a></cite>].
|
|
Any character string <em>sss</em> which satisfies the conditions for being
|
|
in the <a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#XMLLiteral-lexical-space">
|
|
lexical space of <code>rdf:XMLLiteral</code></a> will be called a <em>well-typed
|
|
XML literal string</em>. The corresponding value will be called the <em>XML
|
|
value of</em> the literal. <span >Note that the XML values of well-typed XML
|
|
literals are in precise 1:1 correspondence with the XML literal strings of
|
|
such literals, but are not themselves character strings</span>. An XML literal
|
|
whose literal string is well-typed will be called a <em>well-typed XML literal</em>;
|
|
other XML literals will be called <em>ill-typed</em>. </p>
|
|
</div>
|
|
|
|
|
|
<p> <a id="rdfinterpdef" name="rdfinterpdef"></a>An <i>rdf-interpretation</i>
|
|
of a vocabulary V is a simple interpretation I <span >of (V union <a href="#defRDFV" class="termref">rdfV</a>)</span>
|
|
which satisfies the extra conditions described in the following table<span >
|
|
and all the triples in the subsequent table. These triples are called the <em>rdf
|
|
axiomatic triples</em>. </span></p>
|
|
|
|
<div class="title">RDF semantic conditions.</div>
|
|
<table border="1" summary="RDF semantic conditions">
|
|
<tbody>
|
|
<tr>
|
|
<td class="semantictable"><p><a name="rdfsemcond1" id="rdfsemcond1"></a>x is
|
|
in IP if and only if <x, I(<code>rdf:Property</code>)> is in IEXT(I(<code>rdf:type</code>))</p></td>
|
|
</tr>
|
|
<tr>
|
|
<td class="semantictable"><p><a name="rdfsemcond2" id="rdfsemcond2"></a>If
|
|
<span ><code>"</code>xxx<code>"^^rdf:XMLLiteral</code></span>
|
|
is in V and xxx is a well-typed XML literal string, then </p>
|
|
<p>IL<span >(<code>"</code>xxx<code>"^^rdf:XMLLiteral</code>)
|
|
is the XML <span >value</span> of xxx;</span><br />
|
|
<span >IL(<code>"</code>xxx<code>"^^rdf:XMLLiteral</code>)
|
|
is in LV;<br />
|
|
IEXT(I(<code>rdf:type</code>)) contains <IL(<code>"</code>xxx<code>"^^rdf:XMLLiteral</code>),
|
|
I(<code>rdf:XMLLiteral</code>)></span></p>
|
|
</td>
|
|
</tr>
|
|
<tr>
|
|
<td class="semantictable"><p><span > <a name="rdfsemcond3" id="rdfsemcond3"></a>If
|
|
<span ><code>"</code>xxx<code>"^^rdf:XMLLiteral</code></span>
|
|
is in V and xxx is an ill-typed XML literal string, then</span></p>
|
|
<p><span >IL(<code>"</code>xxx<code>"^^rdf:XMLLiteral</code>)
|
|
is not in LV;<br />
|
|
IEXT(I(<code>rdf:type</code>)) does not contain <IL(<code>"</code>xxx<code>"^^rdf:XMLLiteral</code>),
|
|
I(<code>rdf:XMLLiteral</code>)>.</span> </p></td>
|
|
</tr>
|
|
</tbody>
|
|
</table>
|
|
|
|
|
|
|
|
<p>
|
|
The <a href="#rdfsemcond1" class="termref">first condition</a> could be regarded as defining IP to be the set of
|
|
resources in the universe of the interpretation which have the value I(<code>rdf:Property</code>)
|
|
of the property I(<code>rdf:type</code>). Such subsets of the universe will
|
|
be central in interpretations of RDFS. Note that this condition requires
|
|
IP to be a subset of IR. The <a href="#rdfsemcond3" class="termref">third condition</a> requires that ill-typed XML literals
|
|
denote something other than a literal value: this will be the standard way of
|
|
handling ill-formed typed literals.
|
|
|
|
</p>
|
|
|
|
|
|
|
|
<div class="title">RDF axiomatic triples.</div>
|
|
|
|
<table border="1" summary="RDF axiomatic triples">
|
|
<tr>
|
|
<td class="ruletable"><a name="RDF_axiomatic_triples" id="RDF_axiomatic_triples"> </a><code>rdf:type rdf:type rdf:Property .<br />
|
|
rdf:subject rdf:type rdf:Property .<br />
|
|
rdf:predicate rdf:type rdf:Property .<br />
|
|
rdf:object rdf:type rdf:Property .<br />
|
|
rdf:first rdf:type rdf:Property .<br />
|
|
rdf:rest rdf:type rdf:Property .<br />
|
|
rdf:value rdf:type rdf:Property .<br />
|
|
rdf:_1 rdf:type rdf:Property .<br />
|
|
rdf:_2 rdf:type rdf:Property .<br />
|
|
... <br />
|
|
rdf:nil rdf:type rdf:List .</code></td>
|
|
</tr>
|
|
</table>
|
|
<p >The <a href="#rdfsinterpdef" class="termref">rdfs-interpretation</a>s described
|
|
in <a href="#rdfs_interp">section 4</a> below assign further semantic
|
|
conditions (range and domain conditions) to the properties used in the RDF
|
|
vocabulary, and other semantic extensions <strong title="MAY in RFC 2119 context" class="RFC2119">MAY</strong>
|
|
impose further conditions so as to further restrict their meanings, provided
|
|
that such conditions<strong title="MUST in RFC 2119 context" class="RFC2119">
|
|
MUST</strong> be compatible with the conditions described in this section.</p>
|
|
|
|
<p>For example, the following rdf-interpretation extends the simple interpretation
|
|
in figure 1 to the case <span >where V contains <a href="#defRDFV" class="termref">rdfV</a></span>.
|
|
For simplicity, we ignore XML literals in this example.</p>
|
|
|
|
<p>IR = <span >LV union </span>{1, 2, T , P}</p>
|
|
<p>IP = {1, T}</p>
|
|
|
|
<p>IEXT: 1<code>=></code>{<1,2>,<2,1>},
|
|
T<code>=></code>{<1,P>,<T,P>}</p>
|
|
|
|
<p>IS: <code>ex:a=></code>1, <code>ex:b=></code>1,
|
|
<code>ex:c=></code> 2, <code>rdf:type=></code>T,
|
|
<code>rdf:Property=></code>P, <code>rdf:nil=></code>1,
|
|
<code>rdf:List=></code>P, <code>rdf:Statement=></code>P<code>,
|
|
rdf:subject=></code>1<code>, rdf:predicate=></code>1<code>, rdf:object=></code>1<code>,
|
|
rdf:first=></code>1<code>, rdf:rest=></code>1<code>, rdf:Seq=></code>P<code>,
|
|
rdf:Bag=></code>P<code>, rdf:Alt=></code>P<code>, rdf:_1, rdf:_2, ...
|
|
=></code>1</p>
|
|
<div class="c1">
|
|
<p><img src="RDFMTFigure2.jpg"
|
|
alt="A drawing of the domains and mappings described in the text" />
|
|
<br />
|
|
<b>Figure 2</b>: An rdf-interpretation.</p>
|
|
</div>
|
|
|
|
<p>This is not the smallest rdf-interpretation which extends the
|
|
earlier example, since one could have made
|
|
IEXT(T) be
|
|
{<1,2>,<T,2>}, and managed without having P in the
|
|
universe. In general, a given entity in an interpretation may play
|
|
several 'roles' at the same time, as long as this can be done
|
|
without violating any of the required semantic conditions. The
|
|
above interpretation identifies properties with lists, for example;
|
|
of course, other interpretations might not make such an
|
|
identification.</p>
|
|
<p>Every <a href="#rdfinterpdef" class="termref">rdf-interpretation</a> is also a simple interpretation. The 'extra' structure
|
|
does not prevent it acting in the simpler role.</p>
|
|
<h3><a name="rdf_entail" id="rdf_entail"></a>3.2. RDF entailment</h3>
|
|
<p>S <i>rdf-entails</i> E when every rdf-interpretation which satisfies every
|
|
member of S also satisfies E. This follows the wording of the definition of
|
|
<a href="#defentail" class="termref">simple entailment</a> in <a href="#entail" >
|
|
Section 2</a>, but refers only to <a href="#rdfinterpdef" class="termref">rdf-interpretation</a>s
|
|
instead of all simple interpretations. <span >Rdf-entailment is an example of
|
|
<a href="#vocabulary_entail" class="termref">vocabulary entailment</a>. </span></p>
|
|
<p>It is easy to see that the lemmas in <a href="#entail" > Section 2</a> do not all apply to rdf-entailment:
|
|
for example, the triple</p>
|
|
<p><code>rdf:type rdf:type rdf:Property .</code></p>
|
|
<p>is true in every <a href="#rdfinterpdef" class="termref">rdf-interpretation</a>, so is rdf-entailed by the empty graph,
|
|
contradicting the interpolation lemma for rdf-entailment. <a href="#RDFRules" > Section 7.2</a> describes
|
|
exact conditions for detecting RDF entailment.</p>
|
|
<h3><a name="ReifAndCont" id="ReifAndCont">3.3. Reification, Containers</a>, Collections
|
|
and rdf:value</h3>
|
|
<p>The RDF semantic conditions impose significant formal constraints on the meaning
|
|
only of the central RDF vocabulary, so the notions of rdf-entailment and <a href="#rdfinterpdef" class="termref">rdf-interpretation</a>
|
|
apply to the remainder of the vocabulary without further change. This includes
|
|
vocabulary which is intended for use in describing containers and bounded collections,
|
|
and a reification vocabulary to enable an RDF graph to describe, as well as
|
|
exhibit, triples. In this section we review the intended meanings of this vocabulary,
|
|
and note some intuitive consequences which are not supported by the formal <a
|
|
href="#glossModeltheory" class="termref">model theory</a>. Semantic extensions
|
|
<strong title="MAY in RFC 2119 context" class="RFC2119">MAY</strong> limit the
|
|
formal interpretations of these vocabularies to conform to these intended meanings.</p>
|
|
<p>The omission of these conditions from the formal semantics is a design decision
|
|
to accomodate variations in existing RDF usage and to make it easier to implement
|
|
processes to check formal RDF entailment. For example, implementations may decide
|
|
to use special procedural techniques to implement the RDF collection vocabulary.</p>
|
|
|
|
<h4><a name="Reif" id="Reif">3.3.1 Reification</a></h4>
|
|
|
|
<div class="c1">
|
|
<table border="1" summary="reification vocabulary">
|
|
<tbody>
|
|
<tr>
|
|
<td class="othertable"><strong>RDF reification vocabulary</strong></td>
|
|
</tr>
|
|
<tr>
|
|
<td class="othertable"><code>rdf:Statement rdf:subject rdf:predicate
|
|
rdf:object</code></td>
|
|
</tr>
|
|
</tbody>
|
|
</table>
|
|
</div>
|
|
|
|
<p>Semantic extensions <strong title="MAY in RFC 2119 context" class="RFC2119">MAY</strong> limit the interpretation of these so
|
|
that a triple of the form</p>
|
|
|
|
<p>aaa <code>rdf:type rdf:Statement .</code></p>
|
|
|
|
<p>is true in I just when I(aaa) is a <a href="#glossToken"
|
|
class="termref">token</a> of an RDF triple in some RDF document,
|
|
and the three properties, when applied to such a denoted triple,
|
|
have the same values as the respective components of that
|
|
triple.</p>
|
|
|
|
<p>This may be illustrated by considering the following two RDF
|
|
graphs, the first of which consists of a single triple.</p>
|
|
|
|
<p><code><ex:a> <ex:b> <ex:c> .</code></p>
|
|
|
|
<p>and</p>
|
|
|
|
<p><code>_:xxx rdf:type rdf:Statement .<br />
|
|
_:xxx rdf:subject <ex:a> .<br />
|
|
_:xxx rdf:predicate <ex:b> .<br />
|
|
_:xxx rdf:object <ex:c> .</code></p>
|
|
|
|
<p>The second graph is called a <i><a href="#glossReify"
|
|
class="termref">reification</a></i> of the triple in the first
|
|
graph, and the node which is intended to refer to the first triple
|
|
- the blank node in the second graph - is called, rather
|
|
confusingly, a <em>reified triple</em>. (This can be a blank node
|
|
or a URI reference.) In the intended interpretation of the reification
|
|
vocabulary, the second graph would be made true in an
|
|
interpretation I by interpreting the reified triple to refer to a
|
|
token of the triple in the first graph in some concrete RDF
|
|
document, considering that token to be valid RDF syntax, and then
|
|
using I to interpret the syntactic triple which the token
|
|
instantiates, so that the subject, predicate and object of that
|
|
triple are interpreted in the same way in the reification as in the
|
|
triple described by the reification. This could be stated formally
|
|
as follows: <x,y> is in IEXT(I(<code>rdf:subject</code>))
|
|
just when x is a token of an RDF triple of the form</p>
|
|
|
|
<p>aaa bbb ccc .</p>
|
|
|
|
<p>and y is I(aaa); similarly for predicate and object. Notice that
|
|
the value of the <code>rdf:subject</code> property is not the
|
|
subject URI reference itself but its interpretation, and so this condition
|
|
involves a two-stage interpretation process: one has to interpret
|
|
the reified node - the subject of the triples in the reification -
|
|
to refer to another triple, then treat that triple as RDF syntax
|
|
and apply the interpretation mapping again to get to the referent
|
|
of its subject. This requires triple tokens to exist as first-class
|
|
entities in the universe IR of an interpretation. In sum: the
|
|
meaning of the reification is that a document exists containing a
|
|
triple token which means whatever the first graph means.<span >Note
|
|
that this way of understanding the reification vocabulary does not interpret
|
|
reification as a form of quotation. Rather, the reification describes the
|
|
relationship between a token of a triple and the resources that triple refers
|
|
to. The reification can be read intuitively as saying "'this piece of
|
|
RDF talks about these things" rather than "this piece of RDF has
|
|
this form".</span></p>
|
|
|
|
<p>The semantic extension described here requires
|
|
the reified triple that the reification describes -
|
|
I(<code>_:xxx</code>) in the above example - to be a particular token
|
|
or instance of a triple in a (real
|
|
or notional) RDF document, rather than an 'abstract' triple
|
|
considered as a grammatical form. There could be several such
|
|
entities which have the same subject, predicate and object
|
|
properties. Although a graph is defined as a set of triples,
|
|
several such tokens with the same triple structure might occur in
|
|
different documents. Thus, it would be meaningful to claim that the
|
|
blank node in the second graph above does not refer to the triple
|
|
in the first graph, but to some other triple with the same
|
|
structure. This particular interpretation of reification was chosen
|
|
on the basis of use cases where properties such as dates of
|
|
composition or provenance information have been applied to the
|
|
reified triple, which are meaningful only when thought of as
|
|
referring to a particular instance or token of a triple. </p>
|
|
<p>Although RDF applications may use reification to refer to triple tokens in
|
|
RDF documents, the connection between the document and its reification must
|
|
be maintained by some means external to <span >the RDF graph
|
|
syntax. (In the RDF/XML syntax described in <i><a
|
|
href="http://www.w3.org/TR/2003/WD-rdf-syntax-grammar-20030123/">RDF/XML
|
|
Syntax Specification (Revised)</a></i> [<a href="#ref-rdf-syntax">RDF-SYNTAX</a>],
|
|
the rdf:ID attribute can be used in the description of a triple to create a
|
|
reification of that triple in which the reified triple is a URI constructed
|
|
from the baseURI of the XML document and the value of rdf:ID as a fragment.)</span>
|
|
Since an assertion of a reification of a triple does not implicitly assert the
|
|
triple itself, this means that there are <em>no</em> entailment relationships
|
|
which hold between a triple and a reification of it. Thus the reification vocabulary
|
|
has no effective semantic constraints on it, other than those that apply to
|
|
an <a href="#rdfinterpdef" class="termref">rdf-interpretation</a>. </p>
|
|
|
|
<p>A reification of a triple does not entail the triple, and is not
|
|
entailed by it. (The
|
|
reification only says that the triple token exists and what it is about,
|
|
not that it is true. The second non-entailment is a consequence of the
|
|
fact
|
|
that asserting a triple does not automatically assert that any
|
|
triple tokens exist in the universe being described by the triple.
|
|
For example, the triple might be part of an ontology describing
|
|
animals, which could be satisfied by an interpretation in which the
|
|
universe contained only animals, and in which a reification of it was therefore
|
|
false.)</p>
|
|
|
|
<p>Since the relation between triples and reifications of triples
|
|
in any RDF graph or graphs need not be one-to-one, asserting a
|
|
property about some entity described by a reification need not
|
|
entail that the same property holds of another such entity, even if
|
|
it has the same components. For example,</p>
|
|
|
|
<p><code>_:xxx rdf:type rdf:Statement .<br />
|
|
_:xxx rdf:subject <ex:subject> .<br />
|
|
_:xxx rdf:predicate <ex:predicate> .<br />
|
|
_:xxx rdf:object <ex:object> .<br />
|
|
_:yyy rdf:type rdf:Statement .<br />
|
|
_:yyy rdf:subject <ex:subject> .<br />
|
|
_:yyy rdf:predicate <ex:predicate> .<br />
|
|
_:yyy rdf:object <ex:object> .<br />
|
|
_:xxx <ex:property> <ex:foo> .</code></p>
|
|
|
|
<p>does not entail</p>
|
|
|
|
<p><code>_:yyy <ex:property> <ex:foo> .</code></p>
|
|
|
|
|
|
<h4><a name="Containers" id="Containers">3.3.2 RDF containers</a></h4>
|
|
|
|
<table border="1" summary="container vocabulary">
|
|
<tbody>
|
|
<tr>
|
|
<td class="othertable"><strong>RDF Container Vocabulary</strong></td>
|
|
</tr>
|
|
<tr>
|
|
<td class="othertable"><code>rdf:Seq rdf:Bag rdf:Alt rdf:_1 rdf:_2
|
|
...</code></td>
|
|
</tr>
|
|
</tbody>
|
|
</table>
|
|
<p>RDF provides vocabularies for describing three classes of
|
|
containers. Containers have a type, and their members can
|
|
be enumerated by using a fixed set of <em>container membership
|
|
properties</em>. These properties are indexed by integers to
|
|
provide a way to distinguish the members from each other, but these
|
|
indices should not necessarily be thought of as defining an
|
|
ordering of the container itself; some containers are considered to be unordered.</p>
|
|
|
|
<p>The RDFS vocabulary, described below, adds a generic membership
|
|
property which holds regardless of position, and classes containing
|
|
all the containers and all the membership properties.</p>
|
|
|
|
<p>One should understand this RDF vocabulary as <em>describing</em>
|
|
containers, rather than as a vocabulary for constructing them, as
|
|
would typically be supplied by a programming language. On this
|
|
view, the actual containers are entities in the semantic universe,
|
|
and RDF graphs which use the vocabulary simply provide very basic
|
|
information about these entities, enabling an RDF graph to
|
|
characterize the container type and give partial information about
|
|
the members of a container. Since the RDF container vocabulary is
|
|
so limited, many 'natural' assumptions concerning RDF containers
|
|
are not formally sanctioned by the RDF <a href="#glossModeltheory"
|
|
class="termref">model theory</a>. This should not be taken as
|
|
meaning that these assumptions are false, but only that RDF does
|
|
not formally entail that they must be true.</p>
|
|
|
|
<p>There are no special semantic conditions on the container
|
|
vocabulary: the only 'structure' which RDF presumes its containers
|
|
to have is what can be inferred from the use of this vocabulary and
|
|
the <span >general RDF</span> semantic conditions. <span >In
|
|
general, this amounts to knowing the type of a container, and having a partial
|
|
enumeration
|
|
of the items in the container.</span> The intended mode of use is that things
|
|
of type <code>rdf:Bag</code>
|
|
are considered to be unordered but to allow duplicates; things of
|
|
type <code>rdf:Seq</code> are considered to be ordered, and things
|
|
of type <code>rdf:Alt</code> are considered to represent a
|
|
collection of alternatives, possibly with a preference ordering.
|
|
The ordering of items in an ordered container is intended to be
|
|
indicated by the numerical ordering of the container membership
|
|
properties, <span >which are assumed to be single-valued</span>.
|
|
However, these informal interpretations are not reflected in any formal RDF
|
|
entailments.</p>
|
|
|
|
|
|
<p>RDF does not support any entailments which could arise from <span >enumerating
|
|
the elements of an <code>rdf:Bag</code> in a different order</span>. For example,</p>
|
|
|
|
<p><code>_:xxx rdf:type rdf:Bag .<br />
|
|
_:xxx rdf:_1 <ex:a> .<br />
|
|
_:xxx rdf:_2 <ex:b> .</code></p>
|
|
|
|
<p>does not entail</p>
|
|
|
|
<p><code>_:xxx rdf:_1 <ex:b> .<br />
|
|
_:xxx rdf:_2 <ex:a> .</code></p>
|
|
|
|
<p>Notice that if this conclusion were <a href="#glossValid"
|
|
class="termref">valid</a>, then the result of
|
|
conjoining it to the original graph would also be a <a href="#glossValid"
|
|
class="termref">valid</a>
|
|
entailment, which would assert that both elements were in both
|
|
positions. This is a consequence of the fact that RDF is a purely
|
|
assertional language.</p>
|
|
|
|
<p>There is no assumption that a property of a container applies to
|
|
any of the elements of the container, or vice versa. </p>
|
|
<p>There is no formal requirement that
|
|
the three container classes are disjoint, so that for example
|
|
something can be asserted to be both an <code>rdf:Bag</code> and an <code>rdf:Seq</code>.
|
|
There is no assumption that containers are gap-free, so that for example</p>
|
|
<p><code>_:xxx rdf:type rdf:Seq.<br />
|
|
_:xxx rdf:_1 <ex:a> .<br />
|
|
_:xxx rdf:_3 <ex:c> .</code></p>
|
|
|
|
<p>does not entail</p>
|
|
|
|
<p><code>_:xxx rdf:_2 _:yyy .</code></p>
|
|
|
|
<p>There is no way in RDF to 'close' a container, i.e. to assert
|
|
that it contains only a fixed number of members. This is a
|
|
reflection of the fact that it is always consistent to add a triple
|
|
to a graph asserting a membership property of any container. And
|
|
finally, there is no built-in assumption that an RDF container has
|
|
only finitely many members.</p>
|
|
|
|
|
|
<h4><a name="collections" id="collections"></a>3.3.3 RDF collections</h4>
|
|
|
|
<table border="1" summary="collection vocabulary">
|
|
<tbody>
|
|
<tr>
|
|
<td class="othertable"><strong>RDF Collection Vocabulary</strong></td>
|
|
</tr>
|
|
<tr>
|
|
<td class="othertable"><code>rdf:List rdf:first rdf:rest rdf:nil</code></td>
|
|
</tr>
|
|
</tbody>
|
|
</table>
|
|
<p>RDF provides a vocabulary for describing collections, i.e.'list
|
|
structures', in terms of head-tail links. Collections differ from
|
|
containers in allowing branching structure and in having an
|
|
explicit terminator, allowing applications to determine the exact
|
|
set of items in the collection.</p>
|
|
|
|
|
|
<p>As with containers, no special semantic conditions are imposed on this vocabulary
|
|
other than the type of <code>rdf:nil</code> being <code>rdf:List</code>. It
|
|
is intended for use typically in a context where a container is described using
|
|
blank nodes to connect a 'well-formed' sequence of items, each described by
|
|
two triples of the form<code><br />
|
|
<br />
|
|
_:c1 rdf:first aaa .<br />
|
|
_:c1 rdf:rest _:c2</code></p>
|
|
|
|
|
|
<p>where the final item is indicated by the use of <code>rdf:nil</code> as the
|
|
value of the property <code>rdf:rest</code>. In a familiar convention, <code>rdf:nil</code>
|
|
can be thought of as the empty collection. Any such graph amounts to an assertion
|
|
that the collection exists, and since the members of the collection can be determined
|
|
by inspection, this is often sufficient to enable applications to determine
|
|
what is meant. Note however that the semantics does not require any collections
|
|
to exist other than those mentioned explicitly in a graph (and the empty collection).
|
|
For example, the existence of a collection containing two items does not automatically
|
|
guarantee that the similar collection with the items permuted also exists:<code><br />
|
|
<br />
|
|
_:c1 rdf:first <ex:aaa> .<br />
|
|
_:c1 rdf:rest _:c2 .<br />
|
|
<span > _:c2 rdf:first</span> <ex:bbb> .<br />
|
|
_:c2 rdf:rest rdf:nil . </code></p>
|
|
<p>does not entail</p>
|
|
|
|
<p><code>_:c3 rdf:first <ex:bbb> .<br />
|
|
_:c3 rdf:rest _:c4 .<br />
|
|
<span >_:c4 rdf:first</span> <ex:aaa> .<br />
|
|
_:c4 rdf:rest rdf:nil .
|
|
</code></p>
|
|
|
|
<p>Also, RDF imposes no '<a href="#glossWellformed"
|
|
class="termref">well-formedness</a>' conditions on the use of this
|
|
vocabulary, so that it is possible to write RDF graphs which assert
|
|
the existence of highly peculiar objects such as lists with forked
|
|
or non-list tails, or multiple heads:</p>
|
|
|
|
<p><code>_:666 rdf:first <ex:aaa> .<br />
|
|
_:666 rdf:first <ex:bbb> .<br />
|
|
_:666 rdf:rest <ex:ccc> .<br />
|
|
_:666 rdf:rest rdf:nil . </code></p>
|
|
|
|
|
|
<p>It is also possible to write a set of triples which underspecify a collection
|
|
by failing to specify its <code>rdf:rest</code> property value.</p>
|
|
|
|
|
|
<p>Semantic extensions <strong title="MAY in RFC 2119 context" class="RFC2119">MAY</strong>
|
|
place extra syntactic well-formedness restrictions on the use of this vocabulary
|
|
in order to rule out such graphs. They <strong title="MAY in RFC 2119 context" class="RFC2119">MAY</strong>
|
|
exclude interpretations of the collection vocabulary which violate the convention
|
|
that the subject of a 'linked' collection of two-triple items of the form described
|
|
above, ending with an item ending with <code>rdf:nil</code>, denotes a totally
|
|
ordered sequence whose members are the denotations of the <code>rdf:first</code>
|
|
values of the items, in the order got by tracing the <code>rdf:rest</code> properties
|
|
from the subject to <code>rdf:nil</code>. This permits sequences which contain
|
|
other sequences.</p>
|
|
<p >Note that the RDFS semantic conditions, described below, require that any
|
|
subject of the <code>rdf:first</code> property, and any subject or object of
|
|
the <code>rdf:rest</code> property, be of <code>rdf:type rdf:List</code>. </p>
|
|
|
|
|
|
<h4><a name="rdfValue" id="rdfValue"></a>3.3.4 rdf:value</h4>
|
|
<p>The intended use for <code>rdf:value</code> is <a href="http://www.w3.org/TR/rdf-primer/#rdfvalue">explained
|
|
intuitively</a> in the RDF Primer
|
|
document [<cite><a href="#ref-rdf-primer">RDF-PRIMER</a></cite>]. It is typically
|
|
used to identify a 'primary' or 'main' value of a property which has several
|
|
values, or has as its value a complex entity with several facets or properties
|
|
of its own.</p>
|
|
<p>Since the range of possible uses for <code>rdf:value</code> is so wide, it
|
|
is difficult to give a precise statement which covers all the intended meanings
|
|
or use cases. Users are cautioned, therefore, that <span >the
|
|
meaning of <code>rdf:value</code> may vary from application to application</span>.
|
|
In practice, the intended meaning is often clear from the context, but may be
|
|
lost when graphs are merged or when conclusions are inferred.</p>
|
|
|
|
|
|
<h2><a name="rdfs_interp" id="rdfs_interp">4. Interpreting the RDFS Vocabulary</a></h2>
|
|
|
|
|
|
<h3><a name="RDFSINTERP" id="RDFSINTERP">4.1 RDFS Interpretations</a></h3>
|
|
|
|
<p>RDF Schema [<cite><a href="#ref-rdf-vocabulary">RDF-VOCABULARY</a></cite>]
|
|
extends RDF to include a larger <a id="defRDFSV" name="defRDFSV"></a>vocabulary
|
|
rdfsV with more complex semantic constraints:</p>
|
|
|
|
<div class="c1">
|
|
<table border="1" summary="RDFS vocabulary">
|
|
<tbody>
|
|
<tr>
|
|
<td class="othertable"><strong>RDFS vocabulary</strong></td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td class="othertable"><code>rdfs:domain rdfs:range rdfs:Resource rdfs:Literal
|
|
rdfs:Datatype rdfs:Class rdfs:subClassOf rdfs:subPropertyOf
|
|
rdfs:member rdfs:Container rdfs:ContainerMembershipProperty
|
|
rdfs:comment rdfs:seeAlso rdfs:isDefinedBy
|
|
rdfs:label</code></td>
|
|
</tr>
|
|
</tbody>
|
|
</table>
|
|
</div>
|
|
<p>(<code>rdfs:comment</code>,<code> rdfs:seeAlso</code>, <code>rdfs:isDefinedBy</code>
|
|
and <code>rdfs:label</code> are included here because some constraints which
|
|
apply to their use can be stated using <code>rdfs:domain</code>,<code> rdfs:range</code>
|
|
and <code>rdfs:subPropertyOf</code>. Other than this, the formal semantics does
|
|
not assign them any particular meanings.)</p>
|
|
<p>Although not strictly necessary, it is convenient to state the RDFS semantics
|
|
in terms of a new semantic construct, a '<a
|
|
href="#glossClass" class="termref">class</a>', i.e. a resource which represents
|
|
a set of things in the universe which all have that class as the value of their
|
|
<code>rdf:type</code> property. Classes are defined to be things of type <code>rdfs:Class</code>,
|
|
and <span >the set of all classes in an interpretation will be called IC</span>.
|
|
The semantic conditions are stated in terms of a mapping ICEXT (for the <em>C</em>lass
|
|
<em>Ext</em>ension in I) from IC to the set of subsets of IR. The meanings of
|
|
ICEXT and IC in a <a href="#rdfinterpdef" class="termref">rdf-interpretation</a>
|
|
of the RDFS vocabulary are completely defined by the first two conditions in
|
|
the table of RDFS semantic conditions, below. Notice that a class may have an
|
|
empty class extension; that (as <a class="termref" href="#technote">noted</a>
|
|
earlier) two different class entities could have the same class extension; and
|
|
that the class extension of <code>rdfs:Class</code> contains the class <code>rdfs:Class</code>.
|
|
</p>
|
|
|
|
<p><a id="rdfsinterpdef" name="rdfsinterpdef"></a>An <i>rdfs-interpretation</i>
|
|
of V is an <a href="#rdfinterpdef" class="termref">rdf-interpretation</a> I
|
|
<span >of (V union </span><a href="#defRDFV" class="termref">rdfV</a> union
|
|
<a href="#defRDFSV" class="termref">rdfsV)</a> which satisfies the following
|
|
semantic conditions and all the triples in the subsequent table, called the<em>
|
|
RDFS axiomatic triples</em>.</p>
|
|
|
|
<div class="title">RDFS semantic conditions.</div>
|
|
<table border="1">
|
|
<tr>
|
|
|
|
<td class="semantictable"> <p><a name="rdfssemcond1" id="rdfssemcond1"></a>x
|
|
is in ICEXT(y) if and only if <x,y> is in IEXT(I(<code>rdf:type</code>))</p>
|
|
<p>IC = ICEXT(I(<code>rdfs:Class</code>))</p>
|
|
<p>IR = ICEXT(I(<code>rdfs:Resource</code>))</p>
|
|
<p >LV = ICEXT(I(<code>rdfs:Literal</code>)) </p></td>
|
|
</tr>
|
|
<tr>
|
|
|
|
<td class="semantictable"> <p><a name="rdfssemcond2" id="rdfssemcond2"></a>If
|
|
<x,y> is in IEXT(I(<code>rdfs:domain</code>)) and <u,v> is
|
|
in IEXT(x) then u is in ICEXT(y)</p></td>
|
|
</tr>
|
|
<tr>
|
|
|
|
<td class="semantictable"> <p><a name="rdfssemcond3" id="rdfssemcond3"></a>If
|
|
<x,y> is in IEXT(I(<code>rdfs:range</code>)) and <u,v> is
|
|
in IEXT(x) then v is in ICEXT(y)</p></td>
|
|
</tr>
|
|
<tr>
|
|
|
|
<td class="semantictable"><p><a name="rdfssemcond4" id="rdfssemcond4"></a>IEXT(I(<code>rdfs:subPropertyOf</code>))
|
|
is transitive and reflexive on IP</p></td>
|
|
</tr>
|
|
<tr>
|
|
|
|
<td class="semantictable"> <p><a name="rdfssemcond5" id="rdfssemcond5"></a>If
|
|
<x,y> is in IEXT(I(<code>rdfs:subPropertyOf</code>)) then x and
|
|
y are in IP and IEXT(x) is a subset of IEXT(y)</p></td>
|
|
</tr>
|
|
<tr>
|
|
|
|
<td class="semantictable"><p><a name="rdfssemcond6" id="rdfssemcond6"></a>If
|
|
x is in IC then <x, I(<code>rdfs:Resource</code>)> is in IEXT(I(<code>rdfs:subClassOf</code>))</p></td>
|
|
</tr>
|
|
<tr>
|
|
|
|
<td class="semantictable"> <p><a name="rdfssemcond7" id="rdfssemcond7"></a>If
|
|
<x,y> is in IEXT(I(<code>rdfs:subClassOf</code>)) then x and y are
|
|
in IC and ICEXT(x) is a subset of ICEXT(y)</p></td>
|
|
</tr>
|
|
<tr>
|
|
|
|
<td class="semantictable"><p><a name="rdfssemcond8" id="rdfssemcond8"></a>IEXT(I(<code>rdfs:subClassOf</code>))
|
|
is transitive and reflexive on IC</p></td>
|
|
</tr>
|
|
<tr>
|
|
<td class="semantictable"><p><a name="rdfssemcond9" id="rdfssemcond9"></a>If
|
|
x is in ICEXT(I(<code>rdfs:ContainerMembershipProperty</code>)) then:<br />
|
|
< x, I(<code>rdfs:member</code>)> is in IEXT(I(<code>rdfs:subPropertyOf</code>))<br />
|
|
</p></td>
|
|
</tr>
|
|
<tr>
|
|
|
|
<td class="semantictable"><p><a name="rdfssemcond10" id="rdfssemcond10"></a>If
|
|
x is in ICEXT(I(<code>rdfs:Datatype</code>)) then <span ><x,
|
|
I(<code>rdfs:Literal</code>)> is in IEXT(I(<code>rdfs:subClassOf</code>))</span></p></td>
|
|
</tr>
|
|
</table>
|
|
|
|
<p><a id="RDFS_axiomatic_triples" name="RDFS_axiomatic_triples"> </a>
|
|
</p>
|
|
<div class="title">RDFS axiomatic triples.</div>
|
|
<table border="1" summary="RDFS axioms">
|
|
|
|
<tr>
|
|
|
|
|
|
<td class="ruletable"> <code>rdf:type rdfs:domain rdfs:Resource .<br />
|
|
rdfs:domain rdfs:domain rdf:Property .<br />
|
|
rdfs:range rdfs:domain rdf:Property .<br />
|
|
rdfs:subPropertyOf rdfs:domain rdf:Property .<br />
|
|
<a name="axtripleforproof1" id="axtripleforproof1"></a>rdfs:subClassOf rdfs:domain
|
|
rdfs:Class .<br />
|
|
rdf:subject rdfs:domain rdf:Statement .<br />
|
|
rdf:predicate rdfs:domain rdf:Statement .<br />
|
|
rdf:object rdfs:domain rdf:Statement .<br />
|
|
rdfs:member rdfs:domain rdfs:Resource . <br />
|
|
rdf:first rdfs:domain rdf:List .<br />
|
|
rdf:rest rdfs:domain rdf:List .<br />
|
|
rdfs:seeAlso rdfs:domain rdfs:Resource .<br />
|
|
rdfs:isDefinedBy rdfs:domain rdfs:Resource .<br />
|
|
rdfs:comment rdfs:domain rdfs:Resource .<br />
|
|
rdfs:label rdfs:domain rdfs:Resource .<br />
|
|
rdf:value rdfs:domain rdfs:Resource .<br />
|
|
<br />
|
|
rdf:type rdfs:range rdfs:Class .<br />
|
|
rdfs:domain rdfs:range rdfs:Class .<br />
|
|
rdfs:range rdfs:range rdfs:Class .<br />
|
|
rdfs:subPropertyOf rdfs:range rdf:Property .<br />
|
|
<a name="axtripleforproof2" id="axtripleforproof2"></a>rdfs:subClassOf rdfs:range
|
|
rdfs:Class .<br />
|
|
rdf:subject rdfs:range rdfs:Resource .<br />
|
|
rdf:predicate rdfs:range rdfs:Resource .<br />
|
|
rdf:object rdfs:range rdfs:Resource .<br />
|
|
rdfs:member rdfs:range rdfs:Resource .<br />
|
|
rdf:first rdfs:range rdfs:Resource .<br />
|
|
rdf:rest rdfs:range rdf:List .<br />
|
|
rdfs:seeAlso rdfs:range rdfs:Resource .<br />
|
|
rdfs:isDefinedBy rdfs:range rdfs:Resource .<br />
|
|
rdfs:comment rdfs:range rdfs:Literal .<br />
|
|
rdfs:label rdfs:range rdfs:Literal .<br />
|
|
rdf:value rdfs:range rdfs:Resource .<br />
|
|
<br />
|
|
rdf:Alt rdfs:subClassOf rdfs:Container .<br />
|
|
rdf:Bag rdfs:subClassOf rdfs:Container .<br />
|
|
rdf:Seq rdfs:subClassOf rdfs:Container .<br />
|
|
rdfs:ContainerMembershipProperty rdfs:subClassOf rdf:Property .<br />
|
|
<br />
|
|
rdfs:isDefinedBy rdfs:subPropertyOf rdfs:seeAlso .<br />
|
|
<br />
|
|
rdf:XMLLiteral rdf:type rdfs:Datatype .<br />
|
|
rdf:XMLLiteral rdfs:subClassOf rdfs:Literal . <br />
|
|
rdfs:Datatype rdfs:subClassOf rdfs:Class .<br />
|
|
<br />
|
|
rdf:_1 rdf:type rdfs:ContainerMembershipProperty .<br />
|
|
<span >rdf:_1 rdfs:domain rdfs:Resource .<br />
|
|
rdf:_1 rdfs:range rdfs:Resource .</span> <br />
|
|
rdf:_2 rdf:type rdfs:ContainerMembershipProperty .<br />
|
|
rdf:_2 rdfs:domain rdfs:Resource .<br />
|
|
rdf:_2 rdfs:range rdfs:Resource . <br />
|
|
...</code> </td>
|
|
</tr>
|
|
|
|
</table>
|
|
|
|
<p><span >Since I is an <a href="#rdfinterpdef" class="termref">rdf-interpretation</a>, the first condition implies that IP
|
|
= ICEXT(I(<code>rdf:Property</code>)).</span></p>
|
|
<p>These axioms and conditions have some redundancy: for example, all but one
|
|
of the RDF axiomatic triples can be derived from the RDFS axiomatic triples
|
|
and the semantic conditions on ICEXT,<code> rdfs:domain</code> and <code>rdfs:range</code>.
|
|
Other triples which must be true in all <a href="#rdfsinterpdef" class="termref">rdfs-interpretation</a>s
|
|
include the following:</p>
|
|
<div class="title">Some triples which are rdfs-valid.</div>
|
|
<table border="1">
|
|
<tr>
|
|
<td class="ruletable"><code>rdfs:Resource rdf:type rdfs:Class .<br />
|
|
rdfs:Class rdf:type rdfs:Class .<br />
|
|
rdfs:Literal rdf:type rdfs:Class .<br />
|
|
rdf:XMLLiteral rdf:type rdfs:Class .<br />
|
|
rdfs:Datatype rdf:type rdfs:Class .<br />
|
|
rdf:Seq rdf:type rdfs:Class .<br />
|
|
rdf:Bag rdf:type rdfs:Class .<br />
|
|
rdf:Alt rdf:type rdfs:Class .<br />
|
|
rdfs:Container rdf:type rdfs:Class .<br />
|
|
rdf:List rdf:type rdfs:Class .<br />
|
|
rdfs:ContainerMembershipProperty rdf:type rdfs:Class .<br />
|
|
rdf:Property rdf:type rdfs:Class .<br />
|
|
rdf:Statement rdf:type rdfs:Class .<br />
|
|
<br />
|
|
rdfs:domain rdf:type rdf:Property .<br />
|
|
rdfs:range rdf:type rdf:Property .<br />
|
|
rdfs:subPropertyOf rdf:type rdf:Property .<br />
|
|
rdfs:subClassOf rdf:type rdf:Property .<br />
|
|
rdfs:member rdf:type rdf:Property .<br />
|
|
rdfs:seeAlso rdf:type rdf:Property .<br />
|
|
rdfs:isDefinedBy rdf:type rdf:Property .<br />
|
|
rdfs:comment rdf:type rdf:Property .<br />
|
|
rdfs:label rdf:type rdf:Property .<br />
|
|
</code><code></code></td>
|
|
</tr>
|
|
</table>
|
|
|
|
<p><br />
|
|
Note that <a href="#defDatatype" class="termref">datatype</a>s are allowed to
|
|
have class extensions, i.e. are considered to be classes, in RDFS. As illustrated
|
|
by the semantic condition on the class extension of <code>rdf:XMLLiteral</code>,
|
|
the members of a datatype class are the values of the <a href="#defDatatype" class="termref">datatype</a>.
|
|
This is explained in more detail in <a href="#dtype_interp" >section 5</a> below.
|
|
<span >The class <code>rdfs:Literal</code> contains all literal values; however,
|
|
typed literals whose strings do not conform to the lexical requirements of their
|
|
<a href="#defDatatype" class="termref">datatype</a> are required to have meanings
|
|
not in this class. The semantic conditions on <a href="#rdfinterpdef" class="termref">rdf-interpretation</a>s
|
|
imply that ICEXT(I(<code>rdf:XMLLiteral</code>)) contains all XML values of
|
|
well-typed XML literals.</span></p>
|
|
<p >The conditions on <code>rdf:XMLLiteral</code> and <code>rdfs:range</code>
|
|
taken together make it possible to write a contradictory statement in RDFS,
|
|
by asserting that a property value must be in the class <code>rdf:XMLLiteral</code>
|
|
but applying this property with a value which is an ill-formed XML literal,
|
|
and therefore required to not be in that class: for example</p>
|
|
<p ><code><ex:a> <ex:p> "<notLegalXML"^^rdf:XMLLiteral
|
|
.<br />
|
|
<ex:p> rdfs:range rdf:XMLLiteral .</code></p>
|
|
<p >cannot be true in any rdfs-interpretation; it is <em>rdfs-<a href="#glossInconsistent" class="termref">inconsistent</a></em>.</p>
|
|
<h3><a name="ExtensionalDomRang" id="ExtensionalDomRang"></a>4.2 Extensional Semantic
|
|
Conditions (Informative)</h3>
|
|
<p>The semantics given above is deliberately chosen to be the weakest 'reasonable'
|
|
interpretation of the RDFS vocabulary. Semantic extensions <strong title="MAY in RFC 2119 context" class="RFC2119">MAY</strong>
|
|
strengthen the range, domain, subclass and subproperty semantic conditions to
|
|
the following '<a class="termref" href="#glossExtensional">extensional</a>'
|
|
versions:</p>
|
|
<div class="title">Extensional alternatives for some RDFS semantic conditions.</div>
|
|
<table summary="range and domain extension conditions" border="1">
|
|
<tr>
|
|
<td class="semantictable"> <p><x,y> is in IEXT(I(<code>rdfs:subClassOf</code>))
|
|
if and only if x and y are in IC and ICEXT(x) is a subset of ICEXT(y)</p></td>
|
|
</tr>
|
|
<tr>
|
|
<td class="semantictable"> <p><x,y> is in IEXT(I(<code>rdfs:subPropertyOf</code>))
|
|
if and only if x and y are in IP and IEXT(x) is a subset of IEXT(y)</p></td>
|
|
</tr>
|
|
<tr>
|
|
<td class="semantictable"> <p><x,y> is in IEXT(I(<code>rdfs:range</code>))
|
|
if and only if (if <u,v> is in IEXT(x) then v is in ICEXT(y))</p></td>
|
|
</tr>
|
|
<tr>
|
|
<td class="semantictable"> <p><x,y> is in IEXT(I(<code>rdfs:domain</code>))
|
|
if and only if (if <u,v> is in IEXT(x) then u is in ICEXT(y))</p></td>
|
|
</tr>
|
|
</table>
|
|
<p>which would guarantee that the subproperty and subclass properties were transitive
|
|
and reflexive, but would also have further consequences. </p>
|
|
<p>These stronger conditions would be trivially satisfied when properties are
|
|
identified with property extensions, classes with class extensions, and <code>rdfs:SubClassOf</code>
|
|
understood to mean subset, and hence would be satisfied by an <a href="#glossExtensional" class="termref">extensional</a> semantics
|
|
for RDFS. In some ways the extensional versions provide a simpler semantics,
|
|
but they require more complex inference rules. The 'intensional' semantics described
|
|
in the main text provides for most common uses of subclass and subproperty assertions,
|
|
and allows for simpler implementations of a <a href="#glossComplete" class="termref">
|
|
complete</a> set of RDFS entailment rules, described in <a href="#RDFSRules" class="termref"> section 7.3</a>.</p>
|
|
<h3><a name="literalnote" id="literalnote">4.3 A Note on rdfs:Literal</a> </h3>
|
|
|
|
|
|
<p>Although the semantic conditions on <a href="#rdfsinterpdef" class="termref">rdfs-interpretation</a>s include the intuitively
|
|
sensible condition that ICEXT(I(<code>rdfs:Literal</code>)) must be the set
|
|
LV, there is no way to impose this condition by any RDF assertion or inference
|
|
rule. This limitation is due to the fact that RDF does not allow literals to
|
|
occur in the subject position of a triple, so there are severe restrictions
|
|
on what can be said <i>about</i> literals in RDF. Similarly, while properties
|
|
may be asserted of the class <code>rdfs:Literal</code>, none of these can be
|
|
validly transferred to literals themselves.</p>
|
|
|
|
<p>For example, a triple of the form</p>
|
|
|
|
<p><code><ex:a> rdf:type rdfs:Literal .</code></p>
|
|
|
|
<p>is consistent even though '<code>ex:a</code>' is a URI reference rather
|
|
than a literal. What it says is that I(<code>ex:a</code>) is a
|
|
literal value, ie that the URI reference '<code>ex:a</code>'
|
|
<i>denotes</i> a literal value. It does not specify exactly which
|
|
literal value it denotes.</p>
|
|
|
|
|
|
<p>The semantic conditions guarantee that any triple containing a plain literal
|
|
object entails a similar triple with a blank node as object:</p>
|
|
|
|
<p><code><ex:a> <ex:b> "10"</code> .</p>
|
|
|
|
<p>entails</p>
|
|
|
|
|
|
<p><code><ex:a> <ex:b> _:xxx .</code></p>
|
|
<p>This means that the literal denotes an entity, which could therefore also be
|
|
named, at least in principle, by a URI reference.</p>
|
|
<h3><a name="rdfs_entailment" id="rdfs_entailment"></a>4.4 RDFS Entailment</h3>
|
|
<p>S <i>rdfs-entails</i> E when every <a href="#rdfsinterpdef" class="termref">rdfs-interpretation</a>
|
|
which satisfies every member of S also satisfies E. This follows the wording
|
|
of the definition of <a href="#defentail" class="termref">simple entailment</a>
|
|
in <a href="#entail" class="termref"> Section 2</a>, but refers only to <a href="#rdfsinterpdef" class="termref">rdfs-interpretation</a>s
|
|
instead of all simple interpretations. <span >Rdfs-entailment is an example
|
|
of <a href="#vocabulary_entail" class="termref">vocabulary entailment</a>.</span>
|
|
</p>
|
|
<p> Since every <a href="#rdfsinterpdef" class="termref">rdfs-interpretation</a> is an <a href="#rdfinterpdef" class="termref">rdf-interpretation</a>, if S rdfs-entails
|
|
E then it rdf-entails E; but rdfs-entailment is stronger than rdf-entailment.
|
|
Even the empty graph has a large number of rdfs-entailments which are not rdf-entailments,
|
|
for example all triples of the form </p>
|
|
<p>xxx <code>rdf:type rdfs:Resource .</code></p>
|
|
<p>are true in all <a href="#rdfsinterpdef" class="termref">rdfs-interpretation</a>s
|
|
of any vocabulary containing the URI reference xxx.</p>
|
|
<p >An rdfs-inconsistent graph rdfs-entails any graph, by the
|
|
definition of entailment; such 'trivial entailments' by an inconsistent set
|
|
are not usually considered useful inferences to draw in practice, however. </p>
|
|
|
|
<h2><a name="dtype_interp" id="dtype_interp">5. Interpreting Datatypes</a></h2>
|
|
<h3><a name="DTYPEINTERP" id="DTYPEINTERP">5.1 Datatyped Interpretations</a></h3>
|
|
|
|
<p >RDF provides for the use of externally defined <a href="#defDatatype" class="termref">datatype</a>s
|
|
identified by a particular URI reference. In the interests of generality, RDF imposes
|
|
minimal conditions on a datatype. It also includes a single built-in datatype
|
|
<code>rdf:XMLLiteral.</code></p>
|
|
<p>This semantics for datatypes is minimal. It makes no provision for associating
|
|
a datatype with a property so that it applies to all values of the property,
|
|
and does not provide any way of explicitly asserting that
|
|
a blank node denotes a particular datatype value. Semantic
|
|
extensions and future versions of RDF may impose more elaborate datatyping
|
|
conditions. Semantic extensions may also refer to other kinds of information
|
|
about a datatype, such as orderings of the value space.</p>
|
|
<p > <a name="defDatatype" id="defDatatype"></a>A <a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#section-Datatypes">datatype</a>
|
|
is an entity characterized by a set of character strings called <em>lexical
|
|
forms</em> and a mapping from that set to a set of <em>values</em>. Exactly
|
|
how these sets <span >and mappings</span> are defined is a matter external to
|
|
RDF. </p>
|
|
|
|
<p >Formally, a datatype d is defined by three items:</p>
|
|
|
|
<p >1. a non-empty set of character strings called the <em>lexical space</em>
|
|
of d;</p>
|
|
|
|
<p >2. a non-empty set called the <em>value space</em> of d;</p>
|
|
<p >3. a mapping from the lexical space of d to the value space of d, called the
|
|
<em>lexical-to-value mapping</em> of d.</p>
|
|
<p >The lexical-to-value mapping of a datatype d is written as
|
|
L2V(d).</p>
|
|
<p>In stating the semantics we assume that interpretations are relativized
|
|
to a particular set of datatypes each of which is identified by a
|
|
URI reference. </p>
|
|
<p><a name="defDatatypeMap" id="defDatatypeMap"></a>Formally, let D be a set of
|
|
pairs consisting of a URI reference and a <a href="#defDatatype" class="termref">datatype</a>
|
|
such that no URI reference appears twice in the set, so that D can be regarded
|
|
as a function from a set of URI references to a set of datatypes: call this
|
|
a <em>datatype map</em>. (The particular URI references must be mentioned explicitly
|
|
in order to ensure that interpretations conform to any naming conventions imposed
|
|
by the external authority responsible for defining the datatypes.) Every <a href="#defDatatypeMap" class="termref">datatype
|
|
map</a> is understood to contain <<code>rdf:XMLLiteral</code>, x> where
|
|
x is the built-in XML Literal datatype whose lexical and value spaces and lexical-to-value
|
|
mapping are <span ><a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/#dfn-rdf-XMLLiteral">defined</a>
|
|
in the <a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/"> RDF Concepts and Abstract
|
|
Syntax</a> document [<cite><a href="#ref-rdf-concepts">RDF-CONCEPTS</a></cite>].
|
|
</span></p>
|
|
<p>The <a href="#defDatatypeMap" class="termref">datatype map</a> which also contains
|
|
the set of all pairs of the form <<code>http://www.w3.org/2001/XMLSchema#</code><i>sss</i>,
|
|
<em>sss</em>>, where <em>sss</em> is a built-in datatype named <em>sss</em>
|
|
in <a href="http://www.w3.org/TR/xmlschema-2/">XML Schema Part 2: Datatypes</a>
|
|
[<cite><a
|
|
href="#ref-xmls">XML-SCHEMA2</a></cite>] <span >and listed in the following
|
|
table</span>, is referred to here as XSD. <a name="XSDtable" id="XSDtable"></a></p>
|
|
<table border="1">
|
|
<tr>
|
|
<td class="ruletable"><strong>XSD datatypes</strong></td>
|
|
</tr>
|
|
<tr>
|
|
<td class="ruletable"><a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#string"><code>xsd:string</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#boolean"><code>xsd:boolean</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#decimal"><code>xsd:decimal</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#float"><code>xsd:float</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#double"><code>xsd:double</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#dateTime"><code>xsd:dateTime</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#time"><code>xsd:time</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#date"><code>xsd:date</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#gYearMonth"><code>xsd:gYearMonth</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#gYear"><code>xsd:gYear</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#gMonthDay"><code>xsd:gMonthDay</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#gDay"><code>xsd:gDay</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#gMonth"><code>xsd:gMonth</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#hexBinary"><code>xsd:hexBinary</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#base64Binary"><code>xsd:base64Binary</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#anyURI"><code>xsd:anyURI</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#normalizedString"><code>xsd:normalizedString</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#token"><code>xsd:token</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#language"><code>xsd:language</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#NMTOKEN"><code>xsd:NMTOKEN</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#Name"><code>xsd:Name</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#NCName"><code>xsd:NCName</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#integer"><code>xsd:integer</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#nonPositiveInteger"><code>xsd:nonPositiveInteger</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#negativeInteger"><code>xsd:negativeInteger</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#long"><code>xsd:long</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#int"><code>xsd:int</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#short"><code>xsd:short</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#byte"><code>xsd:byte</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#nonNegativeInteger"><code>xsd:nonNegativeInteger</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#unsignedLong"><code>xsd:unsignedLong</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#unsignedInt"><code>xsd:unsignedInt</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#unsignedShort"><code>xsd:unsignedShort</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#unsignedByte"><code>xsd:unsignedByte</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#positiveInteger"><code>xsd:positiveInteger</code></a>
|
|
</td>
|
|
</tr>
|
|
</table>
|
|
<p >The other built-in XML Schema datatypes are unsuitable for various reasons,
|
|
and <strong title="SHOULD NOT in RFC 2119 context" class="RFC2119">SHOULD NOT</strong>
|
|
be used: <a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#duration"><code>xsd:duration</code></a>
|
|
does not have a well-defined value space (this may be corrected in later revisions
|
|
of XML Schema datatypes, in which case the revised datatype would be suitable
|
|
for use in RDF datatyping); <a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#QName"><code>xsd:QName</code></a>
|
|
and <a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#ENTITY"><code>xsd:ENTITY</code></a>
|
|
require an enclosing XML document context; <a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#ID"><code>xsd:ID</code></a>
|
|
and <a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#IDREF"><code>xsd:IDREF</code></a>
|
|
are for cross references within an XML document; <a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#NOTATION"><code>xsd:NOTATION</code></a>
|
|
is not intended for direct use; <a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#IDREFS"><code>xsd:IDREFS</code></a>,
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#ENTITIES"><code>xsd:ENTITIES</code></a>
|
|
and <a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#NMTOKENS"><code>xsd:NMTOKENS</code></a>
|
|
are sequence-valued datatypes which do not fit the RDF <a href="#defDatatype" class="termref">datatype</a>
|
|
model.</p>
|
|
<p><a name="defDinterp"></a>If D is a <a href="#defDatatypeMap" class="termref">datatype
|
|
map</a>, a <em>D-interpretation</em> of a vocabulary V is any <a href="#rdfsinterpdef" class="termref">rdfs-interpretation</a>
|
|
I of V union {aaa: < aaa, x > in D for some x } which satisfies the following extra conditions for every pair < aaa,
|
|
x > in D:</p>
|
|
<div class="title">General semantic conditions for datatypes.</div>
|
|
<table border="1" class="semantictable" summary="datatype semantic conditions">
|
|
<tr>
|
|
<td>if <aaa,x> is in D then I(aaa) = x </td>
|
|
</tr>
|
|
<tr>
|
|
<td>if <aaa,x> is in D then ICEXT(x) is the value space of x and is
|
|
a subset of LV</td>
|
|
</tr>
|
|
<tr>
|
|
<td >if <aaa,x> is in D then for any typed literal "sss"^^ddd
|
|
in V with I(ddd) = x , <em><br />
|
|
</em> if sss is in the lexical space of x then IL("sss"^^ddd)
|
|
= L2V(x)(sss), otherwise IL("sss"^^ddd) is not in LV</td>
|
|
</tr>
|
|
<tr>
|
|
<td >if <aaa,x> is in D then I(aaa) is in ICEXT(I(<code>rdfs:Datatype</code>))</td>
|
|
</tr>
|
|
</table>
|
|
<p>The first condition ensures that I interprets the URI reference according to
|
|
the <a href="#defDatatypeMap" class="termref">datatype map</a> provided. Note that this does not prevent other URI references
|
|
from also denoting the <a href="#defDatatype" class="termref">datatype</a>. </p>
|
|
|
|
<p>The second condition ensures that the datatype URI reference, when used as
|
|
a class name, refers to the value space of the <a href="#defDatatype" class="termref">datatype</a>,
|
|
and that all elements of a value space must be literal values.</p>
|
|
|
|
<p>The third condition ensures that typed literals in the vocabulary respect
|
|
the datatype lexical-to-value mapping. For example, if I is an XSD-interpretation
|
|
then I("15"^^<code>xsd:decimal</code>)
|
|
must be the number fifteen. <a name="illformedliteral" id="illformedliteral"></a>The
|
|
condition also requires that an <em>ill-typed</em> literal, where the literal
|
|
string is not in the lexical space of the <a href="#defDatatype" class="termref">datatype</a>,
|
|
not denote any literal value. Intuitively, such a name does not denote
|
|
any value, but in order to avoid the semantic complexities which arise
|
|
from empty names, the semantics requires such a typed literal to denote
|
|
an 'arbitrary' non-literal value. Thus for example, if I is an XSD-interpretation,
|
|
then all that can be concluded about I("arthur"^^<code>xsd:decimal</code>)
|
|
is that it is not in LV, i.e. not in ICEXT(I(<code>rdfs:Literal</code>)). <span >An
|
|
ill-typed literal does not in itself constitute an inconsistency, but
|
|
a graph which entails that an ill-typed literal has <code>rdf:type rdfs:Literal</code>, <span >or
|
|
that an ill-typed XML literal has <code>rdf:type rdf:XMLLiteral</code>, </span>would
|
|
be inconsistent.</span></p>
|
|
<p>Note that this third condition applies only to <a href="#defDatatype" class="termref">datatype</a>s
|
|
in the range of D. Typed literals whose type is not in the <a href="#defDatatypeMap" class="termref">datatype
|
|
map</a> of the interpretation are treated as before, i.e. as denoting some unknown
|
|
thing. The condition does not require that the URI reference in the typed literal
|
|
be the same as the associated URI reference of the <a href="#defDatatype" class="termref">datatype</a>;
|
|
this allows semantic extensions which can express identity conditions on URI
|
|
references to draw appropriate conclusions.</p>
|
|
|
|
<p>The fourth condition ensures that the class <code>rdfs:Datatype</code> contains
|
|
the <a href="#defDatatype" class="termref">datatype</a>s used in any satisfying
|
|
<a href="#defDinterp" class="termref">D-interpretation</a>. Notice that this
|
|
is a necessary, but not a sufficient, condition; it allows the class I(<code>rdfs:Datatype</code>)
|
|
to contain other <a href="#defDatatype" class="termref">datatype</a>s. </p>
|
|
|
|
<p><a name="pfps8L1" id="pfps8L1"></a>The semantic conditions for <a href="#rdfinterpdef" class="termref">rdf-interpretation</a>s
|
|
impose the correct interpretation on literals typed by <code>'rdf:XMLLiteral'</code>.
|
|
However, a D-interpretation recognizes the <a href="#defDatatype" class="termref">datatype</a> to exist as an entity,
|
|
rather than simply being a semantic condition imposed on the RDF typed
|
|
literal syntax. Semantic extensions which can express identity conditions
|
|
on resources could therefore draw stronger conclusions from <a href="#defDinterp" class="termref">D-interpretation</a>s
|
|
than from <a href="#rdfsinterpdef" class="termref">rdfs-interpretation</a>s. </p>
|
|
<p ><a name="defdatatypeclash" id="defdatatypeclash"></a>If the <a href="#defDatatype" class="termref">datatype</a>s
|
|
in the datatype map D impose disjointness conditions on their value spaces,
|
|
it is possible for an RDF graph to have no <a href="#defDinterp" class="termref">D-interpretation</a>
|
|
which satisfies it. For example, XML Schema defines the value spaces of <code>xsd:string</code>
|
|
and <code>xsd:decimal</code> to be disjoint, so it is impossible to construct
|
|
a XSD-interpretation <a href="#glossSatisfy" class="termref">satisfying</a>
|
|
the graph</p>
|
|
<p><code><ex:a> <ex:b> "25"^^xsd:decimal .<br />
|
|
<ex:b> rdfs:range xsd:string .</code></p>
|
|
<p>This situation could be characterized by saying that the graph is XSD-inconsistent,
|
|
or more generally as a <em>datatype clash</em>. Note that it is possible to
|
|
construct a <a
|
|
href="#glossSatisfy" class="termref">satisfying</a> <a href="#rdfsinterpdef" class="termref">rdfs-interpretation</a>
|
|
for this graph, but it would violate the XSD conditions, since the class extensions
|
|
of I(<code>xsd:decimal</code>) and I(<code>xsd:string</code>) would have a nonempty
|
|
intersection.</p>
|
|
<p>Datatype clashes can arise in several other ways. For example, any assertion
|
|
that something is in both of two disjoint dataype classes:</p>
|
|
<p><code>_:x rdf:type xsd:string .<br />
|
|
_:x rdf:type xsd:decimal .</code></p>
|
|
<p>or that a property with an 'impossible' range has a value:</p>
|
|
<p><code><ex:p> rdfs:range xsd:string .<br />
|
|
<ex:p> rdfs:range xsd:decimal .<br />
|
|
_:x <ex:p> _:y .</code></p>
|
|
<p>would constitute a datatype clash. A datatype clash may also arise from the
|
|
use of a particular lexical form, for example:</p>
|
|
<p><code><ex:a> <ex:p> "2.5"^^xsd:decimal .<br />
|
|
<ex:p> rdfs:range xsd:integer .</code></p>
|
|
<p>or by the use of an ill-typed lexical form:</p>
|
|
<p><code><ex:a> <ex:p> "abc"^^xsd:integer .<br />
|
|
<ex:p> rdfs:range xsd:integer .</code></p>
|
|
<p>Datatype clashes are the only <a
|
|
href="#glossInconsistent" class="termref">inconsistencies</a> recognized by
|
|
this <a
|
|
href="#glossModeltheory" class="termref">model theory</a>; note however that
|
|
datatype clashes involving XML literals can arise in RDFS.</p>
|
|
<p><span >If D is a subset of D', then restricting interpretations
|
|
of a graph to D'-interpretations amounts to a semantic extension compared
|
|
to the same restriction with respect to D. In effect, the extension of
|
|
the <a href="#defDatatypeMap" class="termref">datatype map</a> makes implicit assertions about typed literals, by requiring
|
|
them
|
|
to denote entities in the value space of a <a href="#defDatatype" class="termref">datatype</a>. The extra semantic
|
|
constraints associated with the larger <a href="#defDatatypeMap" class="termref">datatype map</a> will force interpretations
|
|
to make more triples true, but they may also reveal datatype clashes
|
|
and violations, so that a D-consistent graph could be D'-inconsistent. </span></p>
|
|
<p >Say that an RDF graph <em>recognizes</em> a datatype
|
|
URI reference aaa when the graph rdfs-entails a <em>datatyping triple</em> of the form</p>
|
|
<p >aaa<code> rdf:type rdfs:Datatype .</code></p>
|
|
<p > The semantic conditions for <a href="#rdfsinterpdef" class="termref">rdfs-interpretation</a>s
|
|
require the built-in datatype URI reference <code>'rdf:XMLLiteral'</code> to
|
|
be recognized.</p>
|
|
|
|
<p >If every recognized URI reference in a graph is the name of a known <a href="#defDatatype" class="termref">datatype</a>,
|
|
then there is a natural <a href="#defDatatypeMap" class="termref">datatype map</a>
|
|
DG which pairs each recognized URI reference to that known datatype (and '<code>rdf:XMLLiteral</code>'
|
|
to <code>rdf:XMLLiteral</code>). Any <a href="#rdfsinterpdef" class="termref">rdfs-interpretation</a>
|
|
I of that graph then has a corresponding 'natural' DG-interpretation which is
|
|
like I except that I(aaa) is the appropriate <a href="#defDatatype" class="termref">datatype</a>
|
|
and the class extension of <code>rdfs:Datatype</code> is modified appropriately.
|
|
Applications <strong class="RFC2119" title="MAY in RFC2119 sense">MAY</strong>
|
|
require that RDF graphs be interpreted by <a href="#defDinterp" class="termref">D-interpretation</a>s
|
|
where D contains a natural datatype map of the graph. This amounts to treating
|
|
datatyping triples as 'declarations' of <a href="#defDatatype" class="termref">datatype</a>s
|
|
by the graph, and making the fourth semantic condition into an 'iff' condition.
|
|
Note however that a datatyping triple does not in itself provide the information
|
|
necessary to check that a graph satisfies the other datatype semantic conditions,
|
|
and it does not formally rule out other interpretations, so that adopting this
|
|
requirement as a formal entailment principle would violate the <a href="#GeneralMonotonicityLemma" class="termref">general
|
|
monotonicity lemma</a> described in <a href="#MonSemExt" class="termref">section
|
|
6</a>, below.</p>
|
|
<h3 ><a name="D_entailment" id="D_entailment"></a>5.2 D-entailment</h3>
|
|
<p >S <em>D-entails</em> E when every <a href="#defDinterp" class="termref">D-interpretation</a>
|
|
which satisfies every member of S also satisfies E. This follows the wording
|
|
of the definition of <a href="#defentail" class="termref">simple entailment</a>
|
|
in <a href="#entail" class="termref"> Section 2</a>, but refers only to <a href="#defDinterp" class="termref">D-interpretation</a>s
|
|
instead of all simple interpretations.<span > D-entailment is an example of
|
|
<a href="#vocabulary_entail" class="termref">vocabulary entailment</a>.</span>
|
|
</p>
|
|
<p >As noted above, it is
|
|
possible that a graph which is consistent in one vocabulary becomes inconsistent
|
|
in a semantic extension defined on a larger vocabulary, and <a href="#defDinterp" class="termref">D-interpretation</a>s
|
|
allow for inconsistencies in an RDF graph. The definition of <a href="#vocabulary_entail" class="termref">vocabulary entailment</a>
|
|
means that an inconsistent graph will entail <em>any</em> graph in the stronger
|
|
vocabulary entailment. For example, a D-inconsistent graph <a href="#D_entailment" class="termref"> D-entail</a>s any RDF
|
|
graph. However, it will usually not be appropriate to consider such 'trivial'
|
|
entailments as useful consequences, since they may not be <a href="#glossValid"
|
|
class="termref">valid</a> entailments in a smaller vocabulary. </p>
|
|
<h2><a name="MonSemExt" id="MonSemExt"></a>6. Monotonicity of semantic extensions
|
|
</h2>
|
|
<p>Given a set of RDF graphs, there are various ways in which one can 'add' information
|
|
to it. Any of the graphs may have some triples added to it; the set of graphs
|
|
may be extended by extra graphs; or the vocabulary of the graph may be interpreted
|
|
relative to a stronger notion of <a href="#vocabulary_entail" class="termref">vocabulary entailment</a>, i.e. with a larger set
|
|
of semantic conditions understood to be imposed on the interpretations. All
|
|
of these can be thought of as an addition of information, and may make more
|
|
entailments hold than held before the change. All of these additions are <a href="#glossMonotonic" class="termref"><em>monotonic</em></a>,
|
|
in the sense that entailments which hold before the addition of information,
|
|
also hold after it. We can sum up this in a single lemma:</p>
|
|
<p ><strong><a name="GeneralMonotonicityLemma" id="GeneralMonotonicityLemma"></a>General monotonicity lemma</strong>. Suppose
|
|
that S, S' are sets of RDF graphs with every member of S a subset
|
|
of some member of S'. Suppose that Y indicates a semantic extension
|
|
of X, S X-entails E, and S and
|
|
E satisfy any syntactic restrictions of Y. Then S' Y-entails E.</p>
|
|
|
|
<p >In particular, if D' is a <a href="#defDatatypeMap" class="termref">datatype map</a>, D a subset of D' and if S <a href="#D_entailment" class="termref"> D-entail</a>s
|
|
E then S also D'-entails E. </p>
|
|
<h2><span ><a name="rules" id="rules"></a></span>7. Entailment
|
|
rules (Informative)</h2>
|
|
<p>The following tables list some inference patterns which capture some of the
|
|
various forms of vocabulary entailment, and could be used as a guide for the
|
|
design of software to check RDF graphs for RDF and RDFS entailment. Implementations
|
|
may be based on applying the rules forwards, or treating the conclusion as a
|
|
pattern to be recognized in the consequent of a proposed entailment and searching
|
|
backwards for an appropriate match with other rule conclusions or the proposed
|
|
antecedent. Other strategies are also possible.</p>
|
|
<p>The rules are all stated with the form <em>add a triple to a graph when it
|
|
contains triples conforming to a pattern</em>, and they are all <a name="validrule" id="validrule"></a><a href="#glossValid" class="termref"><em>valid</em></a>
|
|
in the following sense: a graph entails (in the appropriate sense listed) any
|
|
larger graph that is obtained by applying the rules to the original graph. Notice
|
|
that applying such a rule to a graph amounts to forming a simple union with
|
|
the conclusion, rather than a <a href="#defmerge" class="termref">merge</a>,
|
|
and hence preserves any blank nodes already in the graph. </p>
|
|
<p>These rules all use the following conventions: aaa, bbb, etc., stand for any
|
|
URI reference, i.e. any possible predicate of a triple; uuu, vvv, etc. for any
|
|
URI reference or blank node identifier, i.e any possible subject of a triple;
|
|
xxx, yyy etc. for any URI reference, blank node identifier or literal, i.e.
|
|
any possible subject or object of a triple; lll for any literal; and _:nnn,
|
|
etc., for blank node identifiers.</p>
|
|
<h3 ><a name="simpleRules" id="simpleRules"></a>7.1 Simple Entailment Rules</h3>
|
|
<p >The <a href="#interplemma" class="termref">interpolation lemma</a> in <a href="#entail" class="termref">Section
|
|
2</a> can be characterized by the following entailment rules which generate
|
|
generalizations, i.e. graphs which have the original graph as an instance.
|
|
Being a subgraph requires no explicit formulation as an inference rule
|
|
on triples.</p>
|
|
<div class="title">simple entailment rules.</div>
|
|
<table border="1" summary="inference rules for existence">
|
|
<tr class="ruletable">
|
|
<td ><strong>Rule name</strong></td>
|
|
<td ><strong>If E contains</strong></td>
|
|
<td ><strong>then add</strong></td>
|
|
</tr>
|
|
<tr>
|
|
<td class="ruletable"><a name="rulese1" id="rulese1"></a>se1</td>
|
|
<td class="ruletable">uuu aaa xxx<code> .</code></td>
|
|
<td class="ruletable"><p>uuu aaa<code> _:</code>nnn<code> .</code></p>
|
|
where <code>_:</code>nnn identifies a blank node <a href="#defallocated" class="termref">allocated</a> to xxx by rule
|
|
se1 or se2.</td>
|
|
</tr>
|
|
<tr>
|
|
<td class="ruletable" ><a name="rulese2" id="rulese2"></a>se2</td>
|
|
<td class="ruletable" >uuu aaa xxx<code> .</code></td>
|
|
<td class="ruletable" ><p><code>_:</code>nnn aaa xxx<code> .</code></p>
|
|
where <code>_:</code>nnn identifies a blank node <a href="#defallocated" class="termref">allocated</a> to uuu by rule
|
|
se1 or se2.</td>
|
|
</tr>
|
|
</table>
|
|
<p ><a name="defallocated" id="defallocated"></a>The terminology 'allocated
|
|
to' means that the blank node must have been created by an earlier application
|
|
of the specified rules on the same URI reference, blank node or literal, or
|
|
if there is no such blank node then it must be a 'new' node which does not occur
|
|
in the graph. This rather complicated condition ensures that the resulting graph,
|
|
obtained by adding the new blank-node triples, has the original graph as a proper
|
|
instance and that any such graph will have a subgraph which is the same as one
|
|
which can be generated by these rules. For example, the graph</p>
|
|
<p ><code><ex:a> <ex:p> <ex:b> .<br />
|
|
<ex:c> <ex:q> <ex:a> .</code></p>
|
|
<p >could be expanded as follows</p>
|
|
<p ><code>_:x <ex:p> <ex:b> . </code>by se1 using a new <code>_:x</code>
|
|
which is <a href="#defallocated" class="termref">allocated</a> to <code>ex:a<br />
|
|
<ex:c> <ex:q> _:x . </code>by se2 using the same <code>_:x </code>allocated
|
|
to <code>ex:a<br />
|
|
_:x <ex:p> _:y . </code> by se2 using a new <code>_:y</code> which is <a href="#defallocated" class="termref">allocated</a> to <code>ex:b</code></p>
|
|
<p >but it would not be correct to infer</p>
|
|
<p >** <code>_:x <ex:q> <ex:a> .</code> ** by se2 (** since<code>
|
|
_:x</code> is not <a href="#defallocated" class="termref">allocated</a> to <code>ex:c</code> )</p>
|
|
<p >These rules allow blank nodes to proliferate, producing highly non-<a href="#deflean" class="termref">lean</a>
|
|
graphs; they sanction entailments such as</p>
|
|
<p><code><ex:a> <ex:p> <ex:b> .<br />
|
|
</code><code><ex:a> <ex:p> _:x .</code> by xse1 with _:x <a href="#defallocated" class="termref">allocated</a> to ex:b<br />
|
|
<code><ex:a> <ex:p> _:y . </code>by xse1 with _:y <a href="#defallocated" class="termref">allocated</a> to _:x<br />
|
|
<code>_:z <ex:p> _:y . </code>by xse2 with _:z <a href="#defallocated" class="termref">allocated</a> to ex:a <br />
|
|
<code>_:u <ex:p> _:y .</code> by xse2 with _:u <a href="#defallocated" class="termref">allocated</a> to _:z<br />
|
|
<code>_:u <ex:p> _:v .</code> by xse1 with _:v <a href="#defallocated" class="termref">allocated</a> to _:y </p>
|
|
<p>It is easy to see that S is an instance of E if and only if one can derive
|
|
E from S by applying these rules in a suitable sequence; the rule applications
|
|
required can be discovered by examination of the instance mapping. So, by the
|
|
interpolation lemma, S simply entails E iff one can derive (a graph containing)
|
|
E from S by the application of these rules. However, it is also clear that applying
|
|
these rules naively would not result in an efficient search process, since the
|
|
rules will not terminate and can produce arbitrarily many redundant derivations
|
|
of equivalent triples. </p>
|
|
<p>The general problem of determining simple entailment between arbitrary RDF
|
|
graphs is decideable but NP-complete. This can be shown by encoding the problem
|
|
of detecting a subgraph of an arbitrary directed graph as an RDF entailment,
|
|
using only blank nodes to represent the graph (observation due to Jeremy Carroll.)</p>
|
|
<p>Subsequent rule sets for detecting RDF and RDFS entailment use a special case
|
|
of rule se1 which applies only to literals:</p>
|
|
<div class="title"> literal generalization rule.</div>
|
|
<table border="1" summary="inference rule connecting literals to blank nodes">
|
|
<tr class="ruletable">
|
|
<td ><strong>Rule Name</strong></td>
|
|
<td ><strong>If E contains</strong></td>
|
|
<td ><strong>then add</strong></td>
|
|
</tr>
|
|
<tr>
|
|
<td class="ruletable"><a name="ruleslg" id="ruleslg"></a>lg</td>
|
|
<td class="ruletable"><p>uuu aaa lll<code> .</code> </p>
|
|
|
|
</td>
|
|
<td class="ruletable"><p>uuu aaa<code> _:</code>nnn<code> .</code></p>
|
|
where <code>_:</code>nnn identifies a blank node <a href="#defallocated" class="termref">allocated</a> to the literal
|
|
lll by this rule.</td>
|
|
</tr>
|
|
</table>
|
|
<p>Note that this rule is just sufficient to reproduce any subgraph of E consisting
|
|
of triples all containing a given literal as an isomorphic subgraph in which
|
|
the literal is replaced by a unique blank node. The significance of this lies
|
|
in the fact the blank nodes can stand in a subject position in an RDF triple,
|
|
allowing conclusions to be drawn by the other rules which express properties
|
|
of the literal value denoted by that literal.</p>
|
|
<p>For RDFS entailment one additional rule is required, which inverts rule
|
|
lg: </p>
|
|
<div class="title"> literal instantiation rule.</div>
|
|
<table border="1" summary="inference rule connecting blank node to literal">
|
|
<tr class="ruletable">
|
|
<td ><strong>Rule Name</strong></td>
|
|
<td ><strong>If E contains</strong></td>
|
|
<td ><strong>then add</strong></td>
|
|
</tr>
|
|
<tr>
|
|
<td class="ruletable"><a name="rulesgl" id="rulesgl"></a>gl</td>
|
|
<td class="ruletable"><p>uuu aaa _:nnn <code> .</code></p>
|
|
<p>where <code>_:</code>nnn identifies a blank node <a href="#defallocated" class="termref">allocated</a> to
|
|
the literal lll by <a href="#ruleslg" class="termref">rule lg</a>.</p></td>
|
|
<td class="ruletable"><p>uuu aaa lll<code> .</code></p> </td>
|
|
</tr>
|
|
</table>
|
|
<p>Clearly rule gl will simply produce a redundancy, except in cases where the
|
|
allocated blank node has been introduced into the object position of a new
|
|
triple by some other inference rule. The effect of these rules
|
|
is to ensure that any triple containing a literal, and the similar triple containing
|
|
the allocated blank node, are always derivable from one another, so that a
|
|
literal can be identified with its allocated blank node for purposes of applying
|
|
these rules. </p>
|
|
<h3 ><a name="RDFRules" id="RDFRules"></a>7.2 RDF Entailment Rules</h3>
|
|
<div class="title">RDF entailment rules</div>
|
|
<table border="1" summary="RDF entailment rules">
|
|
<tbody>
|
|
<tr class="ruletable">
|
|
<td ><strong>Rule Name</strong> </td>
|
|
<td ><strong>if E contains</strong></td>
|
|
<td ><strong>then add</strong></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td ><a name="rulerdf1" id="rulerdf1"></a>rdf1</td>
|
|
<td>uuu aaa yyy <code>.</code></td>
|
|
<td>aaa <code>rdf:type rdf:Property .</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdf2" id="rulerdf2"></a>rdf2</td>
|
|
<td><p>uuu aaa lll <code>.</code></p>
|
|
where lll is a well-typed XML literal .</td>
|
|
<td><p><code> _:</code>nnn <code>rdf:type rdf:XMLLiteral .</code></p>
|
|
<p>where _:nnn identifies a blank node <a href="#defallocated" class="termref">allocated
|
|
to</a> lll by <a href="#ruleslg" class="termref">rule lg</a>.</p></td>
|
|
</tr>
|
|
</tbody>
|
|
</table>
|
|
<p>These rules are <em><a href="#glossComplete" class="termref"> complete</a></em>
|
|
in the following sense. </p>
|
|
<p><strong>RDF entailment lemma</strong>. S <a href="#rdf_entail" class="termref">rdf-entails</a>
|
|
E if and only if there is a graph which can be derived from S plus the <a href="#RDF_axiomatic_triples" class="termref">RDF
|
|
axiomatic triples</a> by the application of <a href="#ruleslg" class="termref">rule
|
|
lg</a> and the <a href="#RDFRules" class="termref">RDF entailment rules</a>
|
|
and which <a href="#defentail" class="termref">simply entails</a> E.<span >
|
|
</span>(<a href="#RDFEntailmentLemmaPrf" class="termref">Proof</a> in Appendix
|
|
A)</p>
|
|
<p>Note that this does not require the use of <a href="#rulesgl" class="termref">rule
|
|
gl</a>. </p>
|
|
<h3><a name="RDFSRules" id="RDFSRules"></a>7.3 RDFS Entailment Rules</h3>
|
|
<div class="title">RDFS entailment rules.</div>
|
|
<table border="1" summary="RDFS entailment rules">
|
|
<tbody>
|
|
<tr class="ruletable">
|
|
<th >Rule Name</th>
|
|
<th >If E contains:</th>
|
|
<th >then add:</th>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs1" id="rulerdfs1"></a>rdfs1</td>
|
|
<td> <p>uuu aaa lll<code>.</code></p>
|
|
<p>where lll is a plain literal (with or without a language tag).</p></td>
|
|
<td><p><code> _:</code>nnn <code>rdf:type rdfs:Literal .</code></p>
|
|
<p>where <code>_:</code>nnn identifies a blank node <a href="#defallocated" class="termref">allocated
|
|
to</a> lll by rule <a href="#ruleslg" class="termref">rule lg</a>.</p></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs2" id="rulerdfs2"></a>rdfs2</td>
|
|
<td> <p>aaa <code>rdfs:domain</code> xxx <code>.</code><br />
|
|
uuu aaa yyy <code>.</code> </p></td>
|
|
<td>uuu <code>rdf:type</code> xxx <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs3" id="rulerdfs3"></a>rdfs3</td>
|
|
<td> <p>aaa <code>rdfs:range</code> xxx <code>.</code><br />
|
|
uuu aaa vvv <code>.</code> </p></td>
|
|
<td>vvv <code>rdf:type</code> xxx <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs4" id="rulerdfs4"></a>rdfs4a</td>
|
|
<td>uuu aaa xxx <code>.</code></td>
|
|
<td>uuu <code>rdf:type rdfs:Resource .</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td>rdfs4b</td>
|
|
<td>uuu aaa vvv<code>.</code></td>
|
|
<td>vvv <code>rdf:type rdfs:Resource .</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs5" id="rulerdfs5"></a>rdfs5</td>
|
|
<td> <p>uuu <code>rdfs:subPropertyOf</code> vvv <code>.</code><br />
|
|
vvv <code>rdfs:subPropertyOf</code> xxx <code>.</code></p></td>
|
|
<td>uuu <code>rdfs:subPropertyOf</code> xxx <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs6" id="rulerdfs6"></a>rdfs6</td>
|
|
<td>uuu <code>rdf:type rdf:Property .</code></td>
|
|
<td>uuu <code>rdfs:subPropertyOf</code> uuu <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs7" id="rulerdfs7"></a>rdfs7</td>
|
|
<td> <p>aaa <code>rdfs:subPropertyOf</code> bbb <code>.</code><br />
|
|
uuu aaa yyy <code>.</code> </p></td>
|
|
<td>uuu bbb yyy <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs8" id="rulerdfs8"></a>rdfs8</td>
|
|
<td> <p>uuu <code>rdf:type rdfs:Class .</code></p></td>
|
|
<td>uuu <code>rdfs:subClassOf rdfs:Resource .</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs9" id="rulerdfs9"></a>rdfs9</td>
|
|
<td> <p>uuu <code>rdfs:subClassOf</code> xxx <code>.</code><br />
|
|
vvv <code>rdf:type</code> uuu <code>.</code></p></td>
|
|
<td>vvv <code>rdf:type</code> xxx <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs10" id="rulerdfs10"></a>rdfs10</td>
|
|
<td>uuu <code>rdf:type rdfs:Class .</code></td>
|
|
<td>uuu <code>rdfs:subClassOf</code> uuu <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs11" id="rulerdfs11"></a>rdfs11</td>
|
|
<td> <p>uuu <code>rdfs:subClassOf</code> vvv <code>.</code><br />
|
|
vvv <code>rdfs:subClassOf</code> xxx <code>.</code></p></td>
|
|
<td>uuu <code>rdfs:subClassOf</code> xxx <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs12" id="rulerdfs12"></a>rdfs12</td>
|
|
<td>uuu <code>rdf:type rdfs:ContainerMembershipProperty .</code></td>
|
|
<td>uuu <code>rdfs:subPropertyOf rdfs:member .</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs13" id="rulerdfs13"></a>rdfs13</td>
|
|
<td>uuu <code>rdf:type rdfs:Datatype .</code></td>
|
|
<td>uuu <code>rdfs:subClassOf rdfs:Literal .</code></td>
|
|
</tr>
|
|
</tbody>
|
|
</table>
|
|
<p>Stating <a href="#glossComplete" class="termref">completeness</a> for these
|
|
rules requires more care, since it is possible for a graph to be rdfs-inconsistent
|
|
by virtue of containing unsatisfiable assertions about ill-typed XML literals,
|
|
for example:</p>
|
|
<p><code><ex:a> rdfs:subClassOf rdfs:Literal .</code><br />
|
|
<code> <ex:b> rdfs:range <ex:a> .</code><br />
|
|
<code> <ex:c> rdfs:subPropertyOf <ex:b>.</code><br />
|
|
<code> <ex:d> <ex:c> "<"^^rdf:XMLLiteral .</code></p>
|
|
<p>where the denotation of the ill-typed XML literal is required not to be a literal
|
|
value but can be inferred to be on the basis of the other assertions. Since
|
|
such an rdfs-inconsistent graph <a href="#rdfs_entailment" class="termref">rdfs-entails</a>
|
|
all RDF graphs, even when they are syntactically unrelated to the antecedent,
|
|
we have to exclude this case. </p>
|
|
<p>There is a characteristic signal of inconsistency which can be recognized by
|
|
the entailment rules, by the derivation of a triple of the form</p>
|
|
<p>xxx <code>rdf:type rdfs:Literal .</code></p>
|
|
<p>where xxx is <a href="#defallocated" class="termref">allocated</a> to an ill-typed
|
|
XML literal by <a href="#ruleslg" class="termref">rule lg</a>. Call such a triple
|
|
an <em>XML clash</em>. The derivation of such a clash from the above example
|
|
is straightforward:</p>
|
|
<p><code><ex:d> <ex:c> _:1 .</code> (by <a href="#ruleslg" class="termref">rule
|
|
lg</a>, with <code>_:1</code> <a href="#defallocated" class="termref">allocated</a>
|
|
to <code>"<"^^rdf:XMLLiteral</code>)<br />
|
|
<code><ex:d> <ex:b> _:1 .</code> (by rule <a href="#rulerdfs7" class="termref">rdfs7</a>)<br />
|
|
<code>_:1 rdf:type <ex:a>.</code> (by rule <a href="#rulerdfs3" class="termref">rdfs3</a>)<br />
|
|
<code>_:1 rdf:type rdfs:Literal .</code> (by rule <a href="#rulerdfs9" class="termref">rdfs9</a>)</p>
|
|
<p>These rules are then<em><a href="#glossComplete" class="termref"> complete</a></em>
|
|
in the following sense: </p>
|
|
<p><strong>RDFS entailment lemma</strong>. S <a href="#rdfs_entailment" class="termref">rdfs-entails</a>
|
|
E if and only if there is a graph which can be derived from S plus the <a href="#RDF_axiomatic_triples" class="termref">RDF</a>
|
|
and <a href="#RDFS_axiomatic_triples" class="termref">RDFS axiomatic triples</a>
|
|
by the application of <a href="#ruleslg" class="termref">rule lg</a>, <a href="#rulesgl" class="termref">rule gl</a> and
|
|
the
|
|
<a href="#RDFRules" class="termref">RDF</a> and <a href="#RDFSRules" class="termref">RDFS
|
|
entailment rules</a> and which either <a href="#defentail" class="termref">simply
|
|
entails</a> E or contains an XML clash. (<a href="#RDFSEntailmentLemmaPrf" class="termref">Proof</a>
|
|
in Appendix A)</p>
|
|
<p>The RDFS rules are somewhat redundant. All but one of the <a href="#RDF_axiomatic_triples" class="termref">RDF
|
|
axiomatic triples</a> can be derived from the rules <a href="#rulerdfs2" class="termref">rdfs2</a>
|
|
and <a href="#rulerdfs3" class="termref">rdfs3</a> and the <a href="#RDFS_axiomatic_triples" class="termref">RDFS
|
|
axiomatic triples</a>, for example.</p>
|
|
<p>The outputs of these rules will often trigger others. These rules will propagate
|
|
all <code>rdf:type</code> assertions in the graph up the subproperty and subclass
|
|
hierarchies, re-asserting them for all super-properties and superclasses. <a href="#rulerdf1" class="termref">rdf1</a>
|
|
will generate type assertions for all the property names used in the graph,
|
|
and <a href="#rulerdfs3" class="termref">rdfs3</a> together with the last <a href="#RDFS_axiomatic_triples" class="termref">RDFS
|
|
axiomatic triple</a> will add all type assertions for all the class names used.
|
|
Any subproperty or subclass assertion will generate appropriate type assertions
|
|
for its subject and object via <a href="#rulerdfs2" class="termref">rdfs2</a>
|
|
and <a href="#rulerdfs3" class="termref">rdfs3</a> and the domain and range
|
|
assertions in the RDFS axiomatic triple set. The rules will generate all assertions
|
|
of the form</p>
|
|
<p>uuu <code>rdf:type rdfs:Resource .</code></p>
|
|
<p>for every uuu in V, and of the form</p>
|
|
<p>uuu <code>rdfs:subClassOf rdfs:Resource .</code></p>
|
|
<p>for every class name uuu; and several more 'universal' facts, such as</p>
|
|
<p><code>rdf:Property rdf:type rdfs:Class .</code></p>
|
|
<h4><a name="RDFSExtRules" id="RDFSExtRules"></a>7.3.1 Extensional Entailment
|
|
Rules </h4>
|
|
<p>The stronger extensional semantic conditions described in <a href="#ExtensionalDomRang" class="termref">
|
|
Section 4.1</a> sanction further entailments which are not covered by the RDFS
|
|
rules. The following table lists some entailment patterns which are valid in
|
|
this stronger semantics. This is not a <a href="#glossComplete" class="termref">
|
|
complete</a> set of rules for the extensional semantic conditions. Note that
|
|
none of these rules are rdfs-valid; they apply only to semantic extensions which
|
|
apply the strengthened extensional semantic conditions described in <a href="#ExtensionalDomRang" class="termref">
|
|
Section 4.1</a>. These rules have other consequences, eg that <code>rdfs:Resource</code>
|
|
is a domain and range of every property.</p>
|
|
<p>Rules ext5-ext9 follow a common pattern; they reflect the fact that the strengthened
|
|
extensional conditions require domains (and ranges for transitive properties)
|
|
of the properties in the rdfV and rdfsV vocabularies to be as large as possible,
|
|
so any attempt to restrict them will be subverted by the semantic conditions.
|
|
Similar rules apply to superproperties of <code>rdfs:range</code> and <span ><code>rdfs:domain</code></span>.
|
|
None of these cases are likely to arise in practice. </p>
|
|
<div class="title">Some additional inferences which would be valid under the extensional
|
|
versions of the RDFS semantic conditions.</div>
|
|
<table border="1">
|
|
<tr class="ruletable">
|
|
<td >ext1</td>
|
|
<td > <p>uuu <code>rdfs:domain</code> vvv <code>.<br />
|
|
</code> vvv <code>rdfs:subClassOf</code> zzz <code>.</code></p></td>
|
|
<td >uuu <code>rdfs:domain</code> zzz <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td>ext2</td>
|
|
<td> <p>uuu <code>rdfs:range</code> vvv <code>.<br />
|
|
</code> vvv <code>rdfs:subClassOf</code> zzz <code>.</code></p></td>
|
|
<td>uuu <code>rdfs:range</code> zzz <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td>ext3</td>
|
|
<td>uuu <code>rdfs:domain</code> vvv <code>.<br />
|
|
</code> www <code>rdfs:subPropertyOf</code> uuu <code>.</code></td>
|
|
<td>www <code>rdfs:domain </code>vvv <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td>ext4</td>
|
|
<td>uuu <code>rdfs:range</code> vvv <code>.<br />
|
|
</code> www <code>rdfs:subPropertyOf</code> uuu <code>.</code></td>
|
|
<td>www <code>rdfs:range</code> vvv <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td >ext5</td>
|
|
<td><span ><code>rdf:type</code><code> rdfs:subPropertyOf</code> www<code>
|
|
.</code><br />
|
|
www <code>rdfs:domain</code> vvv<code> .</code> <br />
|
|
</span> </td>
|
|
<td ><code>rdfs:Resource </code><code>rdfs:subClassOf</code> vvv<code> .</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td >ext6</td>
|
|
<td><span ><code>rdfs:</code><code>subClassOf</code> <code>rdfs:subPropertyOf</code>
|
|
www<code> .</code><br />
|
|
www <code>rdfs:domain</code> vvv<code> .</code> <br />
|
|
</span> </td>
|
|
<td ><code>rdfs:Class</code> <code>rdfs:subClassOf</code> vvv<code> .</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td >ext7</td>
|
|
<td><span ><code>rdfs:subPropertyOf</code> <code>rdfs:subPropertyOf</code>
|
|
www<code> .</code><br />
|
|
www <code>rdfs:domain</code> vvv<code> .</code> <br />
|
|
</span> </td>
|
|
<td ><code>rdf:Property</code> <code>rdfs:subClassOf</code> vvv<code> .</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td >ext8</td>
|
|
<td><span ><code>rdfs:</code><code>subClassOf</code><code> rdfs:subPropertyOf</code>
|
|
www <code>.</code><br />
|
|
www <code>rdfs:range</code> vvv<code> .</code> <br />
|
|
</span> </td>
|
|
<td ><code>rdfs:Class</code> <code>rdfs:subClassOf</code> vvv<code> .</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td >ext9</td>
|
|
<td><span ><code>rdfs:subPropertyOf</code><code> rdfs:subPropertyOf</code>
|
|
www <code>.</code><br />
|
|
www <code>rdfs:range</code> vvv<code> .</code> <br />
|
|
</span> </td>
|
|
<td ><code>rdf:Property</code> <code>rdfs:subClassOf</code> vvv<code> .</code></td>
|
|
</tr>
|
|
</table>
|
|
<p> </p>
|
|
<h3><a name="DtypeRules" id="DtypeRules"></a>7.4 Datatype
|
|
Entailment Rules</h3>
|
|
<p>In order to capture <a href="#D_entailment" class="termref"> datatype entailment</a>
|
|
in terms of assertions and entailment rules, the rules need to refer to information
|
|
supplied by the <a href="#defDatatype" class="termref">datatype</a>s themselves;
|
|
and to state the rules it is necessary to assume syntactic conditions which
|
|
can only be checked by consulting the <a href="#defDatatype" class="termref">datatype</a>
|
|
sources.</p>
|
|
<p>For each kind of information which is available about a <a href="#defDatatype" class="termref">datatype</a>,
|
|
inference rules for information of that kind can be stated, which can be thought
|
|
of as extending the table of RDFS entailment rules. These should be understood
|
|
as applying to <a href="#defDatatype" class="termref">datatype</a>s other than
|
|
the built-in datatype, the rules for which are part of the RDFS entailment rules.
|
|
The rules stated below assume that information is available about the <a href="#defDatatype" class="termref">datatype</a>
|
|
denoted by a recognized URI reference, and they use that URI reference to refer
|
|
to the <a href="#defDatatype" class="termref">datatype</a>.</p>
|
|
<p>The basic information specifies, for each literal string, whether or not it
|
|
is a legal lexical form for the datatype, i.e. one which maps to some value
|
|
under the lexical-to-value mapping of the <a href="#defDatatype" class="termref">datatype</a>.
|
|
This corresponds to the following rule, for each string sss that is a legal
|
|
lexical form for the <a href="#defDatatype" class="termref">datatype</a> denoted
|
|
by ddd:</p>
|
|
<table border="1" summary="datatype rule">
|
|
<tr class="ruletable">
|
|
<td > <a name="rulerdfD1" id="rulerdfD1"></a>rdfD1</td>
|
|
<td > <p>ddd <code>rdf:type rdfs:Datatype .</code><br />
|
|
uuu aaa "sss"^^ddd <code>.</code></p></td>
|
|
<td > <p> _:nnn <code>rdf:type</code> ddd <code>.</code></p>
|
|
<p >where _:nnn identifies a blank node <a href="#defallocated" class="termref">allocated
|
|
to</a> "sss"^^ddd by rule <a href="#ruleslg" class="termref">rule
|
|
lg</a>.</p></td>
|
|
</tr>
|
|
</table>
|
|
<p>Suppose it is known that two lexical forms sss and ttt map to the same value
|
|
under the <a href="#defDatatype" class="termref">datatype</a> denoted by ddd; then the following rule applies:</p>
|
|
<table border="1" summary="datatype rule2">
|
|
<tr class="ruletable">
|
|
<td >rdfD2</td>
|
|
<td > <p>ddd <code>rdf:type rdfs:Datatype .</code><br />
|
|
uuu aaa "sss"^^ddd <code>.</code><br />
|
|
</p></td>
|
|
<td >uuu aaa "ttt"^^ddd <code>.</code></td>
|
|
</tr>
|
|
</table>
|
|
<p>Suppose it is known that the lexical form sss of the <a href="#defDatatype" class="termref">datatype</a> denoted by ddd
|
|
and the lexical form ttt of the <a href="#defDatatype" class="termref">datatype</a> denoted by eee map to the same value.
|
|
Then the following rule applies:</p>
|
|
<table border="1" summary="datatype rule3">
|
|
<tr class="ruletable">
|
|
<td >rdfD3</td>
|
|
<td > <p>ddd <code>rdf:type rdfs:Datatype .</code><br />
|
|
eee <code>rdf:type rdfs:Datatype .</code><br />
|
|
uuu aaa "sss"^^ddd <code>.</code><br />
|
|
</p></td>
|
|
<td >uuu aaa "ttt"^^eee <code>.</code></td>
|
|
</tr>
|
|
</table>
|
|
<p>In addition, if it is known that the value space of the <a href="#defDatatype" class="termref">datatype</a>
|
|
denoted by ddd is a subset of that of the <a href="#defDatatype" class="termref">datatype</a>
|
|
denoted by eee, then it would be appropriate to assert that </p>
|
|
<p>ddd <code>rdfs:subClassOf</code> eee <code>.</code></p>
|
|
<p>but this needs to be asserted explicitly; it does not follow from the subset
|
|
relationship alone.</p>
|
|
<p>Assuming that the information encoded in these rules is correct, applying these
|
|
and the earlier rules will produce a graph which is <a href="#D_entailment" class="termref">
|
|
D-entail</a>ed by the original. </p>
|
|
<p>The rules rdfD2 and 3 are essentially substitutions by virtue of equations
|
|
between lexical forms. Such equations may be capable of generating infinitely
|
|
many conclusions, e.g. it is possible to add any number of leading zeros to
|
|
any lexical form for <code>xsd:integer</code> without it ceasing to be a correct
|
|
lexical form for <code>xsd:integer</code>. To avoid such <a href="#glossValid" class="termref">correct</a>
|
|
but unhelpful inferences, it is sufficient to restrict rdfD2 to cases which
|
|
replace a lexical form with the canonical form for the <a href="#defDatatype" class="termref">datatype</a> in question,
|
|
when such a canonical form is defined. In order not to omit some valid entailments,
|
|
however, such canonicalization rules should be applied to the conclusions as
|
|
well as the antecedents of any proposed entailments, and the corresponding rules
|
|
of type rdfD3 would need to reflect knowledge of identities between canonical
|
|
forms of the distinct <a href="#defDatatype" class="termref">datatype</a>.</p>
|
|
<p>In particular cases other information might be available, which could be expressed
|
|
using a particular RDFS vocabulary. Semantic extensions may also define further
|
|
such datatype-specific meanings.</p>
|
|
<p>These rules allow one to conclude that any well-formed typed literal of a recognized
|
|
datatype will denote something in the class <code>rdfs:Literal</code>.</p>
|
|
<p><code><ex:a> <ex:p> "sss"^^<ex:dtype> .<br />
|
|
<ex:dtype> rdf:type rdfs:Datatype .</code></p>
|
|
<p><code><ex:a> <ex:p> _:nnn . </code>(by <a href="#ruleslg" class="termref">rule lg</a>)<code><br />
|
|
_:nnn rdf:type <ex:dtype> .</code> (by rule <a href="#rulerdfD1" class="termref">rdfD1</a>)<code><br />
|
|
<ex:dtype> rdfs:subClassOf rdfs:Literal .</code> (by rule <a href="#rulerdfs11" class="termref">rdfs11</a>)<code><br />
|
|
_:nnn rdf:type rdfs:Literal .</code> (by rule <a href="#rulerdfs9" class="termref">rdfs9</a>)</p>
|
|
<p>The rule rdfD1 is sufficient to expose some cases of a <a href="#defdatatypeclash" class="termref">datatype
|
|
clash</a>, by a chain of reasoning of the following form:</p>
|
|
<p><code><ex:p> rdfs:range <ex:dtype> .<br />
|
|
<ex:a> <ex:p> "sss"^^<ex:otherdtype> .</code></p>
|
|
<p><code><ex:a> <ex:p> _:nnn .<br />
|
|
_:nnn rdf:type <ex:otherdtype> .</code> (by rule <a href="#rulerdfD1" class="termref">rdfD1</a>)<br />
|
|
<code>_:nnn rdf:type <ex:dtype> .</code> (by rule <a href="#rulerdfs3" class="termref">rdfs3</a>)</p>
|
|
<p>These rules may not provide a complete set of inference principles for D-entailment,
|
|
since there may be valid D-entailments for particular datatypes which depend
|
|
on idiosyncratic properties of the particular datatypes, such as the size of
|
|
the value space (e.g. <code>xsd:boolean</code> has only two elements, so anything
|
|
established for those two values must be true for all literals with this datatype.)<a name="xsdstringlitnote" id="xsdstringlitnote"></a><span >
|
|
In particular, the value space and lexical-to-value mapping of the XSD datatype
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#string"><code>xsd:string</code></a>
|
|
sanctions the identification of typed literals with plain literals without language
|
|
tags for all character strings which are in the lexical space of the datatype,
|
|
since both of them denote the Unicode character string which is displayed in
|
|
the literal; so the following inference rule is valid in all XSD-interpretations.
|
|
Here, 'sss' indicates any RDF string in the lexical space of
|
|
<a href="http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#string"><code>xsd:string</code></a>.</span></p>
|
|
<table border="1" summary="xsd strings are same as plain literals">
|
|
<tr class="ruletable">
|
|
<td >xsd 1a</td>
|
|
<td >uuu aaa "sss"<code>.</code></td>
|
|
<td >uuu aaa "sss"^^<code>xsd:string
|
|
.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td >xsd 1b</td>
|
|
<td >uuu aaa "sss"^^<code>xsd:string .</code></td>
|
|
<td >uuu aaa "sss"<code>.</code></td>
|
|
</tr>
|
|
</table>
|
|
<p >Again, as with the rules rdfD2 and rdfD3, applications may
|
|
use a systematic replacement of one of these equivalent forms for the other
|
|
rather than apply these rules directly. </p>
|
|
<h2><a name="prf" id="prf">Appendix A: Proofs of Lemmas (Informative)</a></h2>
|
|
|
|
|
|
<div class="title">"One of the merits of a proof is that it instills a certain
|
|
doubt as to the result proved." -Bertrand Russell</div>
|
|
<p><strong><a name="emptygraphlemmaprf" id="emptygraphlemmaprf"></a>Empty Graph
|
|
Lemma.</strong> The empty set of triples is entailed by any graph, and does
|
|
not entail any graph except itself.</p>
|
|
<blockquote>
|
|
<p><strong>Proof.</strong> Let N be the empty set of triples. The semantic conditions
|
|
on graphs require that N is true in I, for any I; so the first part follows
|
|
from the definition of entailment. Suppose G is any nonempty graph and s p
|
|
o <code>.</code> is a triple in G, then an interpretation I with IEXT(I(p))
|
|
= { } does not satisfy G but does satisfy N; so N does not entail G. <strong>QED</strong>.</p>
|
|
</blockquote>
|
|
<p>This means that most of the subsequent results are trivial for empty graphs,
|
|
which is what one would expect. </p>
|
|
<p><a name="subglemprf" id="subglemprf"><strong>Subgraph Lemma.</strong> A graph
|
|
entails all its subgraphs.</a></p>
|
|
<blockquote>
|
|
<p><strong>Proof.</strong> Obvious, from definitions of <a
|
|
href="#defsubg" class="termref">subgraph</a> and <a
|
|
href="#defentail" class="termref">entailment</a>. If the graph is true in
|
|
I then for some A, all its triples are true in I+A, so every subset of triples
|
|
is true in I. <strong>QED</strong></p>
|
|
</blockquote>
|
|
<p><a name="mergelemprf" id="mergelemprf"><strong>Merging lemma.</strong></a>
|
|
The <a href="#defmerge" class="termref">merge</a> of a set S of RDF graphs is
|
|
entailed by S, and entails every member of S.</p>
|
|
<blockquote>
|
|
<p><strong>Proof.</strong> Obvious, from definitions of <a
|
|
href="#defentail" class="termref">entailment</a> and merge. All members
|
|
of S are true if and only if all triples in the merge of S are true. <strong>QED</strong>.</p>
|
|
</blockquote>
|
|
<p>This means that, as noted in the text, a set of graphs can be treated as a
|
|
single graph when discussing satisfaction and entailment. This convention will
|
|
be adopted in the rest of the appendix, where a reference to an interpretation
|
|
of a set of graphs, a set of graphs entailing a graph, and so on, should be
|
|
understood in each case to refer to the merge of the set of graphs, and references
|
|
to 'graph' in the following can be taken to refer to graphs or to sets of graphs.</p>
|
|
<p><a name="instlemprf" id="instlemprf"><strong>Instance Lemma.</strong> A graph
|
|
is entailed by all its instances.</a></p>
|
|
<blockquote>
|
|
<p><strong>Proof.</strong> Suppose I <a
|
|
href="#defsatis" class="termref">satisfies</a> E' and E' is an <a
|
|
href="#definst" class="termref">instance</a> of E. Then for some mapping
|
|
A on the blank nodes of E', I+A satisfies every triple in E'. For each blank
|
|
node b in E, define B(b)=I+A(c), where c is the blank node or <a href="#defname" class="termref">name</a>
|
|
that is substituted for b in E', or c=b if nothing was substituted for it.
|
|
Then I+B(E)=I+A(E')=true, so I satisfies E. But I was arbitrary; so E' <a href="#defentail" class="termref">entails</a>
|
|
E. <strong>QED</strong>.</p>
|
|
</blockquote>
|
|
<p><a id="defskolem" name="defskolem">Skolemization</a> is a syntactic transformation
|
|
routinely used in automatic inference systems in which existential variables
|
|
are replaced by 'new' functions - function names not used elsewhere - applied
|
|
to any enclosing universal variables. In RDF, Skolemization amounts to replacing
|
|
every blank node in a graph by a 'new' name, i.e. a URI reference which is guaranteed
|
|
to not occur anywhere else. In effect, it gives 'arbitrary' names to the anonymous
|
|
entities whose existence was asserted by the use of blank nodes: the arbitrariness
|
|
of the names ensures that nothing can be inferred that would not follow from
|
|
the bare assertion of existence represented by the blank node. (Using a literal
|
|
would not do. Literals are never 'new' in the required sense.) </p>
|
|
<p>To be precise, a <em>Skolemization</em> of E (with respect to V) is a ground
|
|
instance of E with respect to V with a 1:1 instance mapping that maps each
|
|
blank node in G to a URI reference that does not appear in G (so the Skolem
|
|
vocabulary V must be disjoint from the vocabulary of E)</p>
|
|
<p>While not itself strictly a <a href="#glossValid"
|
|
class="termref">valid</a> operation, Skolemization adds no new content to
|
|
an expression, in the sense that a Skolemized expression has the same entailments
|
|
as the original expression provided they do not contain names from the Skolem
|
|
vocabulary:</p>
|
|
<p><a name="skolemlemprf" id="skolemlemprf"><strong>Skolemization Lemma.</strong>
|
|
Suppose sk(E) is a skolemization of E with respect to V. Then sk(E) entails
|
|
E; and if sk(E) entails F and the vocabulary of F is disjoint from V, then E
|
|
entails F .</a></p>
|
|
<blockquote>
|
|
<p><strong>Proof.</strong> sk(E) entails E by the instance lemma.</p>
|
|
<p>Now, suppose that sk(E) entails F where F shares no vocabulary with V; and
|
|
suppose I is some interpretation satisfying E. Then for some mapping A from
|
|
the blank nodes of E, I+A satisfies E. Define an interpretation I' of the
|
|
vocabulary of sk(E) by: IR'=IR, IEXT'=IEXT, I'(x)=I(x) for x in the vocabulary
|
|
of E, and I'(x)=[I+A](y) for x in V, where y is the blank node in E that is
|
|
replaced by x in sk(E). Clearly I' satisfies sk(E), so I' satisfies F. But
|
|
I'(F)=[I+A](F) since the vocabulary of F is disjoint from that of V; so I
|
|
satisfies F. But I was arbitrary; so E entails F. </p>
|
|
<p><strong>QED</strong>.</p>
|
|
</blockquote>
|
|
<p> Intuitively, this lemma shows that asserting a Skolemization expresses a similar
|
|
content to asserting the original graph, in many respects. However, a graph
|
|
should not be thought of as being equivalent to its Skolemization, since these
|
|
'arbitrary' names would have the same status as any other URI references once
|
|
published. Also, Skolemization would not be an appropriate operation when applied
|
|
to anything other than the antecendent of an entailment. A Skolemization of
|
|
a query would represent a completely different query. Nevertheless, for many
|
|
purposes when proving results about entailment, we need only consider ground
|
|
graphs: for provided E does not contain any Skolem vocabulary, S entails E iff
|
|
S' entails E.</p>
|
|
<p>The proof of the subsequent lemmas uses a way of constructing an interpretation
|
|
of a graph by using the lexical items in the graph itself. (This was <a
|
|
href="http://www-groups.dcs.st-andrews.ac.uk/%7Ehistory/Mathematicians/Herbrand.html">
|
|
Herbrand</a>'s idea; we here modify it slightly to handle literals appropriately.)
|
|
Given a nonempty graph G, <a name="defherbinterp" id="defherbinterp"></a>the
|
|
<em>(simple) Herbrand interpretation</em> of G, written <a name="defHerb" id="defHerb"></a>Herb(G),
|
|
is the interpretation defined as follows.</p>
|
|
<table border="1">
|
|
<tr>
|
|
<td><p>LV<sub>Herb(G)</sub> = the set of all plain literals in G; </p>
|
|
<p>IR<sub>Herb(G)</sub> = the set of all <a href="#defname" class="termref">name</a>s
|
|
and blank nodes which occur in a subject or object position in a triple
|
|
in G; </p>
|
|
<p>IP<sub>Herb(G)</sub> = the set of URI references which occur in the property
|
|
position of a triple in G;</p>
|
|
<p>IEXT<sub>Herb(G)</sub> = {<s,o>: G contains a triple s p o <code>.</code>
|
|
} </p>
|
|
<p>IS<sub>Herb(G)</sub> and IL<sub>Herb(G)</sub> are both identity mappings
|
|
on the appropriate parts of the vocabulary of G.</p> </td>
|
|
</tr>
|
|
</table>
|
|
<p>Clearly Herb(G)+B, where B is the identity map on blank nodes in G, satisfies
|
|
every triple in G, by construction, so Herb(G) satisfies G.</p>
|
|
<p><a href="#defherbinterp" class="termref">Herbrand interpretation</a>s treat
|
|
URI references and typed literals (and blank nodes) in the same way as plain literals, i.e. as denoting their own syntactic forms. Of course this may not
|
|
be what was intended by the writer of the RDF, but the construction shows that
|
|
any graph <i>can</i> be interpreted in this way. This therefore establishes
|
|
that any RDF graph has a <a href="#glossSatisfy"
|
|
class="termref">satisfying</a> simple interpretation, i.e. there cannot be
|
|
a simple inconsistency in RDF. </p>
|
|
<p>Notice that the universe of the Herbrand interpretation of G contains the blank
|
|
nodes of G; they are 'standing for' the entities that they assert the existence
|
|
of, in effect. Since blank nodes must be interpreted to denote themselves in
|
|
order to satisfy the graph, the Herbrand interpretation of a Skolemization of
|
|
a graph is isomorphic with the Herbrand interpretation of the graph together
|
|
with the blank node mapping: Herb(sk(G)) = Herb(G)+B (using a familiar abuse
|
|
of notation where a blank node in a Herbrand interpretation is treated as a
|
|
Skolem name.)</p>
|
|
<p><a name="interplemmaprf"
|
|
id="interplemmaprf"><strong>Interpolation Lemma.</strong> S entails E if and
|
|
only if a subgraph of S is an instance of E</a>.</p>
|
|
<blockquote>
|
|
<p><strong>Proof.</strong> 'if' follows from the subgraph and instance lemmas.
|
|
</p>
|
|
<p>'only if' uses the Herbrand construction. Suppose S simply entails E. <a href="#defHerb" class="termref">Herb(</a>S)
|
|
satisfies S, so <a href="#defHerb" class="termref">Herb(</a>S) satisfies E,
|
|
i.e. for some mapping A from the blank nodes of E to IR<sub>Herb(S)</sub>,
|
|
[<a href="#defHerb" class="termref">Herb</a>(S)+A] satisfies every triple
|
|
<br />
|
|
s p o <code>.</code> <br />
|
|
in E, so S must contain the triple <br />
|
|
[<a href="#defHerb" class="termref">Herb(</a>E)+A](s) p [<a href="#defHerb" class="termref">Herb(</a>E)+A](o)
|
|
<code>.</code> <br />
|
|
which is the instance of the previous triple under the instance mapping A.
|
|
So the set of all such triples is a subgraph of S which is an instance of
|
|
E. </p>
|
|
<p><strong> QED</strong></p>
|
|
</blockquote>
|
|
<p>The following are direct consequences of the interpolation lemma:</p>
|
|
<p><a name="Anonlem1prf" id="Anonlem1prf"><strong>Anonymity lemma.</strong></a>
|
|
Suppose E is a <a href="#deflean" class="termref">lean</a> graph and E' is a
|
|
proper instance of E. Then E does not entail E'.</p>
|
|
<blockquote>
|
|
<p><strong>Proof.</strong> Suppose E entails E', then a subgraph of E is an
|
|
instance of E' and therefore a proper instance of E; so E is not <a
|
|
href="#deflean" class="termref">lean</a> , contrary to hypothesis. So E
|
|
does not entail E'.<strong><br />
|
|
QED</strong></p>
|
|
</blockquote>
|
|
<p><strong><a name="compactlemmaprf" id="compactlemmaprf"></a>Compactness Lemma</strong>.
|
|
If S entails E and E is a finite graph, then some finite subset S' of S entails
|
|
E.</p>
|
|
<blockquote>
|
|
<p><strong>Proof.</strong> By the interpolation lemma, a subgraph S' of S is
|
|
an instance of E; so S' is finite, and S' entails E. <strong><br />
|
|
QED</strong></p>
|
|
</blockquote>
|
|
<p>Although compactness is trivial for simple entailment, it becomes progressively
|
|
less trivial in more elaborate semantic extensions. </p>
|
|
<p><strong><a name="monotonicitylemmaprf" id="monotonicitylemmaprf"></a>Monotonicity
|
|
Lemma</strong>. Suppose S is a subgraph of S' and S entails E. Then S' entails
|
|
E. (Special case of <a href="#GeneralMonotonicityLemmaprf" class="termref">general
|
|
monotonicity lemma</a>) <strong>QED</strong></p>
|
|
<p><strong><a name="GeneralMonotonicityLemmaprf" id="GeneralMonotonicityLemmaprf"></a>General
|
|
monotonicity lemma</strong>. Suppose that S, S' are sets of RDF graphs with
|
|
every member of S a subset of some member of S'. Suppose that Y indicates a
|
|
semantic extension of X, S X-entails E, and S and E satisfy any syntactic
|
|
restrictions of Y. Then S' Y-entails E.</p>
|
|
<blockquote>
|
|
<p><strong>Proof. </strong>This follows simply by tracing the definitions. Suppose
|
|
that I is a Y-interpretation of S'; then since Y is a semantic extension of
|
|
X, I is an X-interpretation; and by the subgraph and merge lemmas, I satisfies
|
|
S; so I satisfies E.<br />
|
|
<strong>QED</strong></p>
|
|
</blockquote>
|
|
<p>Both of the following proofs follow a common pattern which generalizes that
|
|
used in the proof of the interpolation lemma, by using a modification of the
|
|
Herbrand construction applied to a 'closure' obtained by applying rules to exhaustion.
|
|
The proofs operate by showing that the resulting interpretation is both appropriate
|
|
to the vocabulary and also acts similarly to the <a href="#defHerb" class="termref">Herbrand
|
|
interpretation</a>. Much of the complexity of the proofs arises from the need
|
|
to adapt the Herbrand construction in order to take proper account of literal
|
|
values. Herbrand interpretations ignore literal typing and treat all typed literals
|
|
as non-literal values; this is irrelevant when considering simple entailment,
|
|
which treats typed literals simply as denoting names; but more care will be
|
|
needed when considering rdf- and rdfs-interpretations.</p>
|
|
<p>Both proofs use a single basic idea which requires rather an awkward notation
|
|
but is basically straightforward to understand. The simple Herbrand interpretation
|
|
treats all vocabulary items as denoting themselves, and builds the interpretation
|
|
out of these syntactic items. The semantic conditions on rdf- and rdfs-interpretations
|
|
do not permit this in all cases: XML literals in particular are required to
|
|
denote other kinds of entity. We therefore distinguish between the 'real' semantic
|
|
values and their syntactic 'surrogates' in these cases, by defining a mapping
|
|
<em>sur</em> from the universe of the intepretation to the vocabulary of the
|
|
graph (plus blank nodes) which is as close as possible to being an identity
|
|
mapping, but which when applied to these special literal values, identifies
|
|
the particular blank node which acts as a witness for that value in the graph.
|
|
In the case of RDFS, the surrogate mapping is extended to all literal values,
|
|
since the blank node allocated to the literal can occur in a subject position,
|
|
and hence record information about the literal value which must be applied back
|
|
to that value in the interpretation. </p>
|
|
<p><strong><a name="RDFEntailmentLemmaPrf" id="RDFEntailmentLemmaPrf"></a></strong><strong>RDF
|
|
entailment lemma</strong>. S <a href="#rdf_entail" class="termref">rdf-entails</a>
|
|
E if and only if there is a graph which can be derived from S plus the <a href="#RDF_axiomatic_triples" class="termref">RDF
|
|
axiomatic triples</a> by the application of <a href="#ruleslg" class="termref">rule
|
|
lg</a> and the <a href="#RDFRules" class="termref">RDF entailment rules</a>
|
|
and which simply entails E.<span > </span></p>
|
|
<blockquote>
|
|
<p><strong>Proof. </strong> To show 'if' one has only to check that the rules
|
|
are rdf-valid, which is left as an exercise for the reader; and if S or E
|
|
is empty then the result follows trivially; so suppose they are both non-empty.</p>
|
|
<p>To establish 'only if', the proof proceeds by constructing an <em>rdf Herbrand
|
|
interpretation</em> RH of S which serves the same role for rdf-interpretations
|
|
that the simple Herbrand interpretation does for simple interpretations. The
|
|
construction follows the Herbrand construction as far as possible, but interprets
|
|
well-formed XML literals so as to satisfy the RDF semantic conditions, guided
|
|
by the triples in the <em>RDF closure</em>, C, defined to be the graph resulting
|
|
from the following process:</p>
|
|
<p>add to S all the <span ><a href="#RDF_axiomatic_triples" class="termref">RDF
|
|
axiomatic triples</a></span>; <br />
|
|
apply <span ><a href="#simpleRules" class="termref"></a> </span> <a href="#ruleslg" class="termref">rule
|
|
lg</a> to any triple containing a well-typed XML literal until the graph is
|
|
unchanged by the rule;<br />
|
|
apply rule <a href="#rulerdf2" class="termref">rdf2</a> until the graph is
|
|
unchanged;<br />
|
|
apply rule <a href="#rulerdf1" class="termref">rdf1</a> until the graph is
|
|
unchanged.</p>
|
|
<p>Note that C contains precisely one new blank node _:nnn <a href="#defallocated" class="termref">allocated</a>
|
|
to each literal in S by the rule <a href="#ruleslg" class="termref">rule lg</a>,
|
|
and that the subgraph of triples in S containing any well-typed XML literal
|
|
is reproduced exactly in C with this blank node replacing the literal and
|
|
with the extra triple<br />
|
|
_:nnn <code>rdf:type</code> <code>rdf:XMLLiteral .</code><br />
|
|
introduced by rule <a href="#rulerdf2" class="termref">rdf2</a>. Note also
|
|
that the proof only requires that <a href="#ruleslg" class="termref">rule
|
|
lg</a> is used on well-typed XML literals, so that it actually establishes
|
|
a slightly tighter result.</p>
|
|
<p>Blank nodes introduced by <a href="#ruleslg" class="termref">rule lg</a>
|
|
stand as <em>surrogates</em> for well-formed XML literals in the subject position
|
|
of a triple. (In the proof of the next lemma, this will be extend to all literals.)
|
|
In order to construct an RDF interpretation, XML literals and their surrogates
|
|
must be replaced by the appropriate literal values in the domain of the interpretation,
|
|
but the proof requires that each XML literal value be uniquely associated
|
|
with a lexical item that denotes it. This requires some delicacy in the following
|
|
construction. </p>
|
|
<p>If lll is a well-formed XML literal, let <em>xml</em>(lll) be the XML value
|
|
of lll; and for each XML value x of any well-formed XML literal in C, let
|
|
<em>sur</em>(x) be the blank node allocated to that XML literal by <a href="#ruleslg" class="termref">rule
|
|
lg</a>; and extend <em>sur</em> to be the identity mapping on URI references,
|
|
blank nodes and all other literals in C. </p>
|
|
<p>RH is then defined by:</p>
|
|
<table border="1">
|
|
<tr>
|
|
<td><p>LV<sub>RH</sub> = all plain literals in C plus {<em>xml</em>(x):
|
|
x a well-typed XML literal in S}</p>
|
|
<p>IR<sub>RH</sub> = LV<sub>RH</sub> plus the set of URI references, blank
|
|
nodes and other typed literals occurring in C<sub></sub> </p>
|
|
|
|
<p>IP<sub>RH</sub> = {x: C contains the triple: x <code>rdf:type rdf:Property
|
|
.</code>}</p>
|
|
|
|
<p>If x is in IP<sub>RH</sub> then IEXT<sub>RH</sub>(x) = {<s,o>:
|
|
C contains the triple <em>sur</em>(s) x <em>sur</em>(o) <code>.</code>
|
|
} </p>
|
|
<p> IS<sub>RH</sub> is the identity map on URIrefs in S</p>
|
|
<p>If x is a well-formed XML literal in S then IL<sub>RH</sub>(x) =
|
|
<em>xml</em>(x), otherwise IL<sub>RH</sub>(x) = x</p>
|
|
</td>
|
|
</tr>
|
|
</table>
|
|
|
|
|
|
<p>Define a mapping B on blank nodes in C as follows: B(x)=<em>xml</em>(lll)
|
|
if x is allocated to a well-formed XML literal lll, otherwise B(x)=x, then
|
|
clearly [RH+B] satisfies C and therefore S, so RH satisfies S. </p>
|
|
<p>Since C contains all the required RDF axiomatic triples, RH satisfies them.
|
|
</p>
|
|
<p>It is easy to see that J satisfies the first two RDF semantic conditions,
|
|
by construction; for the triples introduced by rule <a href="#rulerdf2" class="termref">rdf2</a>
|
|
require that IEXT<sub>RH</sub>(rdf:type) contains <<em>xml</em>(lll),<code>rdf:XMLLiteral</code>>
|
|
for every well-typed XML literal lll. </p>
|
|
<p>The <a href="#rdfsemcond3" class="termref">third RDF semantic condition</a>
|
|
is the only negative semantic condition which cannot be satisfied simply by
|
|
construction, but it is satisfied trivially. Ill-typed XML literals denote
|
|
themselves in RH, and so are excluded from LV<sub>RH </sub>by construction.
|
|
The pair <lll, <code>rdf:XMLLiteral</code>> cannot occur in IEXT<sub>RH</sub>(<code>rdf:type</code>)
|
|
because a literal cannot occur in subject position; so the condition is satisfied,
|
|
so RH is an rdf-interpretation.</p>
|
|
<p>Since S rdf-entails E, RH satisfies E: so for some mapping A from the blank
|
|
nodes of E to IR<sub>RH</sub>, [RH+A] satisfies every triple <br />
|
|
s p o <code>.</code><br />
|
|
in E, i.e. IEXT<sub>RH</sub>(p) contains <[RH+A](s),[RH+A](o)>, i.e.C
|
|
contains a triple <br />
|
|
<em>sur</em>([RH+A](s)) p <em>sur</em>([RH+A](o))<code>.<br />
|
|
</code> but this is an instance of the first triple under the instantiation
|
|
mapping x -> <em>sur</em>(A(x)); so a subgraph of C is an instance of E;
|
|
so C simply entails E.</p>
|
|
<p><strong>QED</strong></p>
|
|
</blockquote>
|
|
<p>This lemma also shows that any graph has a satisfying rdf-interpretation, and
|
|
the proof illustrates how to construct it from a Herbrand interpretation of
|
|
the closure, by interpreting well-formed XML literals appropriately and allowing
|
|
the possible existence of properties which have no extensions. Note that if
|
|
E is finite then the derived subgraph of C is also finite.</p>
|
|
<p>The proof of the RDFS entailment lemma is similar in structure and uses closely
|
|
similar definitions, but is of course longer and requires a more elaborate construction
|
|
to ensure that the class extensions of <code>rdfs:Literal</code> and <code>rdfs:Resource</code>
|
|
contain all literal values. </p>
|
|
<p><a name="RDFSEntailmentLemmaPrf" id="RDFSEntailmentLemmaPrf"></a><strong>RDFS
|
|
entailment lemma</strong>. S <a href="#rdfs_entailment" class="termref">rdfs-entails</a>
|
|
E if and only if there is a graph which can be derived from S plus the <a href="#RDF_axiomatic_triples" class="termref">RDF</a>
|
|
and <a href="#RDFS_axiomatic_triples" class="termref">RDFS axiomatic triples</a>
|
|
by the application of <a href="#ruleslg" class="termref">rule lg</a>, <a class="termref" href="#rulesgl">rule
|
|
gl</a> and the
|
|
<a href="#RDFRules" class="termref">RDF</a> and <a href="#RDFSRules" class="termref">RDFS
|
|
entailment rules</a> and which either simply entails E or is an XML clash. </p>
|
|
<blockquote>
|
|
<p><strong>Proof. </strong> Again, to show 'if' it is sufficient to show that
|
|
the <span ><a href="#RDFSRules" class="termref">RDFS entailment
|
|
rules</a></span> are rdfs-valid, which is again left as an exercise; and again,
|
|
the empty cases are trivial. </p>
|
|
<p>The proof of 'only if' is similar to that used in the previous lemma, and
|
|
similar constructions and terminology will be used, except that the RDFS closure,
|
|
D, is defined to be the graph resulting from the following process:</p>
|
|
<p>add to S all the <span ><a href="#RDF_axiomatic_triples" class="termref">RDF</a></span>
|
|
and <a href="#RDFS_axiomatic_triples" class="termref">RDFS axiomatic triples</a>;
|
|
<br />
|
|
apply <span ><a href="#simpleRules" class="termref"></a> </span> <a href="#ruleslg" class="termref">rule
|
|
lg</a> to any triple containing a literal until the graph is unchanged by
|
|
the rule;<br />
|
|
apply rules <a href="#rulerdf2" class="termref">rdf2</a> and <a href="#rulerdfs1" class="termref">rdfs1</a>
|
|
until the graph is unchanged;<br />
|
|
apply rule <a href="#rulerdf1" class="termref">rdf1</a>, <a href="#rulesgl" class="termref">rule gl</a> and the
|
|
remaining
|
|
<a href="#RDFSRules" class="termref">RDFS entailment rules</a> until the
|
|
graph is unchanged.</p>
|
|
<p>Unlike the previous
|
|
lemma, this proof requires that <a href="#ruleslg" class="termref">rule
|
|
lg</a> is applied to all literals, even ill-typed XML literals, and it
|
|
requires the inverse <a href="#rulesgl" class="termref">rule gl</a>. <a href="#rulesgl" class="termref">Rule
|
|
gl</a> needs to be used only after an application of rules
|
|
<a href="#rulerdfs6" class="termref">rdfs6</a> or <a href="#rulerdfs10" class="termref">rdfs10</a>,
|
|
since those are the only rules which can move a blank node from subject
|
|
to object position. Note
|
|
that D contains precisely one new blank node _:nnn <a href="#defallocated" class="termref">allocated</a>
|
|
to each literal in S by the rule <a href="#ruleslg" class="termref">rule
|
|
lg</a>,
|
|
and that the subgraph of triples in S containing any literal is reproduced
|
|
exactly in D with this blank node replacing the literal and with the extra
|
|
triple<br />
|
|
_:nnn <code>rdf:type</code> <code>rdfs:Literal .<br />
|
|
</code>introduced by rule <a href="#rulerdfs1" class="termref">rdfs1</a>,
|
|
and possibly also <br />
|
|
_:nnn <code>rdf:type</code> <code>rdf:XMLLiteral .</code><br />
|
|
introduced by rule <a href="#rulerdf2" class="termref">rdf2</a> when appropriate.
|
|
This means that after this point in the construction, literals can effectively
|
|
be ignored, since any of the subsequent rules which applies to triples containing
|
|
a literal will also apply equally well to the similar triples where the
|
|
literal is replaced by its allocated blank node. The rest of the proof uses
|
|
this by requiring literal values in the interpretation to satisfy just the
|
|
semantic conditions imposed on the blank nodes allocated to the corresponding
|
|
literal, and ignoring triples in the graph which contain literals. The use
|
|
of <a href="#rulesgl" class="termref">rule gl</a> ensures that D contains
|
|
any triple containing a literal if and only if it contains the similar triple
|
|
with the literal replaced by its allocated blank node. </p>
|
|
<p>As in the previous proof, if lll is a well-formed XML literal, let <em>xml</em>(lll)
|
|
be the XML value of lll; the surrogate mapping <em>sur</em> is then extended
|
|
as follows. First, the domain of <em>sur</em> is the set containing just the
|
|
URI references, literals and blank nodes occurring in D and all XML values
|
|
of well-formed XML literals in D. (This is the universe of the rdfs-Herbrand
|
|
interpretation, defined below.) Now, if lll is a well-formed XML literal in
|
|
D, let <em>sur</em>(<em>xml</em>(lll)) be the blank node allocated to lll
|
|
by <a href="#ruleslg" class="termref">rule lg</a>; for any other literal lll
|
|
in D, let <em>sur</em>(lll) be the blank node allocated to lll by <a href="#ruleslg" class="termref">rule
|
|
lg</a>, and for all URI references and blank nodes in D, let <em>sur</em>(x)
|
|
= x . Note that the range of <em>sur</em> contains only URI references
|
|
and blank nodes which occur in D. </p>
|
|
<p>The <em>rdfs-Herbrand interpretation</em> SH of S is then constructed similarly
|
|
to the previous lemma. </p>
|
|
<table border="1">
|
|
<tr>
|
|
<td ><p>LV<sub>SH</sub> = {x: D contains the triple: <em>sur</em>(x) <code>rdf:type
|
|
rdfs:Literal .</code>}</p>
|
|
<p>IR<sub>SH</sub> = LV<sub>SH</sub> plus the set of URI references, blank
|
|
nodes and literals other than well-formed XML literals occurring in D </p>
|
|
<p>IP<sub>SH</sub> = {x: D contains the triple: <em>sur</em>(x)<code></code><code>
|
|
rdf:type rdf:Property .</code>}</p>
|
|
|
|
<p>If x is in IP<sub>RH</sub> then IEXT<sub>RH</sub>(x) = {<s,o>:
|
|
D contains the triple <em>sur</em>(s) x <em>sur</em>(o) <code>.</code>
|
|
} </p>
|
|
<p> IS<sub>SH</sub> is the identity map on URI references in S</p>
|
|
|
|
<p>If x is a well-formed XML literal in S then IL<sub>SH</sub>(x) = <em>xml</em>(x),
|
|
otherwise IL<sub>SH</sub>(x) = x</p>
|
|
</td>
|
|
</tr>
|
|
</table>
|
|
|
|
|
|
<p>Define B(x) as follows: if x is a blank node allocated to a well-formed XML
|
|
literal lll in D then B(x) = <em>xml</em>(lll); if it is allocated to any
|
|
other literal lll in D then B(x)=lll; and otherwise B(x)=x; then clearly [SH+B]
|
|
satisfies D and therefore S, so SH satisfies S. </p>
|
|
<p>As in the previous lemma, SH satisfies all the required RDF and RDFS axiomatic
|
|
triples and the first two RDF semantic conditions by construction.</p>
|
|
<p>SH satisfies the third RDF semantic condition just in case D does not contain
|
|
an XML clash. Note that the presence of surrogates for ill-typed XML literals
|
|
invalidates the argument used in the previous lemma to the effect that this
|
|
condition is trivally satisfied. So assume that D does not contain an XML
|
|
clash. </p>
|
|
<p>As noted in the text, we can regard the first RDFS semantic condition as
|
|
defining ICEXT and IC: we will do so without further comment and describe
|
|
all the conditions in terms of IEXT. To show that SH satisfies
|
|
the remaining RDFS semantic conditions we argue case by case, using the minimality
|
|
of the Herbrand interpretation and the completeness of the closure. </p>
|
|
<p>All of these conditions can be mirrored by a corresponding sequence of rule
|
|
applications. The general form of the argument can be illustrated with the
|
|
case of the <a href="#rdfssemcond2" class="termref">second RDFS semantic condition</a>.
|
|
Suppose <x,y> is in IEXT<sub>SH</sub>(<code>rdfs:domain</code>) and
|
|
<u,v> is in IEXT<sub>SH</sub>(x); then D must contain the triples</p>
|
|
<p><em>sur</em>(x<code>) rdfs:domain </code><em>sur</em>(y<code>) .<br />
|
|
</code><em>sur</em>(u)<em> </em>x <em>sur</em>(v)<code>.</code></p>
|
|
<p>so x must be a URIref, so <em>sur</em>(x)=x; and then by rule <a href="#rulerdfs2" class="termref">rdfs2</a>,
|
|
it must also contain the triple</p>
|
|
<p><em>sur</em>(u)<code> rdf:type</code> <em>sur</em>(y)<code>.</code></p>
|
|
<p>so IEXT<sub>SH</sub>(<code>rdf:type</code>) contains <u,v> ; so the
|
|
condition is satisfied.</p>
|
|
<p>The other cases proceed similarly, by translating the semantic condition
|
|
into a derivation using the rules and axiomatic triples. The argument forms
|
|
are summarized in the following table. Some of the semantic conditions split
|
|
into several subconditions, and some also have special subcases.</p>
|
|
<table border="1">
|
|
<tr>
|
|
<td ><strong>RDFS semantic condition</strong></td>
|
|
<td colspan="2" ><strong>Derivation</strong></td>
|
|
</tr>
|
|
<tr>
|
|
<td rowspan="4">if x in IR then<br /> <x,rdfs:Resource> in IEXT(rdf:type)</td>
|
|
<td >URIref or bnode in subject:<br />
|
|
x a b<br />
|
|
x rdf:type rdfs:Resource</td>
|
|
<td ><br /> <br />
|
|
<a href="#rulerdfs4" class="termref">rdfs4a</a></td>
|
|
</tr>
|
|
<tr>
|
|
<td > Literal:<br />
|
|
_:x rdf:type rdfs:Literal<br />
|
|
rdfs:type rdfs:range rdfs:Class<br />
|
|
rdfs:Literal rdf:type rdfs:Class<br />
|
|
rdfs:Literal rdfs:subClassOf rdfs:Resource<br />
|
|
_:x rdf:type rdfs:Resource</td>
|
|
<td><br />
|
|
see below<br />
|
|
axiomatic<br />
|
|
<a href="#rulerdfs3" class="termref">rdfs3</a><br />
|
|
<a href="#rulerdfs8" class="termref">rdfs8</a><br />
|
|
<a href="#rulerdfs9" class="termref">rdfs9</a></td>
|
|
</tr>
|
|
<tr>
|
|
<td>URIref or bnode in object:<br />
|
|
a b x<br />
|
|
x rdf:type rdfs:Resource</td>
|
|
<td><br /> <br />
|
|
<a href="#rulerdfs4" class="termref">rdfs4b</a></td>
|
|
</tr>
|
|
<tr>
|
|
<td><p>URIref in predicate:<br />
|
|
a x b<br />
|
|
x rdf:type rdf:Property<br />
|
|
rdf:type rdfs:domain rdfs:Resource<br />
|
|
x rdf:type rdfs:Resource</p></td>
|
|
<td><br /> <br />
|
|
<a href="#rulerdf1" class="termref">rdf1</a><br />
|
|
axiomatic<br />
|
|
<a href="#rulerdfs2" class="termref">rdfs2</a></td>
|
|
</tr>
|
|
<tr>
|
|
<td rowspan="2">x in LV iff<br /> <x,rdfs:Literal> in IEXT(rdf:type)</td>
|
|
<td>well-typed XML literal lll:<br />
|
|
a b lll<br />
|
|
_:x rdf:type rdf:XMLLiteral<br />
|
|
rdf:XMLLiteral rdfs:subClassOf rdfs:Literal<br />
|
|
_:x rdf:type rdfs:Literal</td>
|
|
<td><br /> <br />
|
|
<a href="#ruleslg" class="termref">lg</a>, <a href="#rulerdf2" class="termref">rdf2</a>,
|
|
<em>sur</em>(<em>xml</em>(lll))=_:x <br />
|
|
axiomatic<br />
|
|
<a href="#rulerdfs9" class="termref">rdfs9</a></td>
|
|
</tr>
|
|
<tr>
|
|
<td><p>other literal lll :<br />
|
|
a b lll<br />
|
|
_:x rdf:type rdfs:Literal</p></td>
|
|
<td><br /> <br />
|
|
<a href="#ruleslg" class="termref">lg</a>, <a href="#rulerdfs1" class="termref">rdfs1</a>,
|
|
<em>sur</em>(lll)=_:x </td>
|
|
</tr>
|
|
<tr>
|
|
<td>if <br /> <x,y> in IEXT(rdfs:domain) and <u,v> in IEXT(x)
|
|
<br />
|
|
then <br /> <u,y> in IEXT(rdf:type)</td>
|
|
<td>x rdfs:domain y .<br />
|
|
u x v .<br />
|
|
u rdf:type y . </td>
|
|
<td><br /> <br />
|
|
<a href="#rulerdfs2" class="termref">rdfs2</a></td>
|
|
</tr>
|
|
<tr>
|
|
<td>if <br /> <x,y> in IEXT(rdfs:range) and <u,v> in IEXT(x)
|
|
<br />
|
|
then <br /> <v,y> in IEXT(rdf:type)</td>
|
|
<td>x rdfs:range y .<br />
|
|
u x v .<br />
|
|
v rdf:type y . </td>
|
|
<td><br /> <br />
|
|
<a href="#rulerdfs3" class="termref">rdfs3</a></td>
|
|
</tr>
|
|
<tr>
|
|
<td><p>if<br />
|
|
<x,rdf:Property> in IEXT(rdf:type)<br />
|
|
then<br />
|
|
<x,x> in IEXT(rdfs:subPropertyOf)</p></td>
|
|
<td>x rdf:type rdf:Property<br />
|
|
x rdfs:subPropertyOf x</td>
|
|
<td><br />
|
|
<a href="#rulerdfs6" class="termref">rdfs6</a></td>
|
|
</tr>
|
|
<tr>
|
|
<td>if<br /> <x,rdf:Property> in IEXT(rdf:type)<br /> <y,rdf:Property>
|
|
in IEXT(rdf:type)<br /> <z,rdf:Property> in IEXT(rdf:type)<br />
|
|
<x,y> in IEXT(rdfs:subPropertyOf)<br /> <y,z> in IEXT(rdfs:subPropertyOf)<br />
|
|
then<br /> <x,z> in IEXT(rdfs:subPropertyOf)</td>
|
|
<td>x rdfs:subPropertyOf y<br />
|
|
y rdfs:subPropertyOf z<br />
|
|
x subPropertyOf z</td>
|
|
<td><br /> <br />
|
|
<a href="#rulerdfs5" class="termref">rdfs5</a></td>
|
|
</tr>
|
|
<tr>
|
|
<td><p>if<br />
|
|
<x,y> in IEXT(rdfs:subPropertyOf)<br />
|
|
<u,v> in IEXT(x)<br />
|
|
then<br />
|
|
<x,rdf:Property> in IEXT(rdf:type)<br />
|
|
<y,rdf:Property> in IEXT(rdf:type)<br />
|
|
<u,v> in IEXT(y)</p></td>
|
|
<td>x rdfs:subPropertyOf y<br />
|
|
u x v<br />
|
|
rdfs:subPropertyOf rdfs:domain rdf:Property<br />
|
|
x type rdf:Property<br />
|
|
rdfs:subPropertyOf rdfs:domain rdf:Property<br />
|
|
y rdf:type rdf:Property<br />
|
|
u y v</td>
|
|
<td><br /> <br />
|
|
axiomatic triple<br />
|
|
<a href="#rulerdfs2" class="termref">rdfs2</a><br />
|
|
axiomatic triple<br />
|
|
<a href="#rulerdfs3" class="termref">rdfs3</a><br />
|
|
<a href="#rulerdfs7" class="termref">rdfs7</a></td>
|
|
</tr>
|
|
<tr>
|
|
<td>if<br /> <x,rdfs:Class> in IEXT(rdf:type)<br />
|
|
then<br /> <x,rdfs:Resource> in IEXT(rdfs:subClassOf)</td>
|
|
<td>x rdf:type rdfs:Class<br />
|
|
x rdfs:subClassOf rdfs:Resource</td>
|
|
<td><br />
|
|
<a href="#rulerdfs8" class="termref">rdfs8</a></td>
|
|
</tr>
|
|
<tr>
|
|
<td><p>if<br />
|
|
<x,y> in IEXT(rdfs:subClassOf)<br />
|
|
<u,x> in IEXT(rdf:type)<br />
|
|
then<br />
|
|
<x,rdfs:Class> in IEXT(rdf:type)<br />
|
|
<y,rdfs:Class> in IEXT(rdf:type)<br />
|
|
<u,y> in IEXT(rdf:type) </p></td>
|
|
<td><p>x rdfs:subClassOf y<br />
|
|
u rdf:type x<br />
|
|
rdfs:subClassOf rdfs:domain rdfs:Class<br />
|
|
x rdf:type rdfs:Class<br />
|
|
rdfs:subClassOf rdfs:range rdfs:Class<br />
|
|
y rdf:type rdfs:Class<br />
|
|
u rdf:type y</p></td>
|
|
<td><br /> <br />
|
|
axiomatic triple<br />
|
|
<a href="#rulerdfs2" class="termref">rdfs2</a><br />
|
|
axiomatic triple<br />
|
|
<a href="#rulerdfs3" class="termref">rdfs3</a><br />
|
|
<a href="#rulerdfs9" class="termref">rdfs9</a></td>
|
|
</tr>
|
|
<tr>
|
|
<td>if<br /> <x,rdfs:Class> in IEXT(rdf:type)<br />
|
|
then<br /> <x,x> in IEXT(rdfs:subClassOf)</td>
|
|
<td>x rdf:type rdfs:Class<br />
|
|
x rdfs:subClassOf x</td>
|
|
<td><br />
|
|
<a href="#rulerdfs10" class="termref">rdfs10</a></td>
|
|
</tr>
|
|
<tr>
|
|
<td>if<br /> <x,rdfs:Class> in IEXT(rdf:type)<br /> <y,rdfs:Class>
|
|
in IEXT(rdf:type)<br /> <z,rdfs:Class> in IEXT(rdf:type)<br /> <x,y>
|
|
in IEXT(rdfs:subClassOf)<br /> <y,z> in IEXT(rdfs:subClassOf)<br />
|
|
then<br /> <x,z> in IEXT(rdfs:subClassOf)</td>
|
|
<td>x rdfs:subClassOf y<br />
|
|
y rdfs:subClassOf z<br />
|
|
x rdfs:subClassOf z</td>
|
|
<td><br /> <br />
|
|
<a href="#rulerdfs11" class="termref">rdfs11</a></td>
|
|
</tr>
|
|
<tr>
|
|
<td>if<br /> <x,rdfs:ContainerMembershipProperty> in IEXT(rdf:type)<br />
|
|
then<br /> <x,rdfs:member> in IEXT(rdfs:subPropertyOf)</td>
|
|
<td>x rdf:type rdfs:ContainerMembershipProperty<br />
|
|
x rdfs:subPropertyOf rdfs:member</td>
|
|
<td><br />
|
|
<a href="#rulerdfs12" class="termref">rdfs12</a></td>
|
|
</tr>
|
|
<tr>
|
|
<td>if<br /> <x,rdfs:Datatype> in IEXT(rdf:type)<br />
|
|
then<br /> <x,rdfs:Literal> in IEXT(rdfs:subClassOf)</td>
|
|
<td>x rdf:type rdfs:Datatype<br />
|
|
x rdfs:subClassOf rdfs:Literal</td>
|
|
<td><br />
|
|
<a href="#rulerdfs13" class="termref">rdfs13</a></td>
|
|
</tr>
|
|
</table>
|
|
<p>so SH is an rdfs-interpretation. </p>
|
|
<p>Since S rdfs-entails E, SH satisfies E: so for some mapping A from the blank
|
|
nodes of E to IR<sub>SH</sub>, [SH+A] satisfies every triple <br />
|
|
s p o <code>.</code><br />
|
|
in E, i.e. IEXT<sub>SH</sub>(p) contains <[SH+A](s),[SH+A](o)>, i.e.D
|
|
contains a triple </p>
|
|
<p><em>sur</em>([SH+A](s)) p <em>sur</em>([SH+A](o))<code>.</code></p>
|
|
<p>which is an instance of the first triple under the instantiation mapping
|
|
x -> <em>sur</em>(A(x)), unless o is a literal. If o is a
|
|
literal, then <em>sur</em>([SH+A](o) is the blank node
|
|
allocated to o, and so D also contains the triple </p>
|
|
<p><em>sur</em>([SH+A](s)) p o <code>.</code></p>
|
|
<p>which is an instance of the first triple under the instantiation mapping
|
|
x -> <em>sur</em>(A(x)). So a subgraph of D is an instance of E under
|
|
the instantiation mapping
|
|
x -> <em>sur</em>(A(x)); so D simply entails E.</p>
|
|
<p>So either D contains an XML clash or D simply entails E, so D satisfies the
|
|
conditions of the lemma.</p>
|
|
<p><strong>QED</strong></p>
|
|
</blockquote>
|
|
<p>Note that if E is finite, or if D contains an XML clash, then a finite subgraph
|
|
of D also satisfies the conditions of the lemma.</p>
|
|
<h2><a name="gloss" id="gloss"></a>Appendix B: Glossary of Terms (Informative)</h2>
|
|
|
|
<p><strong><a name="glossAntecedent"
|
|
id="glossAntecedent"></a>Antecedent</strong> (n.) In an <a
|
|
href="#glossInference" class="termref">inference</a>, the
|
|
expression(s) from which the <a href="#glossConsequent"
|
|
class="termref">conclusion</a> is derived. In an <a
|
|
href="#glossEntail" class="termref">entailment</a> relation, the
|
|
entailer. Also <em>assumption</em>.</p>
|
|
|
|
<p><strong><a name="glossAssertion"
|
|
id="glossAssertion"></a>Assertion</strong> (n.) (i) Any expression
|
|
which is claimed to be true. (ii) The act of claiming something to
|
|
be true.</p>
|
|
|
|
<p><strong><a name="glossClass" id="glossClass"></a>Class</strong>
|
|
(n.) A general concept, category or classification. Something<a
|
|
href="#glossResource" class="termref"></a> used primarily to
|
|
classify or categorize other things. Formally, in RDF, a <a
|
|
href="#glossResource" class="termref">resource</a> of type
|
|
<code>rdfs:Class</code> with an associated set of <a
|
|
href="#glossResource" class="termref">resources</a> all of which
|
|
have the class as a value of the <code>rdf:type</code> property.
|
|
Classes are often called 'predicates' in the formal logical
|
|
literature.</p>
|
|
|
|
<p>(RDF distinguishes <em>class</em> from <em>set</em>, although the two are often
|
|
identified. Distinguishing classes from sets allows RDF more
|
|
freedom in constructing class hierarchies, as <a
|
|
href="#technote">explained earlier</a>.)</p>
|
|
<p><strong><a name="glossComplete"
|
|
id="glossComplete"></a>Complete</strong> (adj., of an inference system). (1)
|
|
Able to detect all <a
|
|
href="#glossEntail" class="termref">entailment</a>s between any two expressions.
|
|
(2) Able to draw all <a href="#glossValid"
|
|
class="termref">valid</a> inferences. See <a href="#glossInference"
|
|
class="termref"><em>Inference</em></a>. Also used with a qualifier: able to
|
|
detect entailments or draw all <a href="#glossValid"
|
|
class="termref">valid</a> inferences in a certain limited form or kind (e.g.
|
|
between expressions in a certain normal form, or meeting certain syntactic conditions.)</p>
|
|
<p>(These definitions are not exactly equivalent, since the first requires that
|
|
the system has access to the consequent of the entailment, and may be unable
|
|
to draw 'trivial' inferences such as (p and p) from p. Typically, efficient
|
|
mechanical inference systems may be complete in the first sense but not necessarily
|
|
in the second.) </p>
|
|
|
|
<p><strong><a name="glossConsequent"
|
|
id="glossConsequent"></a>Consequent</strong> (n.) In an inference,
|
|
the expression constructed from the <a href="#glossAntecedent"
|
|
class="termref">antecedent</a>. In an entailment relation, the
|
|
entailee. Also <em>conclusion</em>.</p>
|
|
<p><strong><a name="glossConsistent"
|
|
id="glossConsistent"></a>Consistent</strong> (adj., of an expression) Having
|
|
a satisfying <a href="#glossInterpretation"
|
|
class="termref">interpretation</a>; not internally contradictory. (Also used
|
|
of an inference system as synonym for <em>Correct</em>.) </p>
|
|
<p><strong><a name="glossCorrect"
|
|
id="glossCorrect"></a>Correct</strong> (adj., of an inference system). Unable
|
|
to draw any invalid inferences, or unable to make false claims of entailment. See <em>Inference</em>.</p>
|
|
<p><strong><a name="glossDecideable" id="glossDecideable"></a>Decideable</strong>
|
|
(adj., of an inference system). Able to determine for any pair of expressions,
|
|
in a finite time with finite resources, whether or not the first entails the
|
|
second. (Also: adj., of a logic:) Having a decideable inference system which
|
|
is complete and correct for the semantics of the logic.</p>
|
|
<p>(Not all logics can have inference systems which are both complete and decideable,
|
|
and decideable inference systems may have arbitrarily high computational complexity.
|
|
The relationships between logical syntax, semantics and complexity of an inference
|
|
system continue to be the subject of considerable research.)</p>
|
|
|
|
<p><strong><a name="glossEntail"
|
|
id="glossEntail"></a>Entail</strong> (v.),
|
|
<strong>entailment</strong> (n.). A semantic relationship between
|
|
expressions which holds whenever the truth of the first guarantees
|
|
the truth of the second. Equivalently, whenever it is logically
|
|
impossible for the first expression to be true and the second one
|
|
false. Equivalently, when any <a href="#glossInterpretation"
|
|
class="termref">interpretation</a> which <a href="#glossSatisfy"
|
|
class="termref">satisfies</a> the first also satisfies the second.
|
|
(Also used between a set of expressions and an expression.)</p>
|
|
|
|
<p><strong><a name="glossEquivalent"
|
|
id="glossEquivalent"></a>Equivalent</strong> (prep., with
|
|
<em>to</em>) True under exactly the same conditions; making
|
|
identical claims about the world, when asserted. <a
|
|
href="#glossEntail" class="termref">Entails</a> and is entailed
|
|
by.</p>
|
|
|
|
<p><strong><a name="glossExtensional"
|
|
id="glossExtensional"></a>Extensional</strong> (adj., of a logic) A
|
|
set-based theory or logic of classes, in which classes are
|
|
considered to be sets, properties considered to be sets of
|
|
<object, value> pairs, and so on. A theory which admits no
|
|
distinction between entities with the same extension. See <a
|
|
href="#glossIntensional"
|
|
class="termref"><em>Intensional</em></a>.</p>
|
|
|
|
<p><strong><a name="glossFormal"
|
|
id="glossFormal"></a>Formal</strong> (adj.) Couched in language
|
|
sufficiently precise as to enable results to be established using
|
|
conventional mathematical techniques.</p>
|
|
|
|
<p><strong><a name="glossIff" id="glossIff"></a>Iff</strong>
|
|
(conj.) Conventional abbreviation for 'if and only if'. Used to
|
|
express necessary and sufficient conditions.</p>
|
|
<p><a name="glossInconsistent"
|
|
id="glossInconsistent"></a><strong>Inconsistent</strong> (adj.) False under
|
|
all interpretations; impossible to <a
|
|
href="#glossSatisfy" class="termref">satisfy</a>. <strong>Inconsistency</strong>
|
|
(n.), any inconsistent expression or graph.</p>
|
|
<p>(<a
|
|
href="#glossEntail" class="termref">Entailment</a> and inconsistency are closely
|
|
related, since A entails B just when (A and not-B) is inconsistent, c.f. the
|
|
second definition for <a
|
|
href="#glossEntail" class="termref">entailment</a>. This is the basis of many
|
|
mechanical inference systems. </p>
|
|
<p>Although the definitions of <a href="#glossConsistent" class="termref">consistency</a>
|
|
and inconsistency are exact duals, they are computationally dissimilar. It is
|
|
often harder to detect consistency in all cases than to detect inconsistency
|
|
in all cases<a
|
|
href="#glossEntail" class="termref"></a>.)</p>
|
|
<p><strong><a name="glossIndexical"
|
|
id="glossIndexical"></a>Indexical</strong> (adj., of an expression) having
|
|
a meaning which implicitly refers to the context of use. Examples from English
|
|
include words like 'here', 'now', 'this'.</p>
|
|
<p><strong><a name="glossInference"
|
|
id="glossInference"></a>Infer</strong><strong>ence</strong> (n.) An act or
|
|
process of constructing new expressions from existing expressions, or the result
|
|
of such an act or process. Inferences corresponding to <a href="#glossEntail"
|
|
class="termref">entailments</a> are described as <em>correct</em> or <em>valid</em>.
|
|
<strong>Inference rule</strong>, formal description of a type of inference;
|
|
<strong>inference system</strong>, organized system of inference rules; also,
|
|
software which generates inferences or checks inferences for validity.</p>
|
|
|
|
<p><strong><a name="glossIntensional"
|
|
id="glossIntensional"></a>Intensional</strong> (adj., of a logic)
|
|
Not <a href="#glossExtensional" class="termref">extensional</a>. A
|
|
logic which allows distinct entities with the same extension.</p>
|
|
|
|
|
|
<p>(The merits and demerits of intensionality have been extensively debated in
|
|
the philosophical logic literature. Extensional semantic theories are simpler,
|
|
and conventional semantics for formal logics usually assume an extensional view,
|
|
but conceptual analysis of ordinary language often suggests that intensional
|
|
thinking is more natural. Examples often cited are that an extensional logic
|
|
is obliged to treat all 'empty' extensions as identical, so must identify 'round
|
|
square' with 'santa clause', and is unable to distinguish concepts that 'accidentally'
|
|
have the same instances, such as human beings and bipedal hominids without body
|
|
hair. The semantics described in this document is basically intensional.)</p>
|
|
|
|
<p><strong><a name="glossInterpretation"
|
|
id="glossInterpretation"></a>Interpretation</strong>
|
|
(<strong>of</strong>) (n.) A minimal formal description of those
|
|
aspects of a <a href="#glossWorld" class="termref">world</a> which
|
|
is just sufficient to establish the truth or falsity of any
|
|
expression of a logic.</p>
|
|
|
|
<p>(Some logic texts distinguish between a <em>interpretation
|
|
structure</em>, which is a 'possible world' considered as something
|
|
independent of any particular vocabulary, and an <em>interpretation
|
|
mapping</em> from a vocabulary into the structure. The RDF
|
|
semantics takes the simpler route of merging these into a single
|
|
concept.)</p>
|
|
|
|
<p><strong><a name="glossLogic" id="glossLogic"></a>Logic</strong>
|
|
(n.) A formal language which expresses <a href="#glossProposition"
|
|
class="termref">propositions</a>.</p>
|
|
|
|
<p><a name="glossMetaphysical"
|
|
id="glossMetaphysical"></a><strong>Metaphysical</strong> (adj.).
|
|
Concerned with the true nature of things in some absolute or
|
|
fundamental sense.</p>
|
|
|
|
<p><a name="glossModeltheory"
|
|
id="glossModeltheory"></a><strong>Model Theory</strong> (n.) A
|
|
formal semantic theory which relates expressions to
|
|
interpretations.</p>
|
|
|
|
<p>(The name 'model theory' arises from the usage, traditional in
|
|
logical semantics, in which a satisfying interpretation is called a
|
|
"model". This usage is often found confusing, however, as it is
|
|
almost exactly the inverse of the meaning implied by terms like
|
|
"computational modelling", so has been avoided in this
|
|
document.)</p>
|
|
|
|
<p><strong><a name="glossMonotonic"
|
|
id="glossMonotonic"></a>Monotonic</strong> (adj., of a logic or
|
|
inference system) Satisfying the condition that if S entails E then
|
|
(S + T) entails E, i.e. adding information to some antecedents
|
|
cannot invalidate a <a href="#glossValid"
|
|
class="termref">valid</a> entailment.</p>
|
|
|
|
<p>(All logics based on a conventional <a href="#glossModeltheory"
|
|
class="termref">model theory</a> and a standard notion of
|
|
entailment are monotonic. Monotonic logics have the property that
|
|
entailments remain <a href="#glossValid"
|
|
class="termref">valid</a> outside of the context in which they were
|
|
generated. This is why RDF is designed to be monotonic.)</p>
|
|
|
|
<p><strong><a name="glossNonmonotonic"
|
|
id="glossNonmonotonic"></a>Nonmonotonic</strong> (adj.,of a logic
|
|
or inference system) Not <a href="#glossMonotonic"
|
|
class="termref">monotonic</a>. Non-monotonic formalisms have been
|
|
proposed and used in AI and various applications. Examples of
|
|
nonmonotonic inferences include <em>default reasoning</em>, where
|
|
one assumes a 'normal' general truth unless it is contradicted by
|
|
more particular information (birds normally fly, but penguins
|
|
don't fly); <em>negation-by-failure</em>, commonly assumed in logic
|
|
programming systems, where one concludes, from a failure to prove a
|
|
proposition, that the proposition is false; and <em>implicit
|
|
closed-world assumptions</em>, often assumed in database
|
|
applications, where one concludes from a lack of information about
|
|
an entity in some corpus that the information is false (e.g. that
|
|
if someone is not listed in an employee database, that he or she is not
|
|
an employee.)</p>
|
|
|
|
<p>(The relationship between monotonic and nonmonotonic inferences
|
|
is often subtle. For example, if a closed-world assumption is made
|
|
explicit, e.g. by asserting explicitly that the corpus is complete
|
|
and providing explicit provenance information in the conclusion,
|
|
then closed-world reasoning is monotonic; it is the implicitness
|
|
that makes the reasoning nonmonotonic. Nonmonotonic conclusions can
|
|
be said to be <a href="#glossValid"
|
|
class="termref">valid</a> only in some kind of 'context', and are liable
|
|
to be incorrect or misleading when used outside that context.
|
|
Making the context explicit in the reasoning and visible in the
|
|
conclusion is a way to map them into a monotonic framework.)</p>
|
|
|
|
<p><strong><a name="glossOntological"
|
|
id="glossOntological"></a>Ontological</strong> (adj.) (Philosophy)
|
|
Concerned with what kinds of things really exist. (Applied)
|
|
Concerned with the details of a formal description of some topic or
|
|
domain.</p>
|
|
|
|
<p><strong><a name="glossProposition"
|
|
id="glossProposition"></a>Proposition</strong> (n.) Something that
|
|
has a truth-value; a statement or expression that is true or
|
|
false.</p>
|
|
|
|
<p>(Philosophical analyses of language traditionally distinguish
|
|
propositions from the expressions which are used to state them, but
|
|
model theory does not require this distinction.)</p>
|
|
|
|
<p><strong><a name="glossReify" id="glossReify"></a>Reify</strong>
|
|
(v.), <strong>reification</strong> (n.) To categorize as an object;
|
|
to describe as an entity. Often used to describe a convention
|
|
whereby a syntactic expression is treated as a semantic object and
|
|
itself described using another syntax. In RDF, a reified triple is
|
|
a description of a triple-token using other RDF triples.</p>
|
|
|
|
<p><strong><a name="glossResource"
|
|
id="glossResource"></a>Resource</strong> (n.)(as used in RDF)(i) An
|
|
entity; anything in the universe. (ii) As a class name: the class
|
|
of everything; the most inclusive category possible.</p>
|
|
|
|
<p><strong><a name="glossSatisfy"
|
|
id="glossSatisfy"></a>Satisfy</strong> (v.t.),
|
|
<strong>satisfaction</strong>,(n.) <strong>satisfying</strong>
|
|
(adj., of an interpretation). To make true. The basic semantic
|
|
relationship between an interpretation and an expression. X
|
|
satisfies Y means that if <a href="#glossWorld" class="termref">the
|
|
world</a> conforms to the conditions described by X, then Y must be
|
|
true.</p>
|
|
|
|
<p><strong><a name="glossSemantic"
|
|
id="glossSemantic"></a>Semantic</strong> (adj.) ,
|
|
<strong>semantics</strong> (n.). Concerned with the specification
|
|
of meanings. Often contrasted with <em>syntactic</em> to emphasize
|
|
the distinction between expressions and what they denote.</p>
|
|
|
|
<p><a name="glossSkolemization" id="glossSkolemization"></a><a
|
|
href="#skolemlemprf"><strong>Skolemization</strong></a> (n.) A
|
|
syntactic transformation in which blank nodes are replaced by 'new'
|
|
names.</p>
|
|
|
|
<p>(Although not strictly <a href="#glossValid"
|
|
class="termref">valid</a>, Skolemization retains the
|
|
essential meaning of an expression and is often used in mechanical
|
|
inference systems. The full logical form is more complex. It is
|
|
named after the logician <a
|
|
href="http://www-gap.dcs.st-and.ac.uk/~history/Mathematicians/Skolem.html">
|
|
A. T. Skolem</a>)</p>
|
|
|
|
<p><a name="glossToken" id="glossToken"></a><strong>Token</strong>
|
|
(n.) A particular physical inscription of a symbol or expression in
|
|
a document. Usually contrasted with <em>type</em>, the abstract
|
|
grammatical form of an expression.</p>
|
|
|
|
<p><strong><a name="glossUniverse"
|
|
id="glossUniverse"></a>Universe</strong> (n., also <em>Universe of
|
|
discourse</em>) The universal classification, or the set of all
|
|
things that an interpretation considers to exist. In RDF/S, this is
|
|
identical to the set of resources.</p>
|
|
|
|
<p><strong><a name="glossUse" id="glossUse"></a>Use</strong> (v.)
|
|
contrasted with <em>mention</em>; to use a piece of syntax to
|
|
denote or refer to something else. The normal way that language is
|
|
used.</p>
|
|
|
|
<p>("Whenever, in a sentence, we wish to say something about a
|
|
certain thing, we have to use, in this sentence, not the thing
|
|
itself but its name or designation." - <a
|
|
href="http://www.philosophypages.com/dy/t.htm">Alfred
|
|
Tarski</a>)</p>
|
|
|
|
<p><strong><a name="glossValid" id="glossValid"></a>Valid</strong>
|
|
(adj., of an inference or inference process) Corresponding to an <a
|
|
href="#glossEntail" class="termref">entailment</a>, i.e. the
|
|
conclusion of the inference is entailed by the antecedent of the
|
|
inference. Also <em>correct</em>.</p>
|
|
|
|
<p><a name="glossWellformed"
|
|
id="glossWellformed"></a><strong>Well-formed</strong> (adj., of an
|
|
expression). Syntactically legal.</p>
|
|
|
|
<p><strong><a name="glossWorld" id="glossWorld"></a>World</strong>
|
|
(n.) (with <em>the:</em>) (i) The actual world. (with
|
|
<em>a:</em>) (ii) A way that the actual world might be arranged.
|
|
(iii) An <a href="#glossInterpretation"
|
|
class="termref">interpretation</a> (iv) A possible world.</p>
|
|
|
|
|
|
<p>(The metaphysical status of '<a
|
|
href="http://plato.stanford.edu/entries/actualism/possible-worlds.html">possible
|
|
worlds</a>' is highly controversial. Fortunately, one does not need to commit
|
|
oneself to a belief in parallel universes in order to use the concept in its
|
|
second and third senses, which are sufficient for semantic purposes.)</p>
|
|
|
|
|
|
<h2><a name="ack" id="ack"></a>Appendix C: Acknowledgements</h2>
|
|
<p>This document reflects the joint effort of the members of the <a
|
|
href="http://www.w3.org/2001/sw/RDFCore/">RDF Core Working Group</a>. Particular
|
|
contributions were made by Jeremy Carroll, Dan Connolly, Jan Grant, R. V. Guha,
|
|
Graham Klyne, Ora Lassilla, Brian McBride, Sergey Melnick, Jos deRoo and Patrick
|
|
Stickler. </p>
|
|
|
|
<p>The basic idea of using an explicit extension mapping to allow
|
|
self-application without violating the axiom of foundation was
|
|
suggested by Christopher Menzel.</p>
|
|
<p>Peter Patel-Schneider and Herman ter Horst found several major problems in
|
|
earlier drafts, and suggested several important technical improvements.</p>
|
|
<p>Patrick Hayes' work on this document was supported in part by DARPA under contract
|
|
#2507-225-22. </p>
|
|
<h2><a name="refs" id="refs">References</a></h2>
|
|
<h2><a name="normative" id="normative">Normative</a></h2>
|
|
|
|
|
|
<dl>
|
|
|
|
<dt><a id="ref-rdf-concepts"
|
|
name="ref-rdf-concepts"></a>[RDF-CONCEPTS]</dt>
|
|
<dd><cite><a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/">Resource Description Framework (RDF): Concepts and Abstract Syntax</a></cite>, Graham Klyne and Jeremy J. Carroll, Editors, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/ . <a href="http://www.w3.org/TR/rdf-concepts/">Latest version</a> available at http://www.w3.org/TR/rdf-concepts/ .</dd>
|
|
|
|
|
|
<dt><a id="ref-rdf-syntax"
|
|
name="ref-rdf-syntax"></a>[RDF-SYNTAX]</dt>
|
|
<dd><cite><a href="http://www.w3.org/TR/2004/REC-rdf-syntax-grammar-20040210/">RDF/XML Syntax Specification (Revised)</a></cite>, Dave Beckett, Editor, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-syntax-grammar-20040210/ . <a href="http://www.w3.org/TR/rdf-syntax-grammar/">Latest version</a> available at http://www.w3.org/TR/rdf-syntax-grammar/ .</dd>
|
|
|
|
<dt><a id="ref-rdf-tests"
|
|
name="ref-rdf-tests"></a>[RDF-TESTS]</dt>
|
|
<dd><cite><a href="http://www.w3.org/TR/2004/REC-rdf-testcases-20040210/">RDF Test Cases</a></cite>, Jan Grant and Dave Beckett, Editors, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-testcases-20040210/ . <a href="http://www.w3.org/TR/rdf-testcases/">Latest version</a> available at http://www.w3.org/TR/rdf-testcases/ .</dd>
|
|
|
|
|
|
<dt><a name="ref-rdfms" id="ref-rdfms"></a>[RDFMS]</dt>
|
|
<dd> <cite><a href="http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/">Resource
|
|
Description Framework (RDF) Model and Syntax Specification</a></cite> , O.
|
|
Lassila and R. Swick, Editors. World Wide Web Consortium. 22 February 1999.
|
|
This version is http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/. The <a href="http://www.w3.org/TR/REC-rdf-syntax/">latest
|
|
version of RDF M&S</a> is available at http://www.w3.org/TR/REC-rdf-syntax/.
|
|
</dd>
|
|
<dt><a id="ref-2119" name="ref-2119"></a>[RFC 2119]</dt>
|
|
<dd> <cite><a href="http://www.ietf.org/rfc/rfc2119.txt">RFC 2119 - Key words
|
|
for use in RFCs to Indicate Requirement Levels</a></cite> , S. Bradner, IETF.
|
|
March 1997. This document is http://www.ietf.org/rfc/rfc2119.txt. </dd>
|
|
<dt><a name="ref-2369" id="ref-2369"></a>[RFC 2396]</dt>
|
|
<dd><cite><a href="http://www.isi.edu/in-notes/rfc2396.txt">RFC 2396 - Uniform
|
|
Resource Identifiers (URI): Generic Syntax</a></cite> Berners-Lee,T., Fielding
|
|
and Masinter, L., August 1998</dd>
|
|
<dt><a id="ref-xmls" name="ref-xmls"></a>[XSD]</dt>
|
|
<dd><cite><a href="http://www.w3.org/TR/xmlschema-2/">XML Schema Part 2: Datatypes</a></cite>,
|
|
Biron, P. V., Malhotra, A. (Editors) World Wide Web Consortium Recommendation,
|
|
2 May 2001</dd>
|
|
</dl>
|
|
|
|
<h2><a name="nonnormative" id="nonnormative">Non-Normative</a></h2>
|
|
<dl>
|
|
<dt><a name="ref-owl" id="ref-owl"></a>[OWL]</dt>
|
|
<dd><cite><a href="http://www.w3.org/TR/2004/REC-owl-ref-20040210/">OWL Web Ontology Language Reference</a></cite>, Mike Dean and Guus Schreiber, Editors, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-owl-ref-20040210/ . <a href="http://www.w3.org/TR/owl-ref/">Latest version</a> available at http://www.w3.org/TR/owl-ref/ .</dd>
|
|
|
|
<dt><a id="ref-ConKla"
|
|
name="ref-ConKla"></a>[Conen&Klapsing]</dt>
|
|
<dd><cite><a
|
|
href="http://nestroy.wi-inf.uni-essen.de/rdf/logical_interpretation/index.html">
|
|
A Logical Interpretation of RDF</a></cite>, Conen, W., Klapsing, R..Circulated
|
|
to <a
|
|
href="http://lists.w3.org/Archives/Public/www-rdf-interest/2000Aug/0122.html">
|
|
RDF Interest Group</a>, August 2000.</dd>
|
|
<dt><a name="ref-daml" id="ref-daml">[DAML]</a></dt>
|
|
<dd>Frank van Harmelen, Peter F. Patel-Schneider, Ian Horrocks (editors), <a
|
|
href="http://www.daml.org/2001/03/reference.html"><em>Reference Description
|
|
of the DAML+OIL (March 2001) ontology markup language</em></a></dd>
|
|
<dt><a id="ref-HayMen"
|
|
name="ref-HayMen"></a>[Hayes&Menzel]</dt>
|
|
<dd><cite><a
|
|
href="http://reliant.teknowledge.com/IJCAI01/HayesMenzel-SKIF-IJCAI2001.pdf">
|
|
A Semantics for the Knowledge Interchange Format</a></cite>, Hayes, P., Menzel,
|
|
C., Proceedings of 2001 <a
|
|
href="http://reliant.teknowledge.com/IJCAI01/">Workshop on the IEEE Standard
|
|
Upper Ontology</a>, August 2001.</dd>
|
|
<dt><a name="ref-KIF" id="ref-KIF">[KIF]</a></dt>
|
|
<dd>Michael R. Genesereth et. al., <a
|
|
href="http://logic.stanford.edu/kif/dpans.html"><em>Knowledge Interchange
|
|
Format</em></a>, 1998 (draft American National Standard).</dd>
|
|
<dt><a id="ref-MarSaa"
|
|
name="ref-MarSaa"></a>[Marchiori&Saarela]</dt>
|
|
<dd><cite><a
|
|
href="http://www.w3.org/TandS/QL/QL98/pp/metalog.html">Query + Metadata
|
|
+ Logic = Metalog</a></cite>, Marchiori, M., Saarela, J. 1998.</dd>
|
|
<dt><a id="ref-Lbase" name="ref-Lbase"></a>[LBASE]</dt>
|
|
<dd><cite><a href="http://www.w3.org/TR/2003/NOTE-lbase-20031010/">Lbase: Semantics
|
|
for Languages of the Semantic Web</a></cite>, Guha, R. V., Hayes, P., W3C
|
|
Note, 10 October 2003.</dd>
|
|
<dt><a id="ref-daml-axiomat"
|
|
name="ref-daml-axiomat"></a>[McGuinness&al]</dt>
|
|
<dd><cite><a
|
|
href="http://www.ksl.stanford.edu/people/dlm/papers/daml-oil-ieee-abstract.html">
|
|
DAML+OIL:An Ontology Language for the Semantic Web</a></cite>, McGuinness,
|
|
D. L., Fikes, R., Hendler J. and Stein, L.A., IEEE Intelligent Systems, Vol.
|
|
17, No. 5, September/October 2002.</dd>
|
|
|
|
|
|
<dt><a id="ref-rdf-primer" name="ref-rdf-primer">[RDF-PRIMER]</a>
|
|
</dt>
|
|
<dd><cite><a href="http://www.w3.org/TR/2004/REC-rdf-primer-20040210/">RDF Primer</a></cite>, Frank Manola and Eric Miller, Editors, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-primer-20040210/ . <a href="http://www.w3.org/TR/rdf-primer/">Latest version</a> available at http://www.w3.org/TR/rdf-primer/ .</dd>
|
|
|
|
|
|
|
|
<dt><a id="ref-rdf-vocabulary"
|
|
name="ref-rdf-vocabulary"></a>[RDF-VOCABULARY]</dt>
|
|
|
|
<dd><cite><a href="http://www.w3.org/TR/2004/REC-rdf-schema-20040210/">RDF Vocabulary Description Language 1.0: RDF Schema</a></cite>, Dan Brickley and R. V. Guha, Editors, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-schema-20040210/ . <a href="http://www.w3.org/TR/rdf-schema/">Latest version</a> available at http://www.w3.org/TR/rdf-schema/ .</dd>
|
|
|
|
|
|
</dl>
|
|
<hr />
|
|
|
|
|
|
<h2><a id="changes" name="changes"></a><a name="change" id="change"></a>Appendix D: Change Log. (Informative)</h2>
|
|
<p><strong>Changes since the <a href="http://www.w3.org/TR/2003/PR-rdf-mt-20031215/">15 December 2003 Proposed Recommendation</a>.</strong></p>
|
|
<p>An error in the wording of the RDFS entailment lemma in appendix A was corrected.
|
|
Some typos in the glossary and main text were corrected.</p>
|
|
<p>After considering <a href="http://lists.w3.org/Archives/Public/www-rdf-comments/2003OctDec/0233.html">comments
|
|
by ter Horst</a>, the definition of D-interpretation has been modified so as
|
|
to apply to an extended vocabulary including the datatype names. </p>
|
|
<p>Older entries in the change log were removed. They can be found in <a href="http://www.w3.org/TR/2003/PR-rdf-mt-20031215/#change">the previous version.</a></p>
|
|
|
|
<hr />
|
|
|
|
<div class="metadata">
|
|
<p><a href="metadata.rdf"><img
|
|
src="http://www.w3.org/RDF/icons/rdf_metadata_button.40"
|
|
alt="RDF/XML Metadata" /></a></p>
|
|
<p>
|
|
<a href="http://validator.w3.org/check/referer"><img
|
|
src="http://www.w3.org/Icons/valid-xhtml10"
|
|
alt="Valid XHTML 1.0!" height="31" width="88" /></a>
|
|
</p>
|
|
<p>
|
|
<a href="http://jigsaw.w3.org/css-validator/">
|
|
<img style="border:0;width:88px;height:31px"
|
|
src="http://jigsaw.w3.org/css-validator/images/vcss"
|
|
alt="Valid CSS!"/>
|
|
</a>
|
|
</p>
|
|
</div>
|
|
</body>
|
|
</html>
|
|
|