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.
4002 lines
233 KiB
4002 lines
233 KiB
<?xml version="1.0" encoding="iso-8859-1"?>
|
|
<!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=iso-8859-1" />
|
|
<meta name="cvsid"
|
|
content="$Id: Overview.html,v 1.1 2003/09/04 17:02:12 vivien 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-WD" />
|
|
</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 Working Draft 5 September 2003</h2>
|
|
|
|
|
|
<dl>
|
|
<dt >This Version:</dt>
|
|
<dd><a
|
|
href="http://www.w3.org/TR/2003/WD-rdf-mt-20030905/">http://www.w3.org/TR/2003/WD-rdf-mt-20030905/</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/WD-rdf-mt-20030123/">http://www.w3.org/TR/2003/WD-rdf-mt-20030123/</a></dd>
|
|
<dt>Editor:</dt>
|
|
<dd><a href="http://www.coginst.uwf.edu/%7Ephayes/">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 class="copyright"><a
|
|
href="http://www.w3.org/Consortium/Legal/ipr-notice#Copyright">Copyright</a>
|
|
© 2003 <a href="http://www.w3.org/"><acronym
|
|
title="World Wide Web Consortium">W3C</acronym></a><sup>®</sup>
|
|
(<a href="http://www.lcs.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 class="newerstuff">and
|
|
corresponding complete systems of inference rules,</span> for the Resource Description
|
|
Framework (RDF) and RDF Schema (RDFS).</p>
|
|
|
|
<h2 >
|
|
<a id="status" name="status">Status of this Document</a>
|
|
</h2>
|
|
|
|
|
|
<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>
|
|
|
|
<p>This is a W3C <a href="http://www.w3.org/2003/06/Process-20030618/tr.html#RecsWD">Working Draft</a> of the <a href="http://www.w3.org/2001/sw/RDFCore/">RDF
|
|
Core Working Group</a> and has been produced as part of the W3C <a href="http://www.w3.org/2001/sw/">Semantic
|
|
Web Activity</a> (<a href="http://www.w3.org/2001/sw/Activity">Activity Statement</a>).</p>
|
|
<p> Detailed changes from the previous <a
|
|
href="http://www.w3.org/TR/2003/WD-rdf-mt-20030123/">23 January 2003 working
|
|
draft</a> are described in <a href="#change">Appendix E.</a> A notable change
|
|
since the Last Call publication is the simplification of typed literals to exclude
|
|
language tags. The Working Group particularly seeks feedback on the impact of
|
|
this change on the built-in datatype <code>rdf:XMLLiteral</code>. Other significant
|
|
changes to the semantic design are the use of 'intensional' conditions on <code>rdfs:subClassOf</code>
|
|
and <code>rdfs:subPropertyOf</code>, which allow simpler complete inference
|
|
rule sets, and the more elaborate treatment of datatypes.</p>
|
|
<p> This Working Draft consolidates changes and editorial improvements undertaken
|
|
in response to feedback received during the Last Call publication of the RDFCore
|
|
specifications which began on 23 January 2003. A
|
|
<a href="http://www.w3.org/2001/sw/RDFCore/20030123-issues/">list of the Last Call issues
|
|
addressed by the Working Group</a> is also available . This document has been endorsed
|
|
by the RDF Core Working Group. </p>
|
|
<p> This document is being released for review by W3C Members and other interested
|
|
parties to encourage feedback and comments, especially with regard to how the
|
|
changes made affect existing implementations and content. </p>
|
|
<p> In conformance with <a href="http://www.w3.org/Consortium/Process-20010719/#ipr">W3C
|
|
policy</a> requirements, known patent and <acronym title="Intellectual Property Rights">IPR</acronym>
|
|
constraints associated with this Working Draft are detailed on the
|
|
<a href="http://www.w3.org/2001/sw/RDFCore/ipr-statements" rel="disclosure">RDF
|
|
Core Working Group Patent Disclosure</a> page.</p>
|
|
<p> Comments on this document are invited and should be sent to the public mailing
|
|
list <a href="mailto:www-rdf-comments@w3.org">www-rdf-comments@w3.org</a>. An
|
|
archive of comments is available at <a href="http://lists.w3.org/Archives/Public/www-rdf-comments/">http://lists.w3.org/Archives/Public/www-rdf-comments/</a>.
|
|
</p>
|
|
<p> This is a public W3C Working Draft for review by W3C Members and
|
|
other interested parties. This section describes the status of this document
|
|
at the time of its publication.
|
|
Publication as a Working Draft does not imply endorsement by the W3C Membership. This is a draft
|
|
document and may be updated, replaced or obsoleted by other documents at any time. It is
|
|
inappropriate to cite this document as other than work in progress.
|
|
A list of current W3C Recommendations and other technical documents can be found
|
|
at <a href="/TR/">http://www.w3.org/TR/</a>. </p>
|
|
|
|
|
|
<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="#rdf_entail"></a><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="#rdf_entail">3.1. RDF Entailment</a><br />
|
|
<a href="#ReifAndCont">3.2 Reification, Containers,
|
|
Collections and rdf:value</a><br />
|
|
<a href="#Reif">3.2.1 Reification</a><br />
|
|
<a
|
|
href="#Containers">3.2.2 RDF Containers</a><br />
|
|
<a
|
|
href="#collections">3.2.3 RDF Collections</a><br />
|
|
<a
|
|
href="#rdfValue">3.2.4 rdf:value</a><br />
|
|
<a href="#rdfs_interp">4. Interpreting the RDFS Vocabulary</a><br />
|
|
<a href="#ExtensionalDomRang">4.1 Extensional
|
|
Semantic Conditions (Informative)</a><br />
|
|
<a href="#literalnote">4.2 A Note on rdfs:Literal</a><br />
|
|
<a href="#rdfs_entailment">4.3 RDFS Entailment</a><br />
|
|
<a href="#dtype_interp">5. Datatyped Interpretations</a><br />
|
|
<a
|
|
href="#D_entailment">5.1 D-Entailment</a><br />
|
|
<a href="#MonSemExt">6. Monotonicity of Semantic Extensions</a><br />
|
|
<a href="#rules">7. Entailment Rules</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 (Informative)</a><br />
|
|
<a href="#DtypeRules">7.4 Datatype Entailment Rules</a><br />
|
|
<a href="#Lbase">Appendix A. Translation into Lbase (Informative)</a><br />
|
|
<a href="#prf">Appendix B. Proofs of lemmas (Informative)</a><br />
|
|
<a href="#gloss">Appendix C. Glossary (Informative)</a><br />
|
|
<a href="#ack">Appendix D. Acknowledgements</a><br />
|
|
<a href="#refs">References</a><br />
|
|
<a href="#change">Appendix E. 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/2003/WD-rdf-concepts-20030905/">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 C 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>This document gives two versions of the same semantic theory: normatively in
|
|
the text, and also (informatively, in <a href="#Lbase">appendix A</a>) an 'axiomatic
|
|
semantics' in the form of a translation from RDF and RDFS into another formal
|
|
language, L<sub>base</sub> [<cite><a
|
|
href="#ref-Lbase">LBASE</a></cite>] which has a pre-defined model-theoretic
|
|
semantics. The translation technique offers some advantages and may be more
|
|
readable, so is described here as a convenience. The axiomatic semantic description
|
|
differs slightly from the normative model theory in the body of the text, as
|
|
noted in the appendix. The document also describes complete sets of inference
|
|
rules corresponding to the semantics decribed in the text. </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. 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 and RDF entailment described in
|
|
sections 1 and 3.1 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>],
|
|
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/2003/WD-rdf-concepts-20030905/#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/2003/WD-rdf-concepts-20030905/#section-Graph-URIref"><em>URI reference</em></a>,
|
|
<a
|
|
href="http://www.w3.org/TR/2003/WD-rdf-concepts-20030905/#section-Graph-Literal"><em> literal</em></a>,
|
|
<a
|
|
href="http://www.w3.org/TR/2003/WD-rdf-concepts-20030905/#section-Graph-Literal"><em>plain
|
|
literal</em></a>, <a
|
|
href="http://www.w3.org/TR/2003/WD-rdf-concepts-20030905/#section-Graph-Literal"><em>typed
|
|
literal</em></a>, <a href="http://www.w3.org/TR/2003/WD-rdf-concepts-20030905/#dfn-rdf-XMLLiteral"><em>XML
|
|
literal</em></a>,<a href="http://www.w3.org/TR/2003/WD-rdf-concepts-20030905/#XMLLiteral-mapping">
|
|
<em>XML data corresponding to,</em></a> <a href="http://www.w3.org/TR/2003/WD-rdf-concepts-20030905/#section-rdf-graph"><em>node</em></a>,
|
|
<a href="http://www.w3.org/TR/2003/WD-rdf-concepts-20030905/#section-blank-nodes"><em>blank node</em></a>,
|
|
<a
|
|
href="http://www.w3.org/TR/2003/WD-rdf-concepts-20030905/#xtocid103646"><em>triple</em></a>
|
|
<span >and <a href="http://www.w3.org/TR/2003/WD-rdf-concepts-20030905/#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 in Normal Form C, and
|
|
'language tag' in the sense of RFC 3066, c.f. <a href="http://www.w3.org/TR/2003/WD-rdf-concepts-20030905/#section-Graph-Literal">section
|
|
6.5</a> in [<cite><a href="#ref-rdf-concepts">RDF-CONCEPTS</a></cite>]. </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/2003/WD-rdf-concepts-20030905/#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/2003/WD-rdf-concepts-20030905/#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 typed
|
|
literal.</a> A name is <em>from</em> a vocabulary V if it is a URI reference
|
|
in V or a typed literal containing an internal type URI reference in V. <a name="defnamesof" id="defnamesof">The
|
|
<em>names of</em> a graph</a> are all the <a href="#defname" class="termref">name</a>s
|
|
which occur in the graph. These are the expressions that need to be assigned
|
|
a meaning by an <a href="#glossInterpretation"
|
|
class="termref">interpretation</a>. Plain literals are not classified as names
|
|
because their interpretation is fixed. Note that a typed literal <span class="newstuff">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 <a href="#defnamesof" class="termref">names of</a> 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 a plain
|
|
literal, or two blank nodes in the graph have been mapped into the same node
|
|
in the instance. An instance is proper just when the instance mapping M is not
|
|
invertible. </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/2003/WD-rdf-concepts-20030905/#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 name="defmerg" id="defmerg"> <span class="newstuff">The <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 merge is the union of the graphs; if they do
|
|
share blank nodes, then it is the union of a set of graphs which is 1:1 with
|
|
the original set of graphs, each of which is equivalent in the above sense to
|
|
one graph in the original set, and which share no blank nodes. This is often
|
|
described by saying that the blank nodes have been 'standardized apart'</span></a><span class="newstuff">.
|
|
Using the convention on equivalent graphs and identity, any graph in the original
|
|
set is considered to be a subgraph of the merge. </span></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 heirarchy 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>
|
|
|
|
<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 class="newstuff"> 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>, which
|
|
denote <a href="//www.w3.org/TR/2002/REC-xml-exc-c14n-20020718/"> exclusive
|
|
Canonical XML</a> [<cite><a href="#ref-C14N">XML-C14N</a></cite>] described
|
|
by the literal string: see <a href="http://www.w3.org/TR/2003/WD-rdf-concepts-20030905/">RDF:
|
|
Concepts and Abstract Syntax</a> [<cite><a href="#ref-rdf-concepts">RDF-CONCEPTS</a></cite>]
|
|
for exact details.</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/2003/WD-rdf-concepts-20030905/#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 width="97%" 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 at least all character strings and all pairs consisting
|
|
of a character string and a <a href="http://www.w3.org/TR/2003/WD-rdf-concepts-20030905/#section-Graph-Literal" class="termref">language
|
|
tag</a>.</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">noted</a> earlier.</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 those listed.
|
|
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 badly typed
|
|
literals are <a href="#illformedliteral">required to denote a <em>non</em>-literal value.</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, i.e. that the terms equated are the same. </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" then
|
|
I(E) = aaa</td>
|
|
</tr>
|
|
<tr>
|
|
<td class="semantictable">if E is a plain literal "aaa"@ttt
|
|
then I(E) = <aaa, ttt></td>
|
|
</tr>
|
|
|
|
<tr>
|
|
|
|
<td class="semantictable">if E is a typed literal then I(E) = IL(E)</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td class="semantictable">if E is a URI reference then I(E) = IS(E)</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
|
|
<td class="semantictable"><p>if E is a triple s p o . 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 URI references 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, ex:b, ex:c</code>} plus all typed literals
|
|
with one of these as the type URI. 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 class="newstuff">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: any typed literal <code>=></code>2 </p>
|
|
|
|
<div class="c1">
|
|
<p><img src="RDF_semantics_fig_1.jpg"
|
|
alt="A drawing of the domains and mappings described in the text"
|
|
width="495" height="390" /><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
|
|
B</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 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 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 class="newstuff">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
|
|
of the vocabulary of (S union E) 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">appendix B. Proofs of lemmas</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.</p>
|
|
<p><a name="subglem" id="subglem"><strong>Subgraph
|
|
Lemma.</strong></a> A graph entails all its <a
|
|
href="#defsubg" class="termref">subgraphs</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>.</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.</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></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'.</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.</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 class="newstuff">2.1
|
|
Vocabulary interpretations and vocabulary entailment</span></h3>
|
|
<p class="newstuff">Simple interpretations and simple entailment capture the semantics
|
|
of RDF graphs when no attention is paid to the particular meaning of any 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>
|
|
|
|
<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 width="85%" 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="defCRDFV" id="defCRDFV"></a>The subset of <a href="#defRDFV" class="termref">rdfV</a>
|
|
consisting of the first 3 items in the above list, {<span class="othertable"><code>rdf:type</code>
|
|
<code>rdf:Property rdf:XMLLiteral</code></span>} is called the
|
|
<em>central RDF vocabulary</em>, crdfV. </p>
|
|
<p><a href="#rdfinterpdef" class="termref">rdf-interpretation</a>s impose extra
|
|
semantic conditions on <a href="#defCRDFV" class="termref">crdfV</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/2003/WD-rdf-concepts-20030905/#section-XMLLiteral">fully
|
|
described</a> in the <i><a href="http://www.w3.org/TR/2003/WD-rdf-concepts-20030905">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/2003/WD-rdf-concepts-20030905/#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 class="newstuff">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="#defCRDFV" class="termref">crdfV)</a></span>
|
|
which satisfies the extra conditions described in the following table for all
|
|
<a href="#defname" class="termref">name</a>s in (V<span > union <a href="#defCRDFV" class="termref">crdfV</a></span>),
|
|
<span >and all the triples in the subsequent table whose vocabulary is contained
|
|
in (V union <a href="#defCRDFV" class="termref">crdfV)</a>. These triples are
|
|
called the <em>rdf axiomatic triples</em>. </span></p>
|
|
|
|
<div class="title">RDF semantic conditions.</div>
|
|
<table width="86%" 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 class="newerstuff">value</span> corresponding to 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 not a well-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 width="86%" 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.1. RDF entailment</h3>
|
|
<p>S <i>rdf-entails</i> E when every rdf-interpretation of the vocabulary of S
|
|
union E 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 class="newstuff">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.2. 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.2.1 Reification</a></h4>
|
|
|
|
<div class="c1">
|
|
<table width="51%" 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 class="newerstuff">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.2.2 RDF
|
|
containers</a></h4>
|
|
|
|
<table width="41%" 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.2.3 RDF
|
|
collections</h4>
|
|
|
|
<table width="34%" 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.2.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 <cite><a
|
|
href="http://www.w3.org/TR/2002/WD-rdf-primer-20021111/">RDF Primer</a></cite>
|
|
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 class="newstuff">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>
|
|
|
|
|
|
<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 width="83%" 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 condiions, 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="#defCRDFV" class="termref">crdfV</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>, which contain only <a href="#defname" class="termref">name</a>s
|
|
from (V <span >union </span><a href="#defCRDFV" class="termref">crdfV</a> union
|
|
<a href="#defRDFSV" class="termref">rdfsV</a>).</p>
|
|
|
|
<div class="title">RDFS semantic conditions.</div>
|
|
<table width="84%" 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, IR> 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>)) and y is in ICEXT(x) then <y,
|
|
LV> is in IEXT(I(<code>rdf:type</code>))</p></td>
|
|
</tr>
|
|
</table>
|
|
|
|
<p><a id="RDFS_axiomatic_triples" name="RDFS_axiomatic_triples"> </a>
|
|
</p>
|
|
<div class="title">RDFS axiomatic triples.</div>
|
|
<table width="84%" 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 width="100%" 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 class="newerstuff">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 class="newerstuff"><code><ex:a> <ex:p> "<notLegalXML"^^rdf:XMLLiteral
|
|
.<br />
|
|
<ex:p> rdfs:range rdf:XMLLiteral .</code></p>
|
|
<p class="newerstuff">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.1 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" width="90%" 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.2 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 simple 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.3 RDFS Entailment</h3>
|
|
<p>S <i>rdfs-entails</i> E when every <a href="#rdfsinterpdef" class="termref">rdfs-interpretation</a>
|
|
of the vocabulary of S union E 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 class="newstuff">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 xxx.</p>
|
|
<p class="newerstuff">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"></a>5. Datatyped Interpretations</h2>
|
|
|
|
|
|
<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/2003/WD-rdf-concepts-20030905/#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 mapping</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 class="newstuff" >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/2003/WD-rdf-concepts-20030905/#dfn-rdf-XMLLiteral">defined</a>
|
|
in the <a href="http://www.w3.org/TR/2003/WD-rdf-concepts-20030905/"> 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 width="90%" 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 graph G is any
|
|
<a href="#rdfsinterpdef" class="termref">rdfs-interpretation</a> I of V, where V contains the vocabulary of G, which
|
|
satisfies the following
|
|
extra conditions for every pair <aaa, x> in D:</p>
|
|
<div class="title">General semantic conditions for datatypes.</div>
|
|
<table width="90%" 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
|
|
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 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 class="newerstuff">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 >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>The only <a
|
|
href="#glossInconsistent" class="termref">inconsistencies</a> recognized by
|
|
this <a
|
|
href="#glossModeltheory" class="termref">model theory</a> are datatype clashes,<span >
|
|
assertions that ill-typed literals are of type <code>rdfs:Literal</code></span>,
|
|
and that ill-typed XML literals are of type <code>rdf:XMLLiteral</code>. </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>.</p>
|
|
<h3 ><a name="D_entailment" id="D_entailment"></a>5.1 D-entailment</h3>
|
|
<p >S <em>D-entails</em> E when every <a href="#defDinterp" class="termref">D-interpretation</a>
|
|
of the vocabulary of S union E 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 class="newstuff"> 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 class="newstuff"><a name="rules" id="rules"></a></span>7. Entailment
|
|
rules</h2>
|
|
<p>This following tables list some inference patterns which capture some of the
|
|
various forms of vocabulary entailment. The rules all have 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, rather than a <a href="#defmerge" class="termref">merge</a>, with
|
|
the conclusion, and hence preserves any blank nodes already in the graph.</p>
|
|
<p>These rules all use the following conventions: uuu stands for any URI reference
|
|
or blank node identifier, vvv for any URI reference or literal, aaa, bbb, etc.,
|
|
for any URI reference, and xxx, yyy etc. for any URI reference, blank node identifier
|
|
or literal. </p>
|
|
<h3 ><a name="simpleRules" id="simpleRules"></a>7.1 Simple Entailment Rules</h3>
|
|
<p >The <a href="#instlem" class="termref">instance lemma</a> in <a href="#entail" class="termref">
|
|
Section 2</a> can be stated as inference rules on triples:</p>
|
|
<div class="title">simple entailment rules.</div>
|
|
<table width="98%" 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 vvv<code> .</code></td>
|
|
<td class="ruletable"><p>uuu aaa<code> _:</code>nnn<code> .</code></p>
|
|
where <code>_:</code>nnn is a blank node <span class="newstuff">identifier</span>
|
|
allocated to vvv by rule se1 or se2.</td>
|
|
</tr>
|
|
<tr>
|
|
<td class="ruletable" ><a name="rulese2" id="rulese2"></a>se2</td>
|
|
<td class="ruletable" >bbb aaa xxx<code> .</code></td>
|
|
<td class="ruletable" ><p><code>_:</code>nnn aaa xxx<code> .</code></p>
|
|
where <code>_:</code>nnn is a blank node <span class="newstuff">identifier
|
|
</span>allocated to bbb by rule se1 or se2.</td>
|
|
</tr>
|
|
</table>
|
|
<p ><a name="defAssociatedWith" id="defAssociatedWith"></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 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: the association between introduced blank nodes
|
|
and the URI reference or literal that they replace provides the instance mapping.
|
|
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 allocated 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
|
|
allocated 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 allocated to <code>ex:c</code> )</p>
|
|
<p >Applying these rules to a graph will produce a graph which is simply entailed
|
|
by the original. These rules will not generate all graphs which have the original
|
|
graph as an instance, which could include arbitrarily many blank-node triples
|
|
all of which instantiate back to the original triples. Modifying the rules so
|
|
that new blank nodes could be allocated to existing blank nodes would generate
|
|
all such graphs. </p>
|
|
<p ></p>
|
|
<h3 ><a name="RDFRules" id="RDFRules"></a>7.2 RDF Entailment Rules</h3>
|
|
<div class="title">RDF entailment rules</div>
|
|
<table width="100%" border="1" summary="RDF closure 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>xxx 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>xxx aaa lll <code>.</code></p>
|
|
where lll is a well-typed XML literal .</td>
|
|
<td><p>xxx aaa <code>_:</code>nnn <code>.<br />
|
|
_:</code>nnn <code>rdf:type rdf:XMLLiteral .</code></p>
|
|
<p>where _:nnn is a blank node <span class="newstuff">identifier</span>
|
|
<a href="#defAssociatedWith" class="termref">allocated to</a> lll by
|
|
this rule.</p></td>
|
|
</tr>
|
|
</tbody>
|
|
</table>
|
|
<p>Applying these and the earlier rules to a graph produces a graph which is rdf-entailed
|
|
by the original. Note also that the RDF axiomatic triples are valid in all <a href="#rdfinterpdef" class="termref">rdf-interpretation</a>s,
|
|
so these rules can be applied to them as well as to any triples in the graph.
|
|
</p>
|
|
<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 the <a href="#simpleRules" class="termref">simple entailment rules</a> and
|
|
<a href="#RDFRules" class="termref">RDF entailment rules</a> and which <a href="#defentail" class="termref">simply entails</a> E.<span class="newstuff"> </span>(<a href="#RDFEntailmentLemmaPrf" >Proof</a>
|
|
in Appendix B)</p>
|
|
<h3><a name="RDFSRules" id="RDFSRules"></a>7.3 RDFS Entailment Rules</h3>
|
|
<div class="title">RDFS entailment rules.</div>
|
|
<table width="100%" border="1" summary="RDFS closure 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>xxx aaa lll<code>.</code></p>
|
|
<p>where lll is a plain literal (with or without a language tag).</p></td>
|
|
<td><p>xxx aaa <code>_:</code>nnn<code>.<br />
|
|
_:</code>nnn <code></code> rdf:type rdfs:Literal <code>.</code></p>
|
|
<p>where <code>_:</code>nnn is a blank node <a href="#defAssociatedWith" class="termref">allocated
|
|
to</a> lll by this rule.</p></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs2" id="rulerdfs2"></a>rdfs2</td>
|
|
<td> <p>aaa <code>rdfs:domain</code> zzz <code>.</code><br />
|
|
xxx aaa yyy <code>.</code> </p></td>
|
|
<td>xxx <code>rdf:type</code> zzz <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs3" id="rulerdfs3"></a>rdfs3</td>
|
|
<td> <p>aaa <code>rdfs:range</code> zzz <code>.</code><br />
|
|
xxx aaa uuu <code>.</code> </p></td>
|
|
<td>uuu <code>rdf:type</code> zzz <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs4" id="rulerdfs4"></a>rdfs4a</td>
|
|
<td>xxx aaa yyy <code>.</code></td>
|
|
<td>xxx <code>rdf:type rdfs:Resource .</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td>rdfs4b</td>
|
|
<td>xxx aaa uuu <code>.</code></td>
|
|
<td>uuu <code>rdf:type rdfs:Resource .</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs5" id="rulerdfs5"></a>rdfs5</td>
|
|
<td> <p>aaa <code>rdfs:subPropertyOf</code> bbb <code>.</code><br />
|
|
bbb <code>rdfs:subPropertyOf</code> ccc <code>.</code></p></td>
|
|
<td>aaa <code>rdfs:subPropertyOf</code> ccc <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs6" id="rulerdfs6"></a>rdfs6</td>
|
|
<td>xxx <code>rdf:type rdf:Property .</code></td>
|
|
<td>xxx <code>rdfs:subPropertyOf</code> xxx <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 />
|
|
xxx aaa yyy <code>.</code> </p></td>
|
|
<td>xxx bbb yyy <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs8" id="rulerdfs8"></a>rdfs8</td>
|
|
<td> <p>xxx <code>rdf:type rdfs:Class .</code></p></td>
|
|
<td>xxx <code>rdfs:subClassOf rdfs:Resource .</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs9" id="rulerdfs9"></a>rdfs9</td>
|
|
<td> <p>xxx <code>rdfs:subClassOf</code> yyy <code>.</code><br />
|
|
aaa <code>rdf:type</code> xxx <code>.</code></p></td>
|
|
<td>aaa <code>rdf:type</code> yyy <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs10" id="rulerdfs10"></a>rdfs10</td>
|
|
<td>xxx <code>rdf:type rdfs:Class .</code></td>
|
|
<td>xxx <code>rdfs:subClassOf</code> xxx <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs11" id="rulerdfs11"></a>rdfs11</td>
|
|
<td> <p>xxx <code>rdfs:subClassOf</code> yyy <code>.</code><br />
|
|
yyy <code>rdfs:subClassOf</code> zzz <code>.</code></p></td>
|
|
<td>xxx <code>rdfs:subClassOf</code> zzz <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs12" id="rulerdfs12"></a>rdfs12</td>
|
|
<td>xxx <code>rdf:type rdfs:ContainerMembershipProperty .</code></td>
|
|
<td>xxx <code>rdfs:subPropertyOf rdfs:member .</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td><a name="rulerdfs13" id="rulerdfs13"></a>rdfs13</td>
|
|
<td>xxx <code>rdf:type rdfs:Datatype .</code></td>
|
|
<td>xxx <code>rdfs:subClassOf rdfs:Literal .</code></td>
|
|
</tr>
|
|
</tbody>
|
|
</table>
|
|
<p>These rules are <em><a href="#glossComplete" class="termref"> complete</a></em> in the following sense: </p>
|
|
<p><strong>RDFS entailment lemma</strong>. <span class="newerstuff">If S is rdfs-consistent,
|
|
then</span> 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 the <a href="#simpleRules" class="termref">simple</a>,
|
|
<a href="#RDFRules" class="termref">RDF</a> and <a href="#RDFSRules" class="termref">RDFS
|
|
entailment rules</a> and which <a href="#defentail" class="termref">simply entails</a>
|
|
E. (<a href="#RDFSEntailmentLemmaPrf" class="termref">Proof</a> in Appendix
|
|
B)</p>
|
|
<p>These rules are somewhat redundant. All but one of the <a href="#RDF_axiomatic_triples" class="termref">RDFaxiomatic
|
|
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; and rule <a href="#rulerdfs1" class="termref">rdfs1</a> subsumes cases of rule
|
|
<a href="#rulese1" class="termref">se1</a>
|
|
where vvv is a plain literal. </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
|
|
heirarchies, re-asserting them for all super-properties and superclasses. <a href="#rulerdfs1" class="termref">rdfs1</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>xxx <code>rdf:type rdfs:Resource .</code></p>
|
|
<p>for every xxx in V, and of the form</p>
|
|
<p>xxx <code>rdfs:subClassOf rdfs:Resource .</code></p>
|
|
<p>for every class name xxx; 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 (Informative)</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 width="100%" border="1">
|
|
<tr class="ruletable">
|
|
<td >ext1</td>
|
|
<td > <p>xxx <code>rdfs:domain</code> yyy <code>.<br />
|
|
</code> yyy <code>rdfs:subClassOf</code> zzz <code>.</code></p></td>
|
|
<td >xxx <code>rdfs:domain</code> zzz <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td>ext2</td>
|
|
<td> <p>xxx <code>rdfs:range</code> yyy <code>.<br />
|
|
</code> yyy <code>rdfs:subClassOf</code> zzz <code>.</code></p></td>
|
|
<td>xxx <code>rdfs:range</code> zzz <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td>ext3</td>
|
|
<td>xxx <code>rdfs:domain</code> yyy <code>.<br />
|
|
</code> zzz <code>rdfs:subPropertyOf</code> xxx <code>.</code></td>
|
|
<td>zzz <code>rdfs:domain </code>yyy <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td>ext4</td>
|
|
<td>xxx <code>rdfs:range</code> yyy <code>.<br />
|
|
</code> zzz <code>rdfs:subPropertyOf</code> xxx <code>.</code></td>
|
|
<td>zzz <code>rdfs:range</code> yyy <code>.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td >ext5</td>
|
|
<td><span ><code>rdf:type</code><code> rdfs:subPropertyOf</code> zzz<code>
|
|
.</code><br />
|
|
zzz <code>rdfs:domain</code> yyy<code> .</code> <br />
|
|
</span> </td>
|
|
<td ><code>rdfs:Resource </code><code>rdfs:subClassOf</code> yyy<code> .</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td >ext6</td>
|
|
<td><span ><code>rdfs:</code><code>subClassOf</code> <code>rdfs:subPropertyOf</code>
|
|
zzz<code> .</code><br />
|
|
zzz <code>rdfs:domain</code> yyy<code> .</code> <br />
|
|
</span> </td>
|
|
<td ><code>rdfs:Class</code> <code>rdfs:subClassOf</code> yyy<code> .</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td >ext7</td>
|
|
<td><span ><code>rdfs:subPropertyOf</code> <code>rdfs:subPropertyOf</code>
|
|
zzz<code> .</code><br />
|
|
zzz <code>rdfs:domain</code> yyy<code> .</code> <br />
|
|
</span> </td>
|
|
<td ><code>rdf:Property</code> <code>rdfs:subClassOf</code> yyy<code> .</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td >ext8</td>
|
|
<td><span ><code>rdfs:</code><code>subClassOf</code><code>rdfs:subPropertyOf</code>
|
|
zzz <code>.</code><br />
|
|
zzz <code>rdfs:range</code> yyy<code> .</code> <br />
|
|
</span> </td>
|
|
<td ><code>rdfs:Class</code> <code>rdfs:subClassOf</code> yyy<code> .</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td >ext9</td>
|
|
<td><span ><code>rdfs:subPropertyOf</code><code>rdfs:subPropertyOf</code>
|
|
zzz <code>.</code><br />
|
|
zzz <code>rdfs:range</code> yyy<code> .</code> <br />
|
|
</span> </td>
|
|
<td ><code>rdf:Property</code> <code>rdfs:subClassOf</code> yyy<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 width="90%" border="1" summary="datatype rule">
|
|
<tr class="ruletable">
|
|
<td >rdfD 1</td>
|
|
<td > <p>ddd <code>rdf:type rdfs:Datatype .</code><br />
|
|
aaa ppp "sss"^^ddd <code>.</code></p></td>
|
|
<td > <p>aaa ppp _:xxx <code>.</code><br />
|
|
_:xxx <code>rdf:type</code> ddd <code>.</code></p>
|
|
<p >where _:xxx is a blank node <span class="newstuff">identifier</span>
|
|
<a href="#defAssociatedWith" class="termref">allocated to</a> "sss"^^ddd
|
|
by this rule.</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 width="90%" border="1" summary="datatype rule2">
|
|
<tr class="ruletable">
|
|
<td >rdfD 2</td>
|
|
<td > <p>ddd <code>rdf:type rdfs:Datatype .</code><br />
|
|
aaa ppp "sss"^^ddd <code>.</code><br />
|
|
</p></td>
|
|
<td >aaa ppp "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 width="90%" border="1" summary="datatype rule3">
|
|
<tr class="ruletable">
|
|
<td >rdfD 3</td>
|
|
<td > <p>ddd <code>rdf:type rdfs:Datatype .</code><br />
|
|
eee <code>rdf:type rdfs:Datatype .</code><br />
|
|
aaa ppp "sss"^^ddd <code>.</code><br />
|
|
</p></td>
|
|
<td >aaa ppp "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>aaa ppp "sss"^^ddd .<br />
|
|
ddd rdf:type rdfs:Datatype .</code></p>
|
|
<p><code>aaa ppp _:xxx .<br />
|
|
_:xxx rdf:type ddd .</code> (by rule rdfD 1)<code><br />
|
|
ddd rdfs:subClassOf rdfs:Literal .</code> (by rule <a href="#rulerdfs11" class="termref">rdfs11</a>)<code><br />
|
|
_:xxx rdf:type rdfs:Literal .</code> (by rule <a href="#rulerdfs9" class="termref">rdfs9</a>)</p>
|
|
<p>The rule rdfD1 is sufficient to expose a datatype clash, by a chain of reasoning
|
|
of the following form:</p>
|
|
<p><code>ppp rdfs:range ddd .<br />
|
|
aaa ppp "sss"^^eee .</code></p>
|
|
<p><code>aaa ppp _:xxx .<br />
|
|
_:xxx rdf:type eee .</code> (by rule rdfD 1)<br />
|
|
<code>_:xxx rdf:type ddd .</code> (by rule <a href="#rulerdfs3" class="termref">rdfs3</a>)</p>
|
|
<p>These rules do 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 (eg <code>xsd:boolean</code> has only two elements, so anything
|
|
established for those two values must be true for all literals with this datatype.)<span class="newstuff">
|
|
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 string of characters 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 width="90%" border="1" summary="xsd strings are same as plain literals">
|
|
<tr class="ruletable">
|
|
<td class="newstuff" >xsd 1a</td>
|
|
<td class="newstuff">uuu aaa "sss"<code>.</code></td>
|
|
<td class="newstuff">uuu aaa "sss"^^<code>xsd:string
|
|
.</code></td>
|
|
</tr>
|
|
<tr class="ruletable">
|
|
<td class="newstuff">xsd 1b</td>
|
|
<td class="newstuff">uuu aaa "sss"^^<code>xsd:string .</code></td>
|
|
<td class="newstuff">uuu aaa "sss"<code>.</code></td>
|
|
</tr>
|
|
</table>
|
|
<p class="newstuff">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="Lbase" id="Lbase">Appendix A: Translation into L<sub>base</sub></a>.
|
|
(Informative) </h2>
|
|
<p>As noted in the introduction, an alternative way to specify <a href="#rdfinterpdef" class="termref">rdf-interpretation</a>s
|
|
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>]. Here a version of
|
|
first-order logic called L<sub>base</sub> [<cite><a href="#ref-Lbase">LBASE</a></cite>],
|
|
which has a particularly efficient syntax permitting quantification over relations
|
|
and predicates, is used. The axioms could be rendered into a conventional first-order
|
|
syntax by systematically rewriting every atom or term using a dummy predicate,
|
|
similar to the mapping used in [<cite><a
|
|
href="#ref-daml-axiomat">McGuinness&al</a></cite>].</p>
|
|
|
|
|
|
<p>To translate an RDF graph into L<sub>base</sub>, apply the following rules
|
|
to each expression noted. Each rule gives a translation <em>TR</em>[E] for the
|
|
expression E, to be applied recursively. To achieve a translation which reflects
|
|
a vocabulary entailment, add the axioms specified; except that the RDF translation
|
|
does not deal with XML typed literals, which are handled as a datatype in this
|
|
translation, for simplicity. Each vocabulary includes all axioms and rules for
|
|
preceding vocabularies, so that the RDFS translation of a graph should include
|
|
the RDF translation as well as the RDF and RDFS axioms, and so on. (Note, the
|
|
document [<cite><a href="#ref-Lbase">LBASE</a></cite>], written earlier, contains
|
|
a description of a different translation for illustrative purposes. The translation
|
|
given here is more accurate.)</p>
|
|
<p>This translation uses the L<sub>base</sub> special names <code><em>String</em></code>
|
|
and <code><em>NatNumber</em></code>, which are true respectively of Unicode
|
|
character strings and natural numbers, and it introduces some terminology in
|
|
order to give a logical account of the meanings implicit in the various literal
|
|
constructions. Note that special names are not URI references. The built-in
|
|
datatype <code>rdf:XMLLiteral</code> is treated uniformly with the other <a href="#defDatatype" class="termref">datatype</a>s,
|
|
later, so that the RDF translation given here is strictly incomplete as it stands.
|
|
The RDFS axioms use a predicate <code>LanguageTag</code> which is supposed to
|
|
be true of all and only the strings which are legal XML language tags; the axioms
|
|
would need to be supplemented by a suitable way of determining the truth of
|
|
instances of this predicate in order to be used to check RDF literal syntax
|
|
adequately.</p>
|
|
<p>L<sub>base</sub> allows a name to be enclosed in the characters '<' and
|
|
'>' if it would otherwise violate the L<sub>base</sub> syntax conventions,
|
|
for example a URI reference beginning with the symbol '('. An exact translation
|
|
for machine use would need to perform some more detailed lexical analysis.</p>
|
|
|
|
|
|
<table width="100%" border="1" summary="Lbase translation">
|
|
<caption>
|
|
L<sub>base</sub> translation rules <br/>
|
|
</caption>
|
|
<tr class="othertable">
|
|
<td ><strong>RDF expression E</strong></td>
|
|
<td ><strong>L<sub>base</sub> expression <em>TR</em>[E]</strong><br/></td>
|
|
</tr>
|
|
<tr class="othertable">
|
|
<td>a plain literal "sss"</td>
|
|
<td>'sss' , with any internal occurrences of ''' prefixed with '\'</td>
|
|
</tr>
|
|
<tr class="othertable">
|
|
<td>a plain literal "sss"@ttt</td>
|
|
<td>the term <code>pair(</code>'sss'<em></em>,'ttt'<code>)</code></td>
|
|
</tr>
|
|
<tr class="othertable">
|
|
<td>a typed literal <span >"sss"^^ddd </span></td>
|
|
<td>the term <code>LiteralValueOf(</code>'sss'<em></em>,<em>TR</em>[ddd]<code>)</code></td>
|
|
</tr>
|
|
<tr class="othertable">
|
|
<td>an RDF container membership property name of the form <code>rdf:_<em>nnn</em></code></td>
|
|
<td><code>rdf-member(</code><em>nnn</em><code>)</code></td>
|
|
</tr>
|
|
<tr class="othertable">
|
|
<td>any other URI reference aaa</td>
|
|
<td>aaa or <aaa></td>
|
|
</tr>
|
|
<tr class="othertable">
|
|
<td>a blank node</td>
|
|
<td>a variable (one distinct variable per blank node)</td>
|
|
</tr>
|
|
<tr class="othertable">
|
|
<td>a triple <br />
|
|
aaa rdf:type bbb .</td>
|
|
<td> <em>TR</em>[bbb]<code>(</code><em>TR</em>[aaa]<code>) and rdfs:Class(</code><em>TR</em>[bbb]<code>)</code></td>
|
|
</tr>
|
|
<tr class="othertable">
|
|
<td>any other triple <br />
|
|
aaa bbb ccc .</td>
|
|
<td><em>TR</em>[bbb]<code>(</code><em>TR</em>[aaa], <em>TR</em>[ccc]<code>)
|
|
and rdf:Property(</code><em>TR</em>[bbb]<code>)</code></td>
|
|
</tr>
|
|
<tr class="othertable">
|
|
<td>an RDF graph</td>
|
|
<td>The existential closure of the conjunction of the translations of all
|
|
the triples in the graph.</td>
|
|
</tr>
|
|
<tr class="othertable">
|
|
<td>a set of RDF graphs</td>
|
|
<td>The conjunction of the translations of all the graphs.</td>
|
|
</tr>
|
|
</table>
|
|
<table summary="rdf Lbase axioms" width="100%" border="1">
|
|
<caption>
|
|
<br />
|
|
RDF axioms
|
|
</caption>
|
|
|
|
<tr>
|
|
<td class="othertable">
|
|
<p><code>rdf:type(?x,?y) implies ?y(?x)</code></p>
|
|
<p><code>rdf:Property(rdf:type)<br />
|
|
rdf:Property(rdf:subject)<br />
|
|
rdf:Property(rdf:predicate)<br />
|
|
rdf:Property(rdf:object)<br />
|
|
rdf:Property(rdf:first)<br />
|
|
rdf:Property(rdf:rest)<br />
|
|
rdf:Property(rdf:value)<br />
|
|
rdf:List(rdf:nil)</code></p>
|
|
<p><code><em>NatNumber</em>(?x) implies rdf:Property(rdf-member(?x))</code></p>
|
|
<p><code>pair(?x,?y)=pair(?u,?v) iff (?x=?u and ?y=?v)</code> <em> ;; uniqueness
|
|
for pairs, required by graph syntax rules. </em></p>
|
|
</td>
|
|
</tr>
|
|
</table>
|
|
<table summary="rdfs axioms" width="100%" border="1">
|
|
<caption>
|
|
<br />
|
|
RDFS axioms
|
|
</caption>
|
|
|
|
<tr>
|
|
|
|
<td class="othertable"> <code>rdfs:Resource(?x)</code>
|
|
<p><code>rdfs:Class(?y) implies (?y(?x) iff rdf:type(?x,?y))</code></p>
|
|
<p><code>rdfs:range(?x,?y) implies ( ?x(?u,?v)) implies ?y(?v) ) </code><em>;;could
|
|
be iff, see below.</em></p>
|
|
<p><code>rdfs:domain(?x,?y) implies ( ?x(?u,?v)) implies ?y(?u) ) </code><em>;;could
|
|
be iff, see below.</em></p>
|
|
<p><span class="newstuff"><code>r</code></span><code>dfs:subClassOf(?x ?y)
|
|
implies<br />
|
|
(rdfs:Class(?x) and rdfs:Class(?y) and (forall (?u)(?x(?u)
|
|
implies ?y(?u)))</code></p>
|
|
<p><code>rdfs:Class(?x) implies ( rdfs:subClassOf(?x ?x) and rdfs:subClassOf(?x
|
|
rdfs:Resource) )</code></p>
|
|
<p><code>( rdfs:subClassOf(?x ?y) and rdfs:subClassOf(?y ?z) ) implies rdfs:subClassOf(?x
|
|
?z)</code></p>
|
|
<p><code>rdfs:subPropertyOf(?x,?y) implies<br />
|
|
(rdf:Property(?x) and rdf:Property(?y) and (forall (?u ?v)(?x(?u,?v)
|
|
implies ?y(?u,?v)))</code></p>
|
|
<p><code>rdf:Property(?x) implies rdfs:subPropertyOf(?x ?x)</code></p>
|
|
<p><code>( rdfs:subPropertyOf(?x ?y) and rdfs:subPropertyOf(?y ?z) ) implies
|
|
rdfs:subPropertyOf(?x ?z)</code></p>
|
|
<p><code>rdfs:ContainerMembershipProperty(?x) implies rdfs:subPropertyOf(?x,rdfs:member)</code></p>
|
|
<p><code>rdf:XMLLiteral(?x) implies rdfs:Literal(?x)</code></p>
|
|
<p><code><em>String</em>(?y) implies rdfs:Literal(?y)</code></p>
|
|
<p><code>(<em>String</em>(?x) and LanguageTag(?y)) implies rdfs:Literal(pair(?x,?y))</code></p>
|
|
<p><code>rdfs:Datatype(?x) implies (?x(?y) implies rdfs:Literal(?y) )</code></p>
|
|
<p><code><em>NatNumber</em>(?x) implies <br />
|
|
(rdfs:ContainerMembershipProperty(rdf-member(?x)) and <br />
|
|
rdfs:domain(rdf-member(?x),rdfs:Resource) and <br />
|
|
rdfs:range(rdf-member(?x), rdfs:Resource) )</code></p>
|
|
<p><code>rdfs:Class(rdfs:Resource)<br />
|
|
rdfs:Class(rdf:Property)<br />
|
|
rdfs:Class(rdfs:Class)<br />
|
|
rdfs:Class(rdfs:Datatype)<br />
|
|
rdfs:Class(rdf:Seq)<br />
|
|
rdfs:Class(rdf:Bag)<br />
|
|
rdfs:Class(rdf:Alt)<br />
|
|
rdfs:Class(rdfs:Container)<br />
|
|
rdfs:Class(rdf:List)<br />
|
|
rdfs:Class(rdfs:ContainerMembershipProperty)<br />
|
|
rdfs:Class(rdf:Statement)<br />
|
|
rdf:Property(rdfs:domain)<br />
|
|
rdf:Property(rdfs:range)<br />
|
|
rdf:Property(rdfs:subClassOf)<br />
|
|
rdf:Property(rdfs:subPropertyOf)<br />
|
|
rdf:Property(rdfs:comment)<br />
|
|
</code><code>rdf:Property(rdfs:seeAlso)<br />
|
|
rdf:Property(rdfs:isDefinedBy)<br />
|
|
rdf:Property(rdfs:label)<br />
|
|
</code><em>;; the rest of the axioms are direct transcriptions of the
|
|
<a href="#RDFS_axiomatic_triples" class="termref">RDFS axiomatic triples</a>,
|
|
using the RDF to L<sub>base</sub> transcription rules:</em></p>
|
|
<p><code>rdfs:domain(rdf:type,rdfs:Resource)<br />
|
|
rdfs:domain(rdfs:domain,rdf:Property)<br />
|
|
rdfs:domain(rdfs:range,rdf:Property) <br />
|
|
rdfs:domain(rdfs:subPropertyOf,rdf:Property)<br />
|
|
rdfs:domain(rdfs:subClassOf,rdfs:Class)<br />
|
|
rdfs:domain(rdf:subject,rdf:Statement)<br />
|
|
rdfs:domain(rdf:predicate,rdf:Statement)<br />
|
|
rdfs:domain(rdf:object,rdf:Statement)<br />
|
|
rdfs:domain(rdf:member,rdfs:Resource)<br />
|
|
rdfs:domain(rdf:first,rdf:List)<br />
|
|
rdfs:domain(rdf:rest,rdf:List)<br />
|
|
rdfs:domain(rdfs:seeAlso,rdfs:Resource)<br />
|
|
rdfs:domain(rdfs:isDefinedBy,rdfs:Resource)<br />
|
|
rdfs:domain(rdfs:comment,rdfs:Resource)<br />
|
|
rdfs:domain(rdfs:label,rdfs:Resource)<br />
|
|
rdfs:domain(rdfs:value,rdfs:Resource) </code></p>
|
|
<p><code>rdfs:range(rdf:type,rdfs:Class)<br />
|
|
rdfs:range(rdfs:domain,rdfs:Class)<br />
|
|
rdfs:range(rdfs:range,rdfs:Class)<br />
|
|
rdfs:range(rdfs:subPropertyOf,rdf:Property)<br />
|
|
rdfs:range(rdfs:subClassOf,rdfs:Class)<br />
|
|
rdfs:range(rdf:subject,rdfs:Resource)<br />
|
|
rdfs:range(rdf:predicate,rdfs:Resource)<br />
|
|
rdfs:range(rdf:object,rdfs:Resource)<br />
|
|
rdfs:range(rdf:member,rdfs:Resource)<br />
|
|
rdfs:range(rdf:first,rdfs:Resource)<br />
|
|
rdfs:range(rdf:rest,rdf:List)<br />
|
|
rdfs:range(rdfs:seeAlso,rdfs:Resource)<br />
|
|
rdfs:range(rdfs:isDefinedBy,rdfs:Resource)<br />
|
|
rdfs:range(rdfs:comment,rdfs:Literal)<br />
|
|
rdfs:range(rdfs:label,rdfs:Literal)<br />
|
|
rdfs:range(rdfs:value,rdfs:Resource) </code></p>
|
|
<p><code>rdfs:subClassOf(rdf:Alt,rdfs:Container)<br />
|
|
rdfs:subClassOf(rdf:Bag,rdfs:Container)<br />
|
|
rdfs:subClassOf(rdf:Seq, rdfs:Container)<br />
|
|
rdfs:subClassOf(rdfs:ContainerMembershipProperty,rdf:Property)</code></p>
|
|
<p><code>rdfs:subPropertyOf(rdfs:isDefinedBy,rdfs:seeAlso)</code></p>
|
|
<p><code>rdfs:Datatype(rdf:XMLLiteral)<br />
|
|
rdfs:subClassOf(rdfs:Datatype,rdfs:Class)<br />
|
|
</code></p>
|
|
</td>
|
|
</tr>
|
|
</table>
|
|
<p>The extensional semantic conditions for subclass, subproperty, domain and range
|
|
described in <a href="#ExtensionalDomRang" class="termref"> Section 4.1</a> can be captured by adding the following axioms:</p>
|
|
<table width="100%" border="1">
|
|
<tr>
|
|
<td class="othertable"> <p><code>rdfs:range(?x,?y) iff ( ?x(?u,?v)) implies
|
|
?y(?v) )</code></p>
|
|
<p><code> rdfs:domain(?x,?y) iff ( ?x(?u,?v)) implies ?y(?u) ) </code></p>
|
|
<p><code> rdfs:subClassOf(?x ?y) iff<br />
|
|
(rdfs:Class(?x) and rdfs:Class(?y) and (forall (?u)(?x(?u)
|
|
implies ?y(?u)))</code></p>
|
|
<p><code>rdfs:subPropertyOf(?x,?y) iff<br />
|
|
(rdf:Property(?x) and rdf:Property(?y) and (forall (?u ?v)(?x(?u,?v)
|
|
implies ?y(?u,?v)))</code><code> </code></p>
|
|
</td>
|
|
</tr>
|
|
</table>
|
|
<p>The L<sub>base</sub> translation for typed literals uses a binary function
|
|
<code>LiteralValueOf</code> from a lexical form and a <a href="#defDatatype" class="termref">datatype</a> to a value. For
|
|
well-formed <a href="#defDatatype" class="termref">datatype</a>s this value will be the same as the lexical-to-value map
|
|
applied to the same arguments, but for ill-formed literals it will be something
|
|
of which the predicate <code>rdfs:Literal</code> is false. </p>
|
|
<p>To fully axiomatize the intended meaning of typed literals requires a <em>datatype
|
|
theory</em>. Formally, such a theory - one for each <a href="#defDatatype" class="termref">datatype</a> - will consist
|
|
of a countably infinite set of ground axioms which list for each possible string
|
|
whether or not it is a legal lexical form for the <a href="#defDatatype" class="termref">datatype</a>, and possibly provide
|
|
a way to indicate its value. In practice it would be appropriate to implement
|
|
these by procedural call-outs to special-purpose code which would check the
|
|
truth or falsity of the appropriate ground atoms. </p>
|
|
<p>A datatype theory for the <a href="#defDatatypeMap" class="termref">datatype map</a> {<<code>ddd</code>, <em>datatype</em>>}
|
|
(where <code>ddd</code> is a URI reference) is the set containing the axiom</p>
|
|
<p><code>rdfs:Datatype(ddd)</code></p>
|
|
<p>and all assertions of the form:</p>
|
|
<p><code>ddd(LiteralValueOf('aaa',ddd))</code></p>
|
|
<p>where <code>aaa</code> is a legal lexical form for <em>datatype</em>, and all
|
|
assertions of the form:</p>
|
|
<p><code>not ddd(LiteralValueOf('aaa',ddd))</code></p>
|
|
<p>where <code>aaa</code> is any string which is not a legal lexical form for
|
|
<em>datatype</em>.</p>
|
|
<p> If there is some notational framework in (or added to) L<sub>base</sub> which
|
|
enables one to write terms denoting the members of the value space of the <a href="#defDatatype" class="termref">datatype</a>,
|
|
then the database theory can also contain all true axioms of the form</p>
|
|
<p><code>LiteralValueOf('aaa',ddd) = [L2V(</code><em>datatype</em><code>,aaa)]</code></p>
|
|
<p>where the square brackets indicate the presence of the appropriate term for
|
|
that value. For example, using decimal numerals to denote the integers, this
|
|
could be all equations of the form</p>
|
|
<p><code>LiteralValueOf('345',xsd:integer) = 345</code></p>
|
|
<p>Obviously, such axioms, or procedural equivalents, would be needed in order
|
|
to connect the RDF translation to other axioms which used the more conventional
|
|
notations.</p>
|
|
<p>In some cases, a datatype theory can be summarized in a finite number of axioms.
|
|
<span class="newstuff">For example, the datatype theory for <code>xsd:string</code>
|
|
can be stated by a single axiom:</span></p>
|
|
<p><code class="newstuff">(<em>String</em>(?x) iff xsd:string(?x) ) and (<em>String</em>(?x)
|
|
implies LiteralValueOf(?x,xsd:string) = ?x )</code></p>
|
|
<table summary="rdf XMLliteral Lbase axioms" width="100%" border="1">
|
|
<caption>
|
|
<br />
|
|
RDF Datatyped Literal axioms
|
|
</caption>
|
|
<tr class="othertable">
|
|
<td> <code>rdfs:Literal(LiteralValueOf(?x,?y)) iff ?y(LiteralValueOf(?x,?y))<br/>
|
|
rdfs:Datatype(?y) implies rdfs:Class(?y)<br />
|
|
rdfs:Datatype(?y) implies (exists (?x) ?y(?x) )</code></td>
|
|
</tr>
|
|
</table>
|
|
<p>To obtain the L<sub>base</sub> translation corresponding to <a href="#defDinterp" class="termref">D-interpretation</a>s
|
|
for some <a href="#defDatatypeMap" class="termref">datatype map</a> D, add the
|
|
above axioms and a datatype theory for every pair in the <a href="#defDatatypeMap" class="termref">datatype
|
|
map</a> D. </p>
|
|
<p>Further information about subclass relationships between value spaces of <a href="#defDatatype" class="termref">datatype</a>s
|
|
can be expressed in L<sub>base</sub> directly in terms of <code>rdfs:subClassOf</code>,
|
|
or equivalently by using the datatype URI references as property names.</p>
|
|
|
|
<h2><a name="prf" id="prf">Appendix B: 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>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 . 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="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 name="mergelemprf" id="mergelemprf"><strong>Merging
|
|
lemma.</strong></a> The <a href="#defmerg" 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>In the following proofs and discussion it is convenient to extend the definition
|
|
of interpretation so as to treat blank nodes similarly to names. Define an <em>extended
|
|
vocabulary</em> to be a set of names or blank nodes, and the set of names and
|
|
blank nodes in a graph G the extended vocabulary <em>of</em> G. If I is a simple
|
|
interpretation of V and IB is a mapping from a set B of blank nodes to IR, then
|
|
call [I+IB] an <em>extended interpretation</em> of the extended vocabulary (V
|
|
union B). The mapping IB plays the same role for blank nodes that IS and IL
|
|
do for URI references and literals respectively. Every interpretation can be
|
|
considered an extended intepretation on an extended vocabulary which happens
|
|
to contain no blank nodes. In the following, when there is no fear of confusion
|
|
we will sometimes omit the "extended", treat extended interpretations
|
|
as interpretations, allow vocabularies to contain blank nodes, and write I(b)
|
|
for IB(b). </p>
|
|
<p>Say that an extended interpretation J <em>extends</em>, or <em>is an extension
|
|
of</em> another I, when IR<sub>I</sub> is a subset of IR<sub>J</sub>, the extended
|
|
vocabulary of J includes that of I, for each a in the vocabulary of I, I(a)=J(a),
|
|
and for each x in IR<sub>I</sub>, if IEXT<sub>I</sub>(x) is defined then IEXT<sub>I</sub>(x)
|
|
is a subset of IEXT<sub>J</sub>(x). Then the definition of satisfaction for
|
|
blank nodes can be paraphrased as saying that I satisfies G just when there
|
|
is an extension of I of the extended vocabulary of G which satisfies every triple
|
|
in G. </p>
|
|
<p>Suppose I is an interpretation and k is a mapping from IR to some set S, then
|
|
I<strong><code>.</code></strong>k is the interpretation gotten by extending
|
|
the mapping k to the rest of I as follows: for any name or blank node a in the
|
|
vocabulary of I, I<strong><code>.</code></strong>k(a)=k(I(a)), and IEXT<sub>I<strong><code>.</code></strong>k</sub>(k(x))={<k(y),k(z)><code>:
|
|
</code><y,z> in IEXT<sub>I</sub>(x)}. Call this a <em>projection</em>
|
|
of I into S. If there is a projection k of I into IR<sub>J</sub> such that J
|
|
extends I<strong><code>.</code></strong>k, then say that I is a <em>subinterpretation</em>
|
|
of J, and write I<<J. The subinterpretation relation between interpretations
|
|
is the dual of the entailment relation between sentences, as shown by the following
|
|
lemma:</p>
|
|
<p><strong>Subinterpretation Lemma.</strong> If I << J and I satisfies E
|
|
then J satisfies E. </p>
|
|
<blockquote>
|
|
<p><strong>Proof.</strong> Let k be the projection of I into IR<sub>J</sub>.
|
|
Since I satisfies E, there is a superinterpretation L of E which extends I
|
|
and satisfies every triple <br />
|
|
s p o <code>.</code><br />
|
|
in E, i.e. <L(s),L(o)> is in IEXT<sub>L</sub>(L(p)). Applying the projection,
|
|
it follows that <k(L(s)),k(L(o))> is in IEXT<sub>J</sub>(k(L(p))). If
|
|
x is a URI reference then k(L(x))=J(x); so consider the superinterpretation
|
|
M=[J+Lk], then we have <M(s),M(o)> is in IEXT<sub>M</sub>(M(p)); so
|
|
M satisfies every triple in E; so J satisfies E. <strong>QED</strong></p>
|
|
</blockquote>
|
|
<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 incorporate XML data appropriately.)
|
|
Given a nonempty graph G, <a name="defherbinterp" id="defherbinterp"></a>the
|
|
<em>Herbrand interpretation</em> of G, written <a name="defHerb" id="defHerb"></a>Herb(G),
|
|
is the interpretation I defined as follows. LV is the set of all required literal
|
|
values (well-formed XML literals in G, character strings and pairs of character
|
|
strings and language tags); IR is LV plus 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;
|
|
IP is the set of URI references which occur in the property position of any
|
|
triple in G; IS is the identity mapping on the vocabulary of G, IL maps all
|
|
typed literals into themselves, and IEXT is defined by: <s,o> is in IEXT(p)
|
|
just when there is a triple in the graph of the form s p o . The <em>Herbrand</em>
|
|
<em>superinterpretation</em> is Herb(G)+B, where B is the identity map on blank
|
|
nodes in G. Clearly the Herbrand superinterpretation 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 in the same way as simple 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 lemma shows that any graph <i>can</i> be interpreted
|
|
in this way. This therefore establishes a useful result:</p>
|
|
<p><a name="Satisfacprf" id="Satisfacprf"><strong>Satisfaction Lemma.</strong></a>
|
|
Any RDF graph has a <a href="#glossSatisfy"
|
|
class="termref">satisfying</a> interpretation. <strong>QED</strong></p>
|
|
<p><a href="#defherbinterp" class="termref">Herbrand interpretation</a>s have
|
|
some very useful properties. The <a href="#defherbinterp" class="termref">Herbrand
|
|
interpretation</a> of a graph is a 'minimal' interpretation, which is 'just
|
|
enough' to make the graph true; and so any interpretation which satisfies the
|
|
graph must in a sense agree with the <a href="#defherbinterp" class="termref">Herbrand
|
|
interpretation</a>; and of course any interpretation which does agree with the
|
|
<a href="#defherbinterp" class="termref">Herbrand interpretation</a> will satisfy
|
|
the graph. Taken together and made precise, these observations provide a way
|
|
to characterize entailment between graphs in terms of <a href="#defherbinterp" class="termref">Herbrand
|
|
interpretation</a>s.</p>
|
|
<p> <strong>Herbrand lemma.</strong> I satisfies E if and only if <a href="#defHerb" class="termref">Herb(</a>E)
|
|
<< I.</p>
|
|
<blockquote>
|
|
<p><strong>Proof.</strong> Write H=Herb(E). </p>
|
|
<p>Suppose I satisfies E, then the interpretation mapping I itself defines a
|
|
projection mapping from <a href="#defHerb" class="termref">H</a> into IR; for
|
|
H(a)=a for any name or blank node in E, and so H<strong><code>.</code></strong>I(a)=I(H(a))=I(a);
|
|
and <s,o> is in IEXT<sub>H</sub>(p) just in case the triple s p o <strong><code>.</code></strong>
|
|
is in E; so <I(x),I(y)> must be in IEXT<sub>I</sub>(I(p)), i.e.in IEXT<sub>H<strong><code>.</code></strong>I</sub>(I(x)),
|
|
which is the condition for I to be a projection from H; so H<<I.</p>
|
|
<p>Suppose H << I. H satisfies E by construction, so I satisfies E by
|
|
the subinterpretation lemma.<strong><br />
|
|
QED</strong></p>
|
|
</blockquote>
|
|
|
|
<p>The following is an immediate consequence<strong>:</strong></p>
|
|
<p><strong>Herbrand entailment lemma</strong>. S entails E if and only if <a href="#defHerb" class="termref">Herb(</a>S)
|
|
satisfies E.</p>
|
|
<blockquote>
|
|
<p><strong>Proof.</strong> Suppose S entails E. <a href="#defHerb" class="termref">Herb(</a>S)
|
|
satisfies S, so <a href="#defHerb" class="termref">Herb(</a>S) satisfies E.</p>
|
|
<p>Now suppose <a href="#defHerb" class="termref">Herb(</a>S) satisfies E. If
|
|
I satisfies S then <a href="#defHerb" class="termref">Herb(</a>S) <<
|
|
I; so I satisfies E. But I was arbitrary; so S entails E.<strong><br />
|
|
QED</strong></p>
|
|
</blockquote>
|
|
<p></p>
|
|
|
|
|
|
<p>The syntactic properties of Herbrand interpretations can be described in terms
|
|
of instances and subgraphs. Say that <a id="defuncon" name="defuncon">a graph
|
|
E' is <i>connected </i> to a graph E if some instance of E' is a subgraph of
|
|
E.</a> In particular, a ground graph is connected to E just when it is a subgraph
|
|
of E, a ground triple is connected just when it is in the graph. Graphs which
|
|
are connected to E are entailed by E, by the subgraph and instance lemmas; but
|
|
for all others, there is a way to arrange the world so that they are false and
|
|
E true.</p>
|
|
<p>In particular, if E' is not <a href="#defuncon" class="termref">connected</a> to E then <a href="#defHerb" class="termref">Herb(</a>E) does not satisfy E';
|
|
for suppose that it did, then for some mapping B from the blank nodes of E'
|
|
to the blank nodes and vocabulary of E, <a href="#defHerb" class="termref">Herb(</a>E)+B satisfies E', which means
|
|
that for every triple</p>
|
|
|
|
<p>s p o .</p>
|
|
|
|
<p>in E', the triple</p>
|
|
|
|
<p>[<a href="#defHerb" class="termref">Herb(</a>E)+B](s) p [<a href="#defHerb" class="termref">Herb(</a>E)+B](o) .</p>
|
|
|
|
|
|
<p>occurs in E, by definition of <a href="#defHerb" class="termref">Herb(</a>E). But the set of these triples is an instance
|
|
of E', by construction; so E' is <a href="#defuncon" class="termref">connected</a> to E.</p>
|
|
|
|
<p>This provides an exact correspondence between
|
|
separability and <a href="#defherbinterp" class="termref">Herbrand interpretation</a>s:</p>
|
|
|
|
|
|
<p><strong>Herbrand separation lemma.</strong> <a href="#defHerb" class="termref">Herb(</a>E) satisfies E' if and only
|
|
if E' is <a href="#defuncon" class="termref">connected</a> to E. <strong>QED</strong></p>
|
|
<p>Putting the separation and entailment results together, it is obvious that
|
|
S entails E if and only if E is <a href="#defuncon" class="termref">connected</a>
|
|
to S. This is simply a restatement of the:</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>
|
|
<strong>QED.</strong></p>
|
|
|
|
<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> Since E' is a <a
|
|
href="#defpropinst" class="termref">proper</a> instance and E is <a
|
|
href="#deflean" class="termref">lean</a>, E' is not <a href="#defuncon" class="termref">connected</a> to E. Therefore E does not
|
|
entail E' <strong>QED</strong></p>
|
|
</blockquote>
|
|
<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 general monotonicity lemma)</p>
|
|
<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>QED</strong></p>
|
|
</blockquote>
|
|
<p>Although this result is trivial for simple entailment, it becomes progressively
|
|
less trivial in more elaborate semantic extensions. </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. </p>
|
|
<p><strong>QED</strong></p>
|
|
</blockquote>
|
|
<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 the <a href="#simpleRules" class="termref">simple
|
|
entailment rules</a> and <a href="#RDFRules" class="termref">RDF entailment
|
|
rules</a> and which <a href="#defentail" class="termref">simply entails</a>
|
|
E.</p>
|
|
<blockquote>
|
|
<p><strong>Proof.</strong> To show 'if' here is trivial: one has only to check
|
|
that the <span class="newstuff"><a href="#RDFRules" class="termref">RDF entailment
|
|
rules</a></span> are rdf-valid, which is left as an exercise for the reader.
|
|
To establish 'only if' requires more work, however.</p>
|
|
<p>If S or E is empty then the result follows trivially; so suppose they are
|
|
both non-empty.</p>
|
|
<p>Define the <em>rdf-V-closure</em> of a graph G, rdfclos(V, G), to be the
|
|
graph gotten by adding all the <span class="newstuff"><a href="#RDF_axiomatic_triples" class="termref">RDF
|
|
axiomatic triples</a></span> which contain any vocabulary from (V union crdfV)
|
|
to G and then applying the <span class="newstuff"><a href="#simpleRules" class="termref">simple
|
|
entailment rules</a> </span>and<span class="newstuff"> <a href="#RDFRules" class="termref">RDF
|
|
entailment rules</a></span> in all possible ways until the graph is unchanged.
|
|
Define the combined vocabulary vocab(S) union vocab(E) to be W. We will show
|
|
that rdfclos(W, S) satisfies the conditions of the lemma. </p>
|
|
<p>Let H be the <a href="#defherbinterp" class="termref">Herbrand interpretation</a>
|
|
of rdfclos(W, S). It is sufficient to show that there is an <a href="#rdfinterpdef" class="termref">rdf-interpretation</a>
|
|
H' of W with H'<<H; for in that case since S rdf-entails E then H' satisfies
|
|
E; and if I is any simple interpretation of W which satisfies rdfclos(S) then
|
|
H <<I by the Herbrand lemma, so H' <<I, so I satisfies E; so rdfclos(S)
|
|
<a href="#defentail" class="termref">simply entails</a> E. </p>
|
|
<p>H' is constructed from H by adjusting the definition of IP and the interpretation
|
|
of well-typed XML literals and the class extension of <code>rdf:XMLLiteral</code>;
|
|
in other respects H' and H are identical (so that for any other URI reference
|
|
uuu, I<sub>H'</sub>(uuu)=I<sub>H</sub>(uuu)=uuu.) To be precise, define IP<sub>H'</sub>
|
|
to be the set of nodes which occur in rdfclos(W, S) as the subject of a triple
|
|
of the form<br />
|
|
x <code>rdf:type rdf:Property .<br />
|
|
</code>, and for each well-typed XML literal
|
|
x in W, define H'(x) to be the XML value of x; and let IEXT<sub>H'</sub>(rdf:type)
|
|
= IEXT<sub>H</sub>(rdf:type) union {<I<sub>H'</sub>(x), <code>rdf:XMLLiteral</code>>:
|
|
x a well-typed XML literal in W}. In other respects H' is defined as H.</p>
|
|
<p>To see that H'<<H we construct a projection mapping from H' to H which
|
|
preserves the truth of all triples. Apart from XML literals, this is trivially satisfied by the identity mapping:
|
|
we need only check that the definition of IP<sub>H'</sub> does not prevent something being a property;
|
|
and it is easy to see that IP<sub>H'</sub> is a superset of IP<sub>H</sub>; for
|
|
if x is in IP<sub>H</sub> then x must occur in the property position of a
|
|
triple<br />
|
|
s x o .<br />
|
|
in rdfclos(W,S), so by the definition of closure and the rule <a href="#rulerdf1" class="termref">rdf1</a>,
|
|
rdfclos(W,S) contains the triple <br />
|
|
x <code>rdf:type rdf:Property .</code><br />
|
|
so x is in IP<sub>H'</sub>. Mapping IP<sub>H'</sub> to IP<sub>H</sub> does
|
|
not change the truth of any triples, therefore.</p>
|
|
<p>For each well-formed XML literal in W, there is a unique blank node in rdfclos(S),
|
|
introduced by rule <a href="#rulerdf2" class="termref">rdf2</a>, which is
|
|
allocated to that literal. The mapping from the XML literal to the blank node
|
|
which is allocated to it defines an injection mapping from H' to H; the fact
|
|
that it preserves the truth of all triples follows from inspection of the
|
|
rule <a href="#rulerdf2" class="termref">rdf2</a> and the construction of
|
|
H'; so H'<<H.</p>
|
|
<p>Clearly H' satisfies the RDF semantic conditions by construction (and by
|
|
the minimality of a <a href="#defherbinterp" class="termref">Herbrand interpretation</a>).
|
|
</p>
|
|
<p><strong>QED</strong></p>
|
|
</blockquote>
|
|
<p><strong><a name="RDFSEntailmentLemmaPrf" id="RDFSEntailmentLemmaPrf"></a></strong><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 the <a href="#simpleRules" class="termref">simple</a>,
|
|
<a href="#RDFRules" class="termref">RDF</a> and <a href="#RDFSRules" class="termref">RDFS
|
|
entailment rules</a> and which <a href="#defentail" class="termref">simply entails</a>
|
|
E. </p>
|
|
<blockquote>
|
|
<p><strong>Proof.</strong> Again, to show 'if' it is sufficient to show that
|
|
the <span class="newstuff"><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
|
|
the same terminology will be used, except that the RDFS closure, rdfsclos(V,G),
|
|
is the graph gotten by adding the appropriate RDF and RDFS axiomatic triples
|
|
to G, and then applying the simple, RDF and RDFS entailment rules until the
|
|
graph is unchanged. Let H be the <a href="#defherbinterp" class="termref">Herbrand interpretation</a> of rdfsclos(W,S)
|
|
and H' be constructed from H as in the previous proof, except that </p>
|
|
<p>IEXT<sub>H'</sub>(rdf:type) = IEXT<sub>H</sub>(rdf:type) union {<I<sub>H'</sub>(x),
|
|
<code>rdf:XMLLiteral</code>>: x a well-typed XML literal in W}union {<I<sub>H'</sub>(x),
|
|
<code>rdfs:Literal</code>>: x a plain literal in W}. </p>
|
|
<p>The projection mapping which establishes that H'<<H is extended in
|
|
the obvious way and rule rdfs1 shows that the truth of triples is preserved
|
|
under the projection. (This technique for using blank nodes as 'surrogates'
|
|
for literals is a general one; it depends on the blank node first introduced
|
|
by the existential rule being uniquely mappable from the term to which it
|
|
is allocated.)</p>
|
|
<p>We will show that H' in this case is an <a href="#rdfsinterpdef" class="termref">rdfs-interpretation</a>; the rest of
|
|
the proof proceeds similarly. Clearly H' is an <a href="#rdfinterpdef" class="termref">rdf-interpretation</a>, so it remains
|
|
only to show that it also satisfies the RDFS semantic conditions; on these,
|
|
H and H' are indistinguishable.</p>
|
|
<p>This is done by simply matching the RDFS semantic conditions with the appropriate
|
|
entailment rules. We will illustrate the form of the argument with two examples.
|
|
</p>
|
|
<p>Consider the <a href="#rdfssemcond1" class="termref">first semantic condition</a>. Suppose <x,y> is in IEXT<sub>H</sub>(<code>rdfs:domain</code>)
|
|
and <u,v> is in IEXT<sub>H</sub>(x); then by the minimality of the <a href="#defherbinterp" class="termref">Herbrand interpretation</a>, rdfsclos(W,S) must contain triples</p>
|
|
<p>x <code>rdfs:domain </code>y<code> .<br />
|
|
</code>u x v <code>.</code></p>
|
|
<p>so by rule <a href="#rulerdfs2" class="termref">rdfs2</a>, it must also contain the triple</p>
|
|
<p>u <code>rdf:type</code> y <code>.</code></p>
|
|
<p>so by the construction of H, IEXT<sub>H</sub>(<code>rdf:type</code>) contains
|
|
<u,y>, i.e. u is in ICEXT<sub>H</sub>(y).</p>
|
|
<p>In some cases, the rule derivation involves several steps and some of the
|
|
RDF and RDFS axiomatic triples; for example, to show that H satisfies the
|
|
<a href="#rdfssemcond7" class="termref">seventh semantic condition</a> </p>
|
|
<table width="100%" border="1">
|
|
<tr class="semantictable">
|
|
<td > 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)
|
|
</td>
|
|
</tr>
|
|
</table>
|
|
<p> note that <x,y> is in IEXT<sub>H</sub>(<code>rdfs:subClassOf</code>)
|
|
only if rdfsclos(W,S) contains </p>
|
|
<p>x <code>rdfs:subClassOf </code>y</p>
|
|
<p>and then the following are all in rdfsclos(W,S):</p>
|
|
<p><code>rdfs:subClassOf rdfs:domain rdfs:Class . </code>(<a href="#axtripleforproof1" class="termref">RDFS axiomatic triple</a>)<br />
|
|
x <code>rdf:type rdfs:Class . </code>(rule <a href="#rulerdfs1" class="termref">rdfs1</a>)<br />
|
|
<code>rdfs:subClassOf rdfs:range rdfs:Class . </code>(<a href="#axtripleforproof2" class="termref">RDFS axiomatic triple</a>)<br />
|
|
y <code>rdf:type rdfs:Class . </code>(rule <a href="#rulerdfs2" class="termref">rdfs2</a>)</p>
|
|
<p>so x and y are both in IC<sub>H</sub>; and that if z is in ICEXT<sub>H</sub>(x)
|
|
then rdfsclos(W,S) must contain a triple</p>
|
|
<p>z <code>rdf:type</code> x <code>.</code></p>
|
|
<p>so it must also contain a triple</p>
|
|
<p>z <code>rdf:type</code> y<code>. </code>by rule <a href="#rulerdfs9" class="termref">rdfs9</a></p>
|
|
<p>so by the construction of the <a href="#defherbinterp" class="termref">Herbrand interpretation</a>, <z,y> is in
|
|
IEXT<sub>H</sub>(<code>rdf:type</code>), i.e. z is in ICEXT<sub>H</sub>(y).</p>
|
|
<p>The other conditions can be checked similarly. </p>
|
|
<p><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. 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 the new skolem functions.</p>
|
|
|
|
|
|
<p>In RDF, Skolemization simplifies to the special case where an existential variable
|
|
is replaced by a 'new' name, i.e. a URI reference which is guaranteed to not occur
|
|
anywhere else. (Using a literal would not do. Literals are never 'new' in the
|
|
required sense.) To be precise, a <em>Skolemization</em> of E (with respect
|
|
to V) is a ground instance of E with respect to a vocabulary V which is disjoint
|
|
from the vocabulary of E.</p>
|
|
|
|
<p>The following lemma shows that Skolemization has the same
|
|
properties in RDF as it has in conventional logics. Intuitively,
|
|
this lemma shows that asserting a Skolemization expresses a similar
|
|
content to asserting the original graph, in many respects. In
|
|
effect, it simply gives 'arbitrary' names to the anonymous entities
|
|
whose existence was asserted by the use of blank nodes. However,
|
|
care is needed, since these 'arbitrary' names 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.</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 interpolation
|
|
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 > </p>
|
|
<h2><a name="gloss" id="gloss"></a>Appendix C: 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). 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 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><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="glossCorrect"
|
|
id="glossCorrect"></a>Correct</strong> (adj., of an inference
|
|
system). Unable to draw any invalid inferences. See
|
|
<em>Inference</em>.</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><strong><a name="glossIndexical"
|
|
id="glossIndexical"></a>Indexical</strong> (adj., of a logic
|
|
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 D: 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 found several major problems in earlier drafts, and suggested
|
|
many important technical improvements. Herman ter Horst made several useful
|
|
technical suggestions.</p>
|
|
<p>Pat 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/2003/WD-rdf-concepts-20030905/">Resource
|
|
Description Framework (RDF): Concepts and Abstract Syntax</a> </cite>, G.
|
|
Klyne, J. Carroll, Editors, World Wide Web Consortium Working Draft,
|
|
work in progress, 5 September 2003. This version of the RDF Concepts and Abstract
|
|
Syntax is http://www.w3.org/TR/2003/WD-rdf-concepts-20030905/.
|
|
The <a href="http://www.w3.org/TR/rdf-concepts/">latest version of the RDF
|
|
Concepts and Abstract Syntax</a> is at http://www.w3.org/TR/rdf-concepts/.
|
|
</dd>
|
|
<dt><a id="ref-rdf-syntax"
|
|
name="ref-rdf-syntax"></a>[RDF-SYNTAX]</dt>
|
|
|
|
<dd><i><a
|
|
href="http://www.w3.org/TR/2003/WD-rdf-syntax-grammar-20030905/">RDF/XML
|
|
Syntax Specification (Revised)</a></i>, Beckett D. (Editor), World Wide Web
|
|
Consortium Working Draft, 5 September 2003 (work in progress). <a
|
|
href="http://www.w3.org/TR/2003/WD-rdf-syntax-grammar-20030905/">This version</a>
|
|
is http://www.w3.org/TR/2003/WD-rdf-syntax-grammar-20030905/. The <a href="http://www.w3.org/TR/rdf-syntax-grammar/">latest
|
|
version</a> is 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/2003/WD-rdf-testcases-20030905/">RDF
|
|
Test Cases</a></cite> , J. Grant and D. Beckett, Editors, World Wide Web Consortium
|
|
Working Draft, work in progress, 5 September 2003. This version
|
|
of the RDF Test Cases is http://www.w3.org/TR/2003/WD-rdf-testcases-20030905/.
|
|
The <a href="http://www.w3.org/TR/rdf-testcases/">latest version of the RDF
|
|
Test Cases</a> is 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 name="ref-XML-1.0" id="ref-XML-1.0"></a>[XML 1.0]</dt>
|
|
<dd><cite><a href="http://www.w3.org/TR/2000/WD-xml-2e-20000814">Extensible
|
|
Markup Language (XML) 1.0 (Second Edition)</a></cite> , Bray, T., Paoli, J.,
|
|
Sperberg-McQueen, C. M., Maler, E. W3C Working Draft, 14 August 2000</dd>
|
|
<dt><a name="ref-C14N" id="ref-C14N"></a>[XML-C14N]</dt>
|
|
<dd><cite><a
|
|
href="http://www.w3.org/TR/2002/REC-xml-exc-c14n-20020718/">Exclusive XML
|
|
Canonicalization Version 1.0</a></cite>, Boyer, J., Eastlake 3rd, D.E., Reagle,
|
|
J., Authors/Editors. W3C Recommendation. World Wide Web Consortium, 18 July
|
|
2002. This version of Exclusive XML Canonicalization is http://www.w3.org/TR/2002/REC-xml-exc-c14n-20020718.
|
|
The latest version of Canonical XML is at <a href="http://www.w3.org/TR/xml-exc-c14n">http://www.w3.org/TR/xml-exc-c14n</a>.
|
|
</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><i><a href="http://www.w3.org/TR/owl-ref/">Web Ontology Language (OWL) Reference
|
|
Version 1.0</a></i>, Dean, M., Connolly, D., van Harmelen, F., Hendler, J.,
|
|
Horrocks, I., McGuinness, D., Patel-Schneider, P., Stein, L. (Editors), World
|
|
Wide Web Consortium Working Draft, 12 November 2002</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-20030905/">Lbase: Semantics
|
|
for Languages of the Semantic Web</a></cite>, Guha, R. V., Hayes, P., W3C
|
|
Note, 5 September 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"></a>[RDF-PRIMER]</dt>
|
|
|
|
|
|
<dd><cite><a href=
|
|
"http://www.w3.org/TR/2003/WD-rdf-primer-20030905/">RDF Primer</a></cite>,
|
|
F. Manola, E. Miller, Editors, World Wide Web Consortium W3C Working Draft,
|
|
work in progress, 5 September 2003. This version of the RDF Primer is http://www.w3.org/TR/2003/WD-rdf-primer-20030905/.
|
|
The <a href=
|
|
"http://www.w3.org/TR/rdf-primer/">latest version of the RDF Primer</a>
|
|
is 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/2003/WD-rdf-schema-20030905/">RDF
|
|
Vocabulary Description Language 1.0: RDF Schema</a> </cite>, D. Brickley,
|
|
R.V. Guha, Editors, World Wide Web Consortium Working Draft, work
|
|
in progress, 5 September 2003. This version of the RDF Vocabulary Description
|
|
Language is http://www.w3.org/TR/2003/WD-rdf-schema-20030905. The
|
|
<a href="http://www.w3.org/TR/rdf-schema/">latest version of the RDF Vocabulary
|
|
Description Language</a> is at http://www.w3.org/TR/rdf-schema. </dd>
|
|
</dl>
|
|
<hr />
|
|
|
|
|
|
<h2><a name="change" id="change"></a>Appendix E: Change Log. (Informative)</h2>
|
|
|
|
<p><strong>Changes since the <a href="http://www.w3.org/TR/2003/WD-rdf-mt-20030123/">23
|
|
January 2003</a> last call working draft.</strong></p>
|
|
|
|
<h3><a name="change_editorial" id="change_editorial"></a><strong>1. Editorial. </strong></h3>
|
|
<p><strong>The following changes do not affect the <span class="newstuff">normative</span>
|
|
technical content</strong></p>
|
|
|
|
<p>Many small changes to wording and document organization to improve clarity,
|
|
remove ambiguities, make definitions clearer, etc. and for conformity with other
|
|
RDF documents and W3C house style, following review comments by Lech. The definition
|
|
of 'graph merge' has been rewritten, following review comments by Patel-Schneider
|
|
and Beckett. The background colors have been changed to avoid red/green confusion
|
|
and internal links highlighted with background color in the text. Some of the
|
|
lemmas have been re-stated more economically and the proofs rephrased for clarity.
|
|
The semantic conditions are now aligned exactly with the vocabularies, so that
|
|
RDF interpretations exactly constrain the rdf: vocabulary, etc.. Some of the
|
|
section numbers and titles have been changed to better reflect this realignment.
|
|
The term 'namespace' has been replaced by 'vocabulary' , cf <a href="http://www.w3.org/2001/sw/RDFCore/20030123-issues/#pfps-21">pfps-21</a>.
|
|
<span class="newerstuff">The description of reification refers to <code>rdf:ID</code>.
|
|
</span></p>
|
|
|
|
<p>The informative appendices on Lbase and the proof appendix have been <strong>extensively
|
|
rewritten</strong> and errors corrected, cf. <a href="http://www.w3.org/2001/sw/RDFCore/20030123-issues/#pfps-02">pfps-02</a>.
|
|
Some parallel changes have been made to the Lbase note. The text of the datatypes
|
|
section been <strong>extensively rewritten</strong> following technical changes
|
|
noted below; the older version was ambiguous and <span class="newstuff">contained
|
|
errors</span>. The XSD datatypes suitable for RDF use are listed explicitly
|
|
in the text, cf. <a href="http://www.w3.org/2001/sw/RDFCore/20030123-issues/#pfps-01">pfps-01</a>.</p>
|
|
<p class="newerstuff">Following email by Patel-Schneider, the possibility of an
|
|
rdfs-inconsistency has been noted in the text (section 4, end), with an example,
|
|
a comment added on trivial entailments in section 4.3, and the wording of the
|
|
rdfs entailment lemma has been restricted to consistent antecedents (section
|
|
7.3). This corrects an omission and a consequent error in the text. </p>
|
|
<h3><a name="change_technical" id="change_technical"></a><strong>2. Technical/editorial.</strong></h3>
|
|
<p><strong>The following changes do not affect any entailments or test cases.</strong></p>
|
|
|
|
<dl>
|
|
<dt>Following a WG decision <a href="http://www.w3.org/2003/06/27-rdfcore-irc#T15-07-36">http://www.w3.org/2003/06/27-rdfcore-irc#T15-07-36</a>, the entailment rules are now labelled as normative.</dt>
|
|
<dt>Lexical and value spaces of datatypes are required to be nonempty, following
|
|
email comments by Patel-Schneider. </dt>
|
|
<dt>In simple interpretations, IP is no longer required to be a subset of IR
|
|
in all interpretations. </dt>
|
|
<dd>This does not affect RDF or RDFS interpretations but makes the model theory
|
|
more conventional and may help with layering future semantic extensions onto
|
|
RDF. Text has been added to clarify why RDF interpretations are unchanged.</dd>
|
|
<dt>"Vocabulary" is now defined to include typed literals as well
|
|
as URI references; definition of 'name' changed accordingly.</dt>
|
|
<dd>This is required by the new treatment of datatypes and is more conventional.</dd>
|
|
<dt>The set LV of literal values is no longer considered 'global' but is part
|
|
of an interpretation.</dt>
|
|
<dd> This is more conventional, makes the semantics easier to state and simplifies
|
|
the proofs. </dd>
|
|
<dt>RDF lists are no longer required to explicitly give <code>rdf:type rdf:List</code>
|
|
triples for all sublists. (WG decision recorded <a href="http://lists.w3.org/Archives/Public/w3c-rdfcore-wg/2003May/0199.html">
|
|
http://lists.w3.org/Archives/Public/w3c-rdfcore-wg/2003May/0199.html</a>)
|
|
The wording of the text and examples in section 3.2.3 have been modified to
|
|
suit.</dt>
|
|
<dt>The definition of rdf-interpretation refers to a 'central' vocabulary. </dt>
|
|
<dd> This avoids a technical awkwardness arising from the infinite container
|
|
vocabulary.</dd>
|
|
<dt>The reference [RDF_VOCABULARY] is not a normative reference.</dt>
|
|
<dd> (WG decision recorded <a href="http://lists.w3.org/Archives/Public/w3c-rdfcore-wg/2003Jul/0236">http://lists.w3.org/Archives/Public/w3c-rdfcore-wg/2003Jul/0236</a>
|
|
) </dd>
|
|
<dd> </dd>
|
|
</dl>
|
|
|
|
<h3><a name="change_substantial" id="change_substantial"></a><strong>3. Substantial.</strong></h3>
|
|
<p><strong>All the following changes cause changes to some entailments.</strong></p>
|
|
|
|
<p>1. The treatment of language tags in literals has been simplified. Typed literals,
|
|
including XML literals, no longer have associated language tags. (WG decision
|
|
recorded <a href="http://lists.w3.org/Archives/Public/w3c-rdfcore-wg/2003May/0138.html">http://lists.w3.org/Archives/Public/w3c-rdfcore-wg/2003May/0138.html)</a>
|
|
There are therefore three types of literal: plain without a language tag, plain
|
|
with a language tag, and typed literals. </p>
|
|
<p>XML literals are required to be in canonical form, and to denote entities
|
|
which are distinct from any character string.(WG decision recorded
|
|
<a href="http://lists.w3.org/Archives/Public/w3c-rdfcore-wg/2003Jun/0156.html">
|
|
http://lists.w3.org/Archives/Public/w3c-rdfcore-wg/2003Jun/0156.html</a>)</p>
|
|
|
|
<p>The chief effect of these decisions in this document is that XML literals can
|
|
be treated uniformly with other typed literals. However, the rdf semantic conditions
|
|
on <code>rdfs:XMLLiteral</code> are stated without explicit reference to datatypes
|
|
in order to make it possible for a conforming RDF inference system to avoid
|
|
full datatyping. The accounts of <code>rdfs:XMLLiteral</code> given for RDF,
|
|
and for RDF with datatyping, are in exact correspondence. This change is relevant
|
|
to the last call comments: <a href="http://www.w3.org/2001/sw/RDFCore/20030123-issues/#pfps-02">pfps-02</a>,
|
|
<a href="http://www.w3.org/2001/sw/RDFCore/20030123-issues/#pfps-06">pfps-06</a>,
|
|
<a href="http://www.w3.org/2001/sw/RDFCore/20030123-issues/#pfps-07">pfps-07</a>.</p>
|
|
<p>2. The treatment of <code>rdfs:subClassOf</code> and <code>rdfs:subPropertyOf</code>
|
|
has been changed. They are no longer required to satisfy 'iff' semantic conditions,
|
|
but only to be transitive and reflexive. This decision was taken as a result
|
|
of the felt need to support simple complete sets of inference rules for RDFS.
|
|
We are grateful to Herman ter Horst and Patel-Schneider for noticing the complexities
|
|
which arose from the older conditions, c.f.
|
|
<a href="http://www.w3.org/2001/sw/RDFCore/20030123-issues/#horst-01">horst-01</a>
|
|
et. seq.. (WG decision recorded <a href="http://lists.w3.org/Archives/Public/w3c-rdfcore-wg/2003Jul/0025.html">
|
|
http://lists.w3.org/Archives/Public/w3c-rdfcore-wg/2003Jul/0025.html</a>)</p>
|
|
|
|
<p>This has required changes to the RDFS entailment rules table. The older conditions
|
|
are now explained in informative sections as 'extensional' conditions, and corresponding
|
|
entailment rules discussed. </p>
|
|
|
|
<p>3. Plain literals, and literals typed with <code>xsd:string</code>, both denote
|
|
character strings. (WG decision recorded <a href="http://lists.w3.org/Archives/Public/w3c-rdfcore-wg/2003Jul/att-0393/rdfcore-2003-07-25-minutes.txt">
|
|
http://lists.w3.org/Archives/Public/w3c-rdfcore-wg/2003Jul/att-0393/rdfcore-2003-07-25-minutes.txt
|
|
</a> ) The semantics now states explicitly that these are the coextensive in
|
|
XSD interpretations and describes a corresponding inference rule.</p>
|
|
<p>4. The account of datatyped interpretations has been stated relative to a 'datatype
|
|
map' from URI references to datatypes. This change was introduced after email discussions with Patel-Schneider,
|
|
cf <a href="http://www.w3.org/2001/sw/RDFCore/20030123-issues/#pfps-08">pfps-08</a>
|
|
and <a href="http://www.w3.org/2001/sw/RDFCore/20030123-issues/#pfps-09">pfps-09</a>
|
|
et. seq.. <span class="newstuff">The previous treatment was not adequate to
|
|
support the intended entailments</span>. (WG decision recorded
|
|
<a href="http://lists.w3.org/Archives/Public/w3c-rdfcore-wg/2003May/0199.html">http://lists.w3.org/Archives/Public/w3c-rdfcore-wg/2003May/0199.html</a>)
|
|
</p>
|
|
|
|
<p> 5. LV is required to be the class extension of <code>rdfs:Literal</code> in
|
|
all RDFS interpretations, cf. <a href="http://www.w3.org/2001/sw/RDFCore/20030123-issues/#pfps-06">pfps-06</a>.
|
|
This clarifies and rationalizes <span class="newstuff">the treatment of rdfs:Literal
|
|
and supports the entailments</span> noted in <a href="http://www.w3.org/2001/sw/RDFCore/20030123-issues/#pfps-10">pfps-10</a>.
|
|
</p>
|
|
<p>6. The rule rdfD4 has been removed: given the change mentioned in 2. above,
|
|
it was no longer valid. The text notes that it is consistent to assert a subClass
|
|
relation between datatypes in this case. </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>
|
|
|