--- a/rdf-mt/index.html Fri May 10 10:50:29 2013 -0400
+++ b/rdf-mt/index.html Mon May 13 03:33:36 2013 -0500
@@ -79,12 +79,19 @@
};
</script>
<style type="text/css">
-.semantictable {background-color: #FFFFAA}
-.ruletable {background-color: #DDDDFF}
-.othertable {background-color: #FDFDFD}
+.semantictable {background-color: #FFFFAA; padding:0.5em;}
+.ruletable {background-color: #DDDDFF; padding:0.5em;}
+.othertable {background-color: #FDFDFD; padding:0.5em;}
.tabletitle {font-size: small; font-weight: bolder;}
-.technote {font-size:small; background: #ccccff;}
-.changenote {font-size: small; background: #ffccff;}
+.technote {font-size:small; background: #ccccff; padding: 0.5em; margin: 2em 1em;}
+.changenote {padding: 0.5em; margin: 2em 1em;font-size: small; background: #ffccff;}
+.fact {
+ padding: 0.5em;
+ margin: 1em 0;
+ position: relative;
+ clear: both;
+ background-color: #ffccaa;
+}
</style>
</head>
<body>
@@ -104,15 +111,15 @@
<section>
<h2 id="introduction">Introduction</h2>
<p>
- This document defines a model-theoretic semantics for RDF graphs and the RDF and RDFS vocabularies, providing an exact formal specification of when truth is preserved by transformations of RDF, or operations which derive RDF content from other RDF. Readers who are unfamiliar with model theory can find a brief introduction to the basic ideas and terminology in <a>Appendix A</a>. </p>
-<p>This specification is normative for RDF semantics and the validity of inference processes. However, there are many aspects of RDF meaning which are not covered by this semantics, including social issues of how IRIs are assigned meanings in use, and how the referents of IRIs are related to Web content expressed in other media such as natural language texts. Accounts of such extended notions of meaning will go beyond this specification, but MUST NOT violate the conditions described here. </p>
+ This document defines a model-theoretic semantics for RDF graphs and the RDF and RDFS vocabularies, providing an exact formal specification of when truth is preserved by transformations of RDF or operations which derive RDF content from other RDF. </p>
+<p>This specification is normative for RDF semantics and the validity of inference processes. There are many aspects of RDF meaning which are not described or specified by this semantics, including social issues of how IRIs are assigned meanings in use, and how the referents of IRIs are related to Web content expressed in other media such as natural language texts. Accounts of such extended notions of meaning will go beyond this specification, but MUST NOT violate the conditions described here. </p>
</section>
<section>
<h2 id="extensions">Semantic extensions and entailment regimes</h2>
<p>RDF is intended for use as a base notation for a variety of extended notations such as OWL [[OWL2-OVERVIEW]] and RIF [[RIF-OVERVIEW]], whose expressions can be encoded as RDF graphs which use a particular vocabulary with a specially defined meaning. Also, particular IRI vocabularies may impose user-defined meanings upon the basic RDF meaning rules. When such extra meanings are assumed, a given RDF graph may support more extensive entailments than are sanctioned by the basic RDF semantics. In general, the more assumptions that are made about the meanings of IRIs in an RDF graph, the more valid entailments it has. </p>
-<p>A particular such set of semantic assumptions is called a <dfn>semantic extension</dfn>. Each semantic extension defines an <dfn>entailment regime</dfn> of entailments which are valid under that extension. RDFS, described later in this document, is one such semantic extension. We will refer to an entailment regime by names such as <em>rdfs-entailment</em>, <em>D-entailment</em>, etc.. </p>
+<p>A particular such set of semantic assumptions is called a <dfn>semantic extension</dfn>. Each semantic extension defines an <dfn>entailment regime</dfn> of entailments which are valid under that extension. RDFS, described later in this document, is one such semantic extension. We will refer to an entailment regime by names such as <em>rdfs-entailment</em>, <em>D-entailment</em>, etc. </p>
<p>Semantic extensions MAY impose special syntactic conditions or restrictions upon RDF graphs, such as requiring certain triples to be present, or prohibiting particular combinations of IRIs in triples, and MAY consider RDF graphs which do not conform to these conditions to be errors. For example, RDF statements of the form <br/>
<code>ex:a rdfs:subClassOf owl:Thing .</code><br/>
@@ -125,22 +132,16 @@
<h2 id="notation">Notation and terminology</h2>
- <p>This document uses the following terminology for describing RDF graph syntax, all as defined in the companion Concepts specification [[RDF11-CONCEPTS]]: <em><a class="externalDFN">RDF triple</a>, <a class="externalDFN">RDF graph</a>, <a class="externalDFN">subject</a>, <a class="externalDFN">predicate</a>, <a class="externalDFN">object</a>, <a class="externalDFN">RDF source</a>, <a class="externalDFN">node</a>, <a class="externalDFN">RDF term</a>, <a class="externalDFN">blank node</a>, <a class="externalDFN">literal</a>, <a class="externalDFN">isomorphic</a>.</em></p>
+ <p>This document uses the following terminology for describing RDF graph syntax, all as defined in the companion Concepts specification [[!RDF11-CONCEPTS]]: <em><a class="externalDFN">RDF triple</a>, <a class="externalDFN">RDF graph</a>, <a class="externalDFN">subject</a>, <a class="externalDFN">predicate</a>, <a class="externalDFN">object</a>, <a class="externalDFN">RDF source</a>, <a class="externalDFN">node</a>, <a class="externalDFN">RDF term</a>, <a class="externalDFN">blank node</a>, <a class="externalDFN">literal</a>, <a class="externalDFN">isomorphic</a>.</em></p>
-<p>Throughout this document, the equality sign = indicates
- identity. The statement "A = B" means that there is one entity to which both expressions "A" and "B" refer. Angle brackets < x, y > are used to indicate an ordered pair
+<p>We use the words <dfn>denotes</dfn> and <dfn>refers to</dfn> interchangeably as synonyms for the relationship between an expression (usually an IRI) and what it refers to in a given interpretation, itself called the <dfn>referent</dfn> or <dfn>denotation</dfn>. IRI meanings may also be determined by other constraints external to the RDF semantics; when we wish to refer to such an externally defined naming relationship, we will use the word <dfn>identify</dfn> and its cognates. For example, the fact that the IRI <code>http://www.w3.org/2001/XMLSchema#decimal</code> is widely used as the name of a datatype described in the XML Schema document [[XMLSCHEMA11-2]] might be described by saying that the IRI <em>identifies</em> that datatype. If an IRI identifies something it may or may not refer to it in a given interpretation, depending on how the semantics is specified. For example, an IRI used as a graph name identifying a named graph in an <a class="external">RDF dataset</a> may refer to something different from the graph it identifies. </p>
+
+<p>Throughout this document, the equality sign = indicates strict identity. The statement "A = B" means that there is one entity to which both expressions "A" and "B" refer. </p>
+
+<p>Angle brackets < x, y > are used to indicate an ordered pair
of x and y. RDF graph syntax is indicated using the notational conventions of
- the N-Triples syntax described
- in the Turtle Working Draft [[TURTLE-TR]]
- literal strings are enclosed within double quote marks and attached to a type IRI using a double-caret <code>^^</code>, language tags indicated
- by the use of the <code>@</code> sign, and triples terminate with a 'code dot'
- <code>.</code> . </p>
-<p>In stating general rules or conditions we use the following conventions:</p>
-<p>sss, ttt, etc. indicate a Unicode character string; <br/>
-aaa, bbb, etc. indicate an IRI<br/>
-lll, mmm, etc. indicate a literal<br/>
-_:xxx, _:yyy, etc. indicate a blank node <br/>
-xxx, yyy, etc. indicate any component of a triple.</p>
+ the Turtle syntax described
+ in the Turtle Working Draft [[TURTLE-TR]]. Prefix definitions are omitted. When stating general rules or conditions we use three-character variables such as aaa, xxx, sss to indicate arbitrary IRIs, literals, or other components of RDF syntax. </p>
<p class="issue">Should the following definitions be in Concepts rather than here?</p>
@@ -184,50 +185,20 @@
of blank nodes between different RDF graphs. Simply downloading a
web document does not mean that the blank nodes in a resulting RDF
graph are the same as the blank nodes coming from other downloads of
-the same document or from the same source.
-</p>
-
-<p>Forming the union of a set of graphs preserves the identity of blank nodes shared between the graphs. A related process, called <dfn>merging</dfn>, first changes any blank nodes shared between two or more graphs so that none of the graphs share any blank nodes, then forms the union. The result is called the <dfn>merge</dfn> of the graphs in the set. </p>
-
-<p>For example, given the three graphs</p>
-
-<p><code><ex:a> <ex:p> _:x .</code></p>
-<p>and</p>
+the same document or from the same source. RDF applications which manipulate concrete syntaxes for RDF which use blank node identifiers must take care to keep track of the identity of the blank nodes they identify. Blank node identifiers often have a local scope, so when RDF from different sources is combined, identifiers may have to be re-named in order to avoid accidental conflation of distinct blank nodes.</p>
-<p><code>_:x <ex:q> <ex:b> . </code></p>
-<p>and</p>
-<p><code><ex:c> <ex:p> _:x .<br/>
-_:x <ex:q> <ex:d> .</code></p>
-<p> their union is</p>
-<p><code><ex:a> <ex:p> _:x .<br/>
-_:x <ex:q> <ex:b> . <br/>
-<ex:c> <ex:p> _:x .<br/>
-_:x <ex:q> <ex:d> .</code></p>
-
-<p>but the merge is</p>
-
-<p><code><ex:a> <ex:p> _:x1 .<br/>
-_:x2 <ex:q> <ex:b> . <br/>
-<ex:c> <ex:p> _:x3 .<br/>
-_:x3 <ex:q> <ex:d> .</code></p>
-
-<p>where the occurrences of the blank node _:x have been "standardized apart" by replacing each with a new blank node which is distinct from the blank nodes in the other graphs in the set. The particular blank node identifiers used in a text describing the graph, as here, have no significance outside the text. </p>
-
-<p>The merge of a set of graphs is unique (up to isomorphism.) A union or merge may be represented by a new RDF source, or may be thought of as a conceptual entity when describing RDF processing. This document will often treat a set of graphs as being identical to a single graph comprising their union, without further comment. </p>
+<p>Forming the union of a set of graphs preserves the identity of blank nodes shared between the graphs. This document will often treat a set of graphs as being identical to a single graph comprising their union, without further comment. </p>
<p >An RDF graph is <dfn>lean</dfn> if it has no instance which is
a proper subgraph of itself. Non-lean graphs have internal redundancy
and express the same content as their lean subgraphs. For example, the graph</p>
-<p ><code><ex:a> <ex:p> _:x .<br/>
- _:y <ex:p> _:x .</code></p>
+<p ><code>ex:a ex:p _:x .<br/>
+ _:y ex:p _:x .</code></p>
<p >is not lean, but</p>
-<p ><code><ex:a> <ex:p> _:x .<br/>
- _:x <ex:p> _:x .</code></p>
+<p ><code>ex:a ex:p _:x .<br/>
+ _:x ex:p _:x .</code></p>
<p >is lean. Ground graphs are lean. </p>
-<p>We use the words <dfn>denotes</dfn> and <dfn>refers to</dfn> interchangeably as synonyms for the relationship between an expression (usually an IRI) and what it refers to in a given interpretation, itself called the <em>referent</em> or <em>denotation</em>. IRI meanings may also be determined by other constraints external to the RDF semantics; when we wish to refer to such an externally defined naming relationship, we will use the word <dfn>identify</dfn> and its cognates. For example, the fact that the IRI <code>http://www.w3.org/2001/XMLSchema#decimal</code> is treated as the name of a datatype described in the XML Schema document [XMLSCHEMA11-2] might be described by saying that the IRI <em>identifies</em> that datatype. If an IRI identifies something it may or may not refer to it in a given interpretation, depending on how the semantics is specified. For example, an IRI used as a graph name identifying a named graph in an <a class="external">RDF dataset</a> may refer to something different from the graph it identifies. </p>
-
-
</section>
<section>
@@ -238,8 +209,8 @@
<div class="tabletitle">Definition of a simple interpretation.</div>
<table border="1">
<tr>
- <td class="semantictable"><p>1. A non-empty set IR of resources, called the domain or universe
- of I.</p>
+ <td class="semantictable">1. A non-empty set IR of resources, called the domain or universe
+ of I.
<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>
@@ -249,10 +220,10 @@
</tr>
</table>
-<ul><li><p class="changenote">The 2004 RDF 1.0 semantics defined interpretations relative to a vocabulary.<br/><br/>In the 2004 RDF 1.0 semantics, IL was a total, rather than partial, mapping.<br/><br/> The 2004 RDF 1.0 specification divided literals into 'plain' literals with no type and optional language tags, and typed literals. Usage has shown that it is important that every literal have a type. RDF 1.1 replaces plain literals without language tags by literals typed with the XML Schema <code>string</code> datatype, and introduces the special type <code>rdf:langString</code> for language-tagged strings. The full semantics for typed literals is given in the next section. </p>
+<p class="changenote">The 2004 RDF 1.0 semantics defined interpretations relative to a vocabulary.<br/><br/>In the 2004 RDF 1.0 semantics, IL was a total, rather than partial, mapping.<br/><br/> The 2004 RDF 1.0 specification divided literals into 'plain' literals with no type and optional language tags, and typed literals. Usage has shown that it is important that every literal have a type. RDF 1.1 replaces plain literals without language tags by literals typed with the XML Schema <code>string</code> datatype, and introduces the special type <code>rdf:langString</code> for language-tagged strings. The full semantics for typed literals is given in the next section. </p>
-</li><li><p class="technote"> Interpretations are required to interpret all names, and are therefore infinite. This simplifies the exposition. However, RDF can be interpreted using finite structures, supporting decidable algorithms. Details are given in Appendix ///. </p>
-</li></ul>
+<p class="technote"> Interpretations are required to interpret all names, and are therefore infinite. This simplifies the exposition. However, RDF can be interpreted using finite structures, supporting decidable algorithms. Details are given in Appendix ///. </p>
+
<p>IEXT(x), called
the <dfn>extension</dfn> of x, is a
@@ -261,10 +232,10 @@
</p>
<p>The distinction between IR and IL will become significant below when the semantics of datatypes are defined. IL is allowed to be partial because some literals may fail to have a referent. </p>
-<ul><li><p class="technote">
+<p class="technote">
It is conventional to map a relation name to a relational extension directly. This however presumes that the vocabulary is segregated into relation names and individual names, and RDF makes no such assumption. Moreover, RDF allows an IRI to be used as a relation name applied to itself as an argument. Such self-application structures are used in RDFS, for example. The use of the IEXT mapping to distinguish the relation as an object from its relational extension accommodates both of these requirements. It also provides for a notion of RDFS 'class' which can be distinguished from its set-theoretic extension.
</p>
-</li></ul>
+
<p>The denotation of a ground RDF graph in I is then given by the following
@@ -304,8 +275,9 @@
<p> The final condition implies that the empty graph (the empty set of triples) is always true.</p>
<p>The sets IP and IR may overlap, indeed IP can be a subset of IR. Because of the domain conditions on IEXT, the denotation of the subject and object of any true triple will be in IR; so any IRI which occurs in a graph both as a predicate and as a subject or object will denote something in the intersection of IP and IR.</p>
-<p>Semantic extensions may impose further constraints upon interpretation mappings by requiring some IRIs to refer in particular ways. For example, D-interpretations, described below, require some IRIs, understood as identifying and referring to datatypes. to have a fixed interpretation. </p>
+<p>Semantic extensions may impose further constraints upon interpretation mappings by requiring some IRIs to refer in particular ways. For example, D-interpretations, described below, require some IRIs, understood as identifying and referring to datatypes, to have a fixed interpretation. </p>
+<section>
<h3 id="blank_nodes">Blank Nodes</h3>
@@ -331,9 +303,8 @@
Blank nodes themselves differ from other nodes in not being assigned
a denotation by an interpretation, reflecting the intuition that
they have no 'global' meaning. </p>
-<p>While a blank node may occur in more than one graph, the truth conditions refer only to its occurrences inside the graph whose truth is being determined. This affects the way that graphs can be validly combined, as described in later sections.
-</p>
-
+</section>
+<section>
<h3 id="intuitions">Intuitive summary</h3>
<p>An RDF graph is true exactly when:</p>
@@ -342,14 +313,15 @@
<p>All semantic extensions of any vocabulary or higher-level notation encoded in RDF MUST conform to these minimal truth conditions. Other semantic extensions may extend and add to these, but they MUST NOT modify or negate them. For example, because interpretations are mappings which apply to IRIs, a semantic extension MUST NOT interpret different occurrences of a single IRI differently.</p>
</section>
+</section>
<section id="simpleentailment"><h2>Simple Entailment</h2>
-<p>Following standard terminology, we say that I <dfn>satisfies</dfn> E when I(E)=true, that E is <dfn>satisfiable</dfn> when an interpretation exists which satisfies it, (otherwise <dfn>inconsistent</dfn>), and that a set
- S of RDF graphs <dfn>simply entails</dfn> a graph E when every interpretation
- which satisfies every member of S also satisfies E. This means that it is always correct to infer E from S, even when one does not know what the names in the vocabulary actually mean. 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>Following standard terminology, we say that I <dfn>satisfies</dfn> E when I(E)=true, that E is <dfn>satisfiable</dfn> when an interpretation exists which satisfies it, (otherwise <dfn>unsatisfiable</dfn>), that a graph G <dfn>simply entails</dfn> a graph E when every interpretation which satisfies G also satisfies E, and that a set S of graphs simply entails E when the union of S simply entails 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 class="changenote">This definition treats a set of graphs identically to its union, unlike the definition used in the 2004 RDF 1.0 Semantics. This is more appropriate for the case where graphs may share blank nodes. If this case does not arise, this definition is exactly equivalent to the previous definition.</p>
+
<p><a id="defvalid">Any process which constructs a graph E from
some other graph(s) S is (simply) <dfn>valid</dfn> if S
simply entails E in every case, otherwise <dfn>invalid.</dfn></a></p>
@@ -358,84 +330,92 @@
<p>Entailment refers only to the truth of RDF graphs, not to their suitability for any other purpose. It is possible for an RDF graph to be fitted for a given purpose and yet validly entail another graph which is not appropriate for the same purpose. An example is the RDF test cases manifest [[!RDF-TESTCASES]] which is provided as an RDF document for user convenience. This document lists examples of correct entailments by describing their antecedents and conclusions. Considered as an RDF graph, the manifest simply entails a subgraph which omits the antecedents, and would therefore be incorrect if used as a test case manifest. This is not a violation of the RDF semantic rules, but it shows that the property of <em> "being a correct RDF test case manifest"</em> is not preserved under RDF entailment, and therefore cannot be described as an RDF semantic extension. Such entailment-risky uses of RDF should be restricted to cases, as here, where it is obvious to all parties what the intended special restrictions on entailment are, in contrast with the more normal case of using RDF for the open publication of data on the Web.</p>
-</section>
+
<section>
<h3>Properties of simple entailment. </h3>
<p>The properties described here apply only to simple entailment, not to extended notions of entailment introduced in later sections. </p>
+<p class="fact">Every graph is satisfiable.</p>
+<p>This does not hold for extended notions of interpretation. A graph containing an <a>ill-typed</a> literal is D-unsatisfiable.</p>
<p>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 <code>(P and Q)</code> to <code>P</code>, and the inference from <code>foo(baz)</code> to <code>(exists (x) foo(x) ) </code>. The first corresponds to taking a subgraph of a graph, the second to replacing an IRI or literal with a blank node. More precisely, the following <dfn>interpolation</dfn> <strong>lemma</strong> </p>
- <p>==
- S simply entails a graph E if and only if a subgraph of S is an instance of E. </a>
-<!-- <a href="#interplemmaprf" class="termref">[Proof]</a> -->
+ <p class="fact">
+ G simply entails a graph E if and only if a subgraph of G is an instance of E.
</p>
<p> completely characterizes simple entailment in syntactic
terms. To tell whether a set of RDF graphs simply entails another, check that
there is some instance of the entailed graph which is a subset of the union
of the original set of graphs. </p>
-<p>This is clearly decidable, but it is also complex in general, since one can encode the NP-hard subgraph problem (detecting whether one mathematical graph is a subgraph of another) as detecting simple entailment between RDF graphs. ([[Refer to Jeremy Carroll.]]) This uses graphs containing many blank nodes, which are unlikely to occur in practice. The complexity of checking simple entailment is reduced by having fewer blank nodes in the conclusion E. When E is a <a>ground</a> graph, it is simply a matter of checking the subset relationship on sets of triples.</p>
+<p class="technote">This is clearly decidable, but it is also complex in general, since one can encode the NP-hard subgraph problem (detecting whether one mathematical graph is a subgraph of another) as detecting simple entailment between RDF graphs. ([[Refer to Jeremy Carroll.]]) This uses graphs containing many blank nodes, which are unlikely to occur in practice. The complexity of checking simple entailment is reduced by having fewer blank nodes in the conclusion E. When E is a <a>ground</a> graph, it is simply a matter of checking the subset relationship on sets of triples.</p>
<p><a>Interpolation</a> has a number of direct consequences, for example:</p>
-<p>== The <a>empty graph</a> is entailed by
+<p class="fact"> The <a>empty graph</a> is entailed by
any graph, and does not entail any graph except itself.
<!-- <a href="#emptygraphlemmaprf" class="termref">[Proof]</a> -->
</p>
-<p> == A graph entails all its subgraphs.
+<p class="fact"> A graph entails all its subgraphs.
<!-- <a href="#subglemprf" class="termref">[Proof]</a> -->
</p>
-<p>== A graph
+<p class="fact"> A graph
is entailed by any of its <a>instance</a>s.
<!-- <a href="#instlemprf" class="termref"> [Proof]</a> -->
</p>
-<p>== If
- E is a <a>lean</a> graph and E' is a <a>proper instance</a> of E, then E does
+<p class="fact"> If
+ E is a consistent <a>lean</a> graph and E' is a <a>proper instance</a> of E, then E does
not simply entail E'.
</p>
-<p>== If S is a subgraph of S' and S entails E, then S' entails E.
+<p class="fact"> If S is a subgraph of S' and S entails E, then S' entails E.
<!-- <a href="#monotonicitylemmaprf" class="termref"> [Proof]</a> -->
</p>
-<p>==
+<p class="fact">
If S entails a finite graph E, then some finite subset S' of S entails E.
<!-- <a href="#compactlemmaprf" class="termref"> [Proof]</a> -->
</p>
<p>
This property is often called <em>compactness</em>. RDF is compact. As RDF graphs can be infinite, this is sometimes important.</p>
-<p>== If E contains an IRI which does not occur anywhere in S, then S does not entail E.</p>
-
-<p>Obviously, the union of a set of graphs entails every member of the set, since they are all subgraphs of the union. However, if two or more graphs in the set share a blank node. then the set may fail to entail the union. For example, consider the graphs</p>
-<p>
-<code>:a :p _:x . </code></p>
-<p>and</p>
-<p>
-<code>:b :p _:x .</code></p>
-<p>Both graphs can be satisfied by an interpretation which does not satisfy their union, e.g. one with <br/>IEXT(I(<code>:p</code>)) = {< I(<code>:a</code>),I(<code>:a</code>) >, < I(<code>:b</code>),I(<code>:b</code>) > }. This is because the mapping <code>_:x</code>/I(<code>:a</code>) works for the first graph, and the mapping <code>_:x</code>/I(<code>:b</code>) for the second graph, but there is no mapping which makes the combination true. Neither graph, taken alone as a single graph, is obliged to consider the full set of constraints on the blank node that are represented by their union. </p>
+<p class="fact"> If E contains an IRI which does not occur anywhere in S, then S does not entail E.</p>
-<p>Say that a set of graphs is <dfn>segregated</dfn> when no two graphs in the set share a blank node. Then:</p>
-
-<p>== the union
- of a <a>segregated</a> set of RDF graphs is entailed by the set, and entails every member of the set.
+<p>When forming the union of graphs, care must be taken over the identity of blank nodes. The process of taking two subgraphs of an RDF graph, treating each subgraph as a separate graph, and then re-combining them by creating the union of these separated graphs, does not yield the original graph when the subgraphs share a common blank node. For example, the following graph contains three nodes:</p>
-</p>
- <p>This means that a <a>segregated</a> set of graphs can be treated as equivalent to its
- union, a single graph. </p>
+<p><code>ex:a ex:p _:x .<br/>
+ex:b ex:q _:x .</code></p>
-<p>Creating a <a>merge</a> can be described as first modifying the set to ensure that it is <a>segregated</a>, then creating the union. Since a blank node replacement operation does not change the truth conditions of any single graph, </p>
-<p>== the merge of any set of graphs entails and is entailed by the set. </p>
-<p>However, when the graphs share blank nodes, the merge loses information compared to the union. In general, when two graphs share blank nodes they should usually be treated as parts of a single RDF graph.</p>
+<p>If the two triples in this graph are treated as two separate graphs</p>
+<p><code>ex:a ex:p _:x . </code></p>
+
+<p>and</p>
+
+<p><code>ex:b ex:q _:x . </code></p>
+
+<p>then the two occurrences of the blank node identifier must be understood to identify distinct blank nodes, which remain distinct when the union of these graphs is created. The resulting union</p>
+
+<p><code>ex:a ex:p _:x1 .<br/>
+ex:b ex:q _:x2 .</code></p>
+
+
+<p>contains four nodes rather than three, and is entailed by the original graph but does not entail it. </p>
+
+<p>This process of combining graphs while forcing a separation of their blank nodes is called <dfn>merging</dfn>, and the result of merging a set of graphs is called its <dfn>merge</dfn>. Merging is typically achieved, as here, by replacing blank node identifiers in the surface syntax to avoid accidentally identifying distinct blank nodes identified by the same blank node identifier in different identifier scopes. </p>
+
+<p class="fact"> The merge of a set of graphs is entailed by the set, and entails every graph in the set. </p>
+
+<p>As the above example illustrates, the fact that G entails every member of S does not imply that G entails the union of S. </p>
+
+</section>
</section>
<section><h2 id="skolemization">Skolemization</h2>
-<p>Skolemization is a transformation on RDF graphs which eliminates blank nodes by replacing them with "new" IRIs, which means IRIs which are coined for this purpose and are therefore guaranteed to not occur in any other RDF graph (at the time of creation). See [[RDF11-CONCEPTS]] for a fuller discussion. </p>
+<p><a class="externaldefinition">Skolemization</a> is a transformation on RDF graphs which eliminates blank nodes by replacing them with "new" IRIs, which means IRIs which are coined for this purpose and are therefore guaranteed to not occur in any other RDF graph (at the time of creation). See [[RDF11-CONCEPTS]] for a fuller discussion. </p>
<p> Suppose G is a graph containing blank nodes and sk is a skolemization mapping on the blank nodes in G, so that sk(G) is a skolemization of G. Then the semantic relationship between them can be summarized as follows. </p>
-<p>== sk(G) simply entails G (since sk(G) is an instance of G.)</p>
-<p>== G does not entail sk(G) (since sk(G) contains IRIs not in G.) </p>
-<p>== For any graph H, if sk(G) entails H then there is a graph H' such that G entails H' and H=sk(H') . </p>
-<p>== For any graph H which does not contain any of the "new" IRIs introduced into sk(G), sk(G) simply entails H if and only if G simply entails H.
+<p class="fact"> sk(G) simply entails G (since sk(G) is an instance of G.)</p>
+<p class="fact"> G does not entail sk(G) (since sk(G) contains IRIs not in G.) </p>
+<p class="fact"> For any graph H, if sk(G) entails H then there is a graph H' such that G entails H' and H=sk(H') . </p>
+<p class="fact"> For any graph H which does not contain any of the "new" IRIs introduced into sk(G), sk(G) simply entails H if and only if G simply entails H.
</p>
<p>The second property means that a graph is not logically <a>equivalent</a> to its skolemization. Nevertheless, they are in a strong sense almost interchangeable, as shown the next two properties. The third property means that even when conclusions are drawn from the skolemized graph which do contain the new vocabulary, these will exactly mirror what could have been derived from the original graph with the original blank nodes in place. The replacement of blank nodes by IRIs does not effectively alter what can be validly derived from the graph, other than by giving new names to what were formerly anonymous entities. The fourth property, which is a consequence of the third, clearly shows that in some sense a skolemization of G can "stand in for" G as far as entailments are concerned. Using sk(G) instead of G will not affect any entailments which do not involve the new skolem vocabulary. </p>
@@ -445,11 +425,11 @@
</section>
<section><h2 id="datatypes">Literals and datatypes</h2>
-<ul><li><p class="changenote"> In the 2004 RDF 1.0 specification, datatype D-entailment was defined as a semantic extension of RDFS-entailment. Here it is defined as a direct extension to basic RDF. This is more in conformity with actual usage, where RDF with datatypes is widely used without the RDFS vocabulary. If there is a need to distinguish this from the 2004 RDF 1.0 terminology, the longer phrasing "simple D-entailment" or "simple datatype entailment" should be used rather than "D-entailment". </p>
-</li></ul>
+<p class="changenote"> In the 2004 RDF 1.0 specification, datatype D-entailment was defined as a semantic extension of RDFS-entailment. Here it is defined as a direct extension to basic RDF. This is more in conformity with actual usage, where RDF with datatypes is widely used without the RDFS vocabulary. If there is a need to distinguish this from the 2004 RDF 1.0 terminology, the longer phrasing "simple D-entailment" or "simple datatype entailment" should be used rather than "D-entailment". </p>
+
<p>RDF literals and datatypes are fully described in [[!RDF11-CONCEPTS]]. In summary: RDF literals are either language-tagged strings, or datatyped literals which
-combine a string and an IRI identifying a datatype. A datatype is understood to define a partial mapping, called the <dfn>lexical-to-value mapping</dfn>, from character strings to values, and the literal refers to (denotes) the value obtained by applying this mapping to the character string. If the mapping gives no value for the literal string, then the literal has no referent. The <dfn>value space</dfn> of a datatype is the range of the <a>lexical-to-value mapping</a>. Every literal with that type either refers to a value in the value space of the type, or fails to refer at all. An <dfn>ill-typed</dfn> literal is one whose datatype IRI is recognized, but whose character string is not in the domain of the datatype lexical-to-value mapping. </p>
+combine a string and an IRI identifying a datatype. A datatype is understood to define a partial mapping, called the <dfn>lexical-to-value mapping</dfn>, from character strings to values. The function L2V maps datatypes to their lexical-to-value mapping. A literal with datatype d refers to (denotes) the value obtained by applying this mapping to the character string: L2V(d)(string). If the mapping gives no value for the literal string, then the literal has no referent. The <dfn>value space</dfn> of a datatype is the range of the <a>lexical-to-value mapping</a>. Every literal with that type either refers to a value in the value space of the type, or fails to refer at all. An <dfn>ill-typed</dfn> literal is one whose datatype IRI is recognized, but whose character string is assigned no value by the lexical-to-value mapping for that datatype. </p>
<p> Datatypes are identified by IRIs. Interpretations will vary according to which IRIs they recognize as denoting datatypes. We describe this using a parameter D on interpretations. where D is the set of recognized datatype IRIs. </p>
@@ -462,29 +442,32 @@
</section>
-<section id="D_interpretations"><h2>D-interpretations and datatype entailment</h2>
+<section id="D_interpretations"><h2>D-interpretations</h2>
<p>Let D be a set of IRIs identifying datatypes. A <dfn>(simple) D-interpretation</dfn> is a simple interpretation which satisfies the following conditions:</p>
<div class="tabletitle">Semantic conditions for datatyped literals.</div>
-<table border="1" class="semantictable">
+<table border="1">
<tbody>
-<tr><td>If <code>rdf:langString</code> is in D, then for every language-tagged string E with lexical form sss and language tag ttt, IL(E)= < sss, ttt > </td></tr>
-<tr><td>For every other IRI aaa in D, and every literal "sss"^^aaa, IL("sss"^^aaa) = L2V(I(aaa))(sss)</td></tr>
+<tr><td class="semantictable">If <code>rdf:langString</code> is in D, then for every language-tagged string E with lexical form sss and language tag ttt, IL(E)= < sss, ttt > </td></tr>
+<tr><td class="semantictable">For every other IRI aaa in D, and every literal "sss"^^aaa, IL("sss"^^aaa) = L2V(I(aaa))(sss)</td></tr>
</tbody></table>
-<p>If the literal is ill-typed then the L2V mapping has no value, and so the literal cannot denote anything. In this case, any triple containing the literal must be false. Thus, any triple, and hence any graph, containing an ill-typed literal will be D-inconsistent, i.e. false in every D-interpretation. This applies only to datatype IRIs in D; literals with "unknown" datatypes are not ill-typed and do not produce a D-inconsistency. </p>
+<p>If the literal is ill-typed then the L2V(I(aaa)) mapping has no value, and so the literal cannot denote anything. In this case, any triple containing the literal must be false. Thus, any triple, and hence any graph, containing an ill-typed literal will be D-unsatisfiable, i.e. false in every D-interpretation. This applies only to datatype IRIs in D; literals with "unknown" datatypes are not ill-typed and do not produce a D-inconsistency. </p>
<p>The built-in RDF datatypes <code>rdf:langString</code> and <code>xsd:string</code> have no ill-typed literals. Any literal with these types which is syntactically legal in RDF will denote a value in every RDF interpretation. </p>
-<p>It follows from the definitions that an inconsistent graph entails every graph. This is called the principle of '<a href="http://en.wikipedia.org/wiki/Principle_of_explosion">ex falso quodlibet</a>'.</p>
+<p class="issue">Is this true? Is "\u0000"^^xsd:string ill-formed or syntactically illegal? What about "foodle"@700 ?</p>
-<ul><li><p class="changenote"> In the 2004 RDF 1.0 specification, ill-typed literals were required to denote a value in IR, and D-inconsistency could only be recognized by using the RDFS semantics. </p>
-</li></ul>
+<p class="changenote"> In the 2004 RDF 1.0 specification, ill-typed literals were required to denote a value in IR, and D-inconsistency could only be recognized by using the RDFS semantics. </p>
+
+
+</section>
+<section>
<h3 id="D_entailment">Datatype entailment</h3>
<p>A graph is (simply) <dfn>D-satisfiable</dfn> when it has the value true in some D-interpretation, and a set S of graphs (simply) <dfn>D-entails</dfn> a graph G when every D-interpretation which makes S true also D-satisfies G.</p>
@@ -495,9 +478,9 @@
-<section> <h4>Patterns of Datatype entailment</h4>
+<section> <h4>Patterns of datatype entailment</h4>
<p>Unlike simple entailment, it is not possible to give a single syntactic criterion to recognize all D-entailments, which
-can hold because of particular properties of the lexical-to-value mappings of the recognized datatypes. For example, if D contains <code>xsd:real</code> then </p>
+can hold because of particular properties of the lexical-to-value mappings of the recognized datatypes. For example, if D contains <code>xsd:decimal</code> then </p>
<p><code>ex:a ex:p "25.0"^^xsd:decimal .</code></p>
@@ -516,7 +499,7 @@
</section>
</section>
-<section><h2 id="rdf_d_interpretations">RDF-D Interpretations and RDF entailment</h2>
+<section><h2 id="rdf_d_interpretations">RDF-D Interpretations</h2>
<p >RDF-D interpretations impose extra semantic conditions on <code>xsd:string</code> and part of the infinite
set of IRIs in the <code>rdf:</code> namespace.
@@ -585,16 +568,16 @@
<th ><strong>then S RDF-D-entails</strong></th>
</tr>
<tr >
- <td>rdfD1</td>
- <td> xxx aaa <code>"</code>sss<code>"^^</code>ddd <code>.</code> <br/>
+ <td class="othertable">rdfD1</td>
+ <td class="othertable"> xxx aaa <code>"</code>sss<code>"^^</code>ddd <code>.</code> <br/>
for ddd in D</td>
- <td>xxx aaa _:nnn <code>.</code><br/>
+ <td class="othertable">xxx aaa _:nnn <code>.</code><br/>
_:nnn <code>rdf:type</code> ddd <code>.</code></td>
</tr>
</tbody>
</table>
-<p>Note, this is valid even when the literal is ill-typed, since a contradiction entails any triple.</p>
+<p>Note, this is valid even when the literal is ill-typed, since an inconsistent graph entails any triple.</p>
<p>For example,</p>
<p> <code>ex:a ex:p "123"^^xsd:integer .</code></p>
@@ -615,9 +598,9 @@
</tr>
<tr>
- <td>rdfD2</td>
- <td>xxx aaa yyy <code>.</code></td>
- <td>aaa <code>rdf:type rdf:Property .</code> </td>
+ <td class="othertable">rdfD2</td>
+ <td class="othertable">xxx aaa yyy <code>.</code></td>
+ <td class="othertable">aaa <code>rdf:type rdf:Property .</code> </td>
</tr>
@@ -641,7 +624,7 @@
</section>
</section>
-<section><h2>RDFS Interpretations and RDFS entailment</h2>
+<section><h2>RDFS Interpretations</h2>
<p>RDF Schema [[RDF-SCHEMA]]
extends RDF to a larger vocabulary
with more complex semantic constraints:</p>
@@ -669,9 +652,8 @@
and <code>rdfs:subPropertyOf</code>. Other than this, the formal semantics does
not constrain their 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"><em>class</em></a>, i.e. a resource which represents
- a set of things in the universe which all have that class as the value of their
+ in terms of a new semantic construct, a <dfn>class</dfn>, i.e. a resource which represents
+ a set of things in the universe which all have that class as a 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
@@ -818,8 +800,8 @@
</table>
-<ul><li><p class="changenote">In the 2004 RDF 1.0 semantics, LV was defined as part of a simple interpretation structure, and the definition given here was a constraint. </p>
-</li></ul>
+<p class="changenote">In the 2004 RDF 1.0 semantics, LV was defined as part of a simple interpretation structure, and the definition given here was a constraint. </p>
+
<p>Since I is an rdf-interpretation, the first condition implies that IP
= ICEXT(I(<code>rdf:Property</code>)).</p>
@@ -861,10 +843,10 @@
</tr>
</table>
-<p>RDFS does not partition the universe into disjoint categories of classes, properties and individuals. Anything in the universe can be used as a class or as a property, or both, while retaining its status as an individual which may be in classes and have properties. Thus, RDFS permits classes which contain other classes, classes of properties, properties of classes, etc. . As the axiomatic triples above illustrate, it also permits classes which contain themselves and properties which apply to themselves. A property of a class is not necessarily a property of its members, nor vice versa. </p>
+<p>RDFS does not partition the universe into disjoint categories of classes, properties and individuals. Anything in the universe can be used as a class or as a property, or both, while retaining its status as an individual which may be in classes and have properties. Thus, RDFS permits classes which contain other classes, classes of properties, properties of classes, etc. As the axiomatic triples above illustrate, it also permits classes which contain themselves and properties which apply to themselves. A property of a class is not necessarily a property of its members, nor vice versa. </p>
<section>
<h4>A note on rdfs:Literal</h3>
-<p>The class <code>rdfs:Literal</code> is not the class of literals, but rather that of literal values, which may also be referred to by IRIs. For example, LV does not contain the literal <code>"24"^^xsd:integer</code> (although it does contain the Unicode string '<em> "24"^^http://www.w3.org/2001/XMLSchema#integer </em>' ) but it does contain the number twenty-four.</p>
+<p>The class <code>rdfs:Literal</code> is not the class of literals, but rather that of literal values, which may also be referred to by IRIs. For example, LV does not contain the literal <code>"24"^^xsd:integer</code> but it does contain the number twenty-four.</p>
<p>A triple of the form</p>
@@ -900,80 +882,80 @@
<th >then S RDFS-D-entails:</th>
</tr>
<tr >
- <td><dfn>rdfs1</dfn></td>
- <td>any IRI aaa in D</td>
- <td>aaa <code>rdf:type rdfs:Datatype . </code></td>
- </tr>
- <tr >
- <td><dfn>rdfs2</dfn></td>
- <td> aaa <code>rdfs:domain</code> xxx <code>.</code><br />
- yyy aaa zzz <code>.</code></td>
- <td>yyy <code>rdf:type</code> xxx <code>.</code></td>
- </tr>
- <tr >
- <td></a><dfn>rdfs3</dfn></td>
- <td>aaa <code>rdfs:range</code> xxx <code>.</code><br />
- yyy aaa zzz <code>.</code></td>
- <td>zzz <code>rdf:type</code> xxx <code>.</code></td>
- </tr>
- <tr >
- <td><dfn>rdfs4a</dfn></td>
- <td>xxx aaa yyy <code>.</code></td>
- <td>xxx <code>rdf:type rdfs:Resource .</code></td>
- </tr>
- <tr >
- <td><dfn>rdfs4b</dfn></td>
- <td>xxx aaa yyy<code>.</code></td>
- <td>yyy <code>rdf:type rdfs:Resource .</code></td>
- </tr>
- <tr >
- <td><dfn>rdfs5</dfn></td>
- <td> xxx <code>rdfs:subPropertyOf</code> yyy <code>.</code><br />
- yyy <code>rdfs:subPropertyOf</code> zzz <code>.</code></td>
- <td>xxx <code>rdfs:subPropertyOf</code> zzz <code>.</code></td>
+ <td class="othertable"><dfn>rdfs1</dfn></td>
+ <td class="othertable">any IRI aaa in D</td>
+ <td class="othertable">aaa <code>rdf:type rdfs:Datatype . </code></td>
</tr>
<tr >
- <td><dfn>rdfs6</dfn></td>
- <td>xxx <code>rdf:type rdf:Property .</code></td>
- <td>xxx <code>rdfs:subPropertyOf</code> xxx <code>.</code></td>
- </tr>
- <tr >
- <td><dfn>rdfs7</dfn></td>
- <td> aaa <code>rdfs:subPropertyOf</code> bbb <code>.</code><br />
- xxx aaa yyy <code>.</code></td>
- <td>xxx bbb yyy <code>.</code></td>
- </tr>
- <tr >
- <td><dfn>rdfs8</dfn></td>
- <td>xxx <code>rdf:type rdfs:Class .</code></td>
- <td>xxx <code>rdfs:subClassOf rdfs:Resource .</code></td>
+ <td class="othertable"><dfn>rdfs2</dfn></td>
+ <td class="othertable"> aaa <code>rdfs:domain</code> xxx <code>.</code><br />
+ yyy aaa zzz <code>.</code></td>
+ <td class="othertable">yyy <code>rdf:type</code> xxx <code>.</code></td>
</tr>
<tr >
- <td><dfn>rdfs9</dfn></td>
- <td>xxx <code>rdfs:subClassOf</code> yyy <code>.</code><br />
- zzz <code>rdf:type</code> xxx <code>.</code></td>
- <td>zzz <code>rdf:type</code> yyy <code>.</code></td>
- </tr>
- <tr >
- <td><dfn>rdfs10</dfn></td>
- <td>xxx <code>rdf:type rdfs:Class .</code></td>
- <td>xxx <code>rdfs:subClassOf</code> xxx <code>.</code></td>
+ <td class="othertable"></a><dfn>rdfs3</dfn></td>
+ <td class="othertable">aaa <code>rdfs:range</code> xxx <code>.</code><br />
+ yyy aaa zzz <code>.</code></td>
+ <td class="othertable">zzz <code>rdf:type</code> xxx <code>.</code></td>
</tr>
<tr >
- <td><dfn>rdfs11</dfn></td>
- <td> xxx <code>rdfs:subClassOf</code> yyy <code>.</code><br />
- yyy <code>rdfs:subClassOf</code> zzz <code>.</code></td>
- <td>xxx <code>rdfs:subClassOf</code> zzz <code>.</code></td>
+ <td class="othertable"><dfn>rdfs4a</dfn></td>
+ <td class="othertable">xxx aaa yyy <code>.</code></td>
+ <td class="othertable">xxx <code>rdf:type rdfs:Resource .</code></td>
</tr>
<tr >
- <td><dfn>rdfs12</dfn></td>
- <td>xxx <code>rdf:type rdfs:ContainerMembershipProperty .</code></td>
- <td>xxx <code>rdfs:subPropertyOf rdfs:member .</code></td>
+ <td class="othertable"><dfn>rdfs4b</dfn></td>
+ <td class="othertable">xxx aaa yyy<code>.</code></td>
+ <td class="othertable">yyy <code>rdf:type rdfs:Resource .</code></td>
</tr>
<tr >
- <td><dfn>rdfs13</dfn></td>
- <td>xxx <code>rdf:type rdfs:Datatype .</code></td>
- <td>xxx <code>rdfs:subClassOf rdfs:Literal .</code></td>
+ <td class="othertable"><dfn>rdfs5</dfn></td>
+ <td class="othertable"> xxx <code>rdfs:subPropertyOf</code> yyy <code>.</code><br />
+ yyy <code>rdfs:subPropertyOf</code> zzz <code>.</code></td>
+ <td class="othertable">xxx <code>rdfs:subPropertyOf</code> zzz <code>.</code></td>
+ </tr>
+ <tr >
+ <td class="othertable"><dfn>rdfs6</dfn></td>
+ <td class="othertable">xxx <code>rdf:type rdf:Property .</code></td>
+ <td class="othertable">xxx <code>rdfs:subPropertyOf</code> xxx <code>.</code></td>
+ </tr>
+ <tr >
+ <td class="othertable"><dfn>rdfs7</dfn></td>
+ <td class="othertable"> aaa <code>rdfs:subPropertyOf</code> bbb <code>.</code><br />
+ xxx aaa yyy <code>.</code></td>
+ <td class="othertable">xxx bbb yyy <code>.</code></td>
+ </tr>
+ <tr >
+ <td class="othertable"><dfn>rdfs8</dfn></td>
+ <td class="othertable">xxx <code>rdf:type rdfs:Class .</code></td>
+ <td class="othertable">xxx <code>rdfs:subClassOf rdfs:Resource .</code></td>
+ </tr>
+ <tr >
+ <td class="othertable"><dfn>rdfs9</dfn></td>
+ <td class="othertable">xxx <code>rdfs:subClassOf</code> yyy <code>.</code><br />
+ zzz <code>rdf:type</code> xxx <code>.</code></td>
+ <td class="othertable">zzz <code>rdf:type</code> yyy <code>.</code></td>
+ </tr>
+ <tr >
+ <td class="othertable"><dfn>rdfs10</dfn></td>
+ <td class="othertable">xxx <code>rdf:type rdfs:Class .</code></td>
+ <td class="othertable">xxx <code>rdfs:subClassOf</code> xxx <code>.</code></td>
+ </tr>
+ <tr >
+ <td class="othertable"><dfn>rdfs11</dfn></td>
+ <td class="othertable"> xxx <code>rdfs:subClassOf</code> yyy <code>.</code><br />
+ yyy <code>rdfs:subClassOf</code> zzz <code>.</code></td>
+ <td class="othertable">xxx <code>rdfs:subClassOf</code> zzz <code>.</code></td>
+ </tr>
+ <tr >
+ <td class="othertable"><dfn>rdfs12</dfn></td>
+ <td class="othertable">xxx <code>rdf:type rdfs:ContainerMembershipProperty .</code></td>
+ <td class="othertable">xxx <code>rdfs:subPropertyOf rdfs:member .</code></td>
+ </tr>
+ <tr >
+ <td class="othertable"><dfn>rdfs13</dfn></td>
+ <td class="othertable">xxx <code>rdf:type rdfs:Datatype .</code></td>
+ <td class="othertable">xxx <code>rdfs:subClassOf rdfs:Literal .</code></td>
</tr>
</tbody>
</table>
@@ -985,16 +967,16 @@
</section>
-<section><h3>Complete sets of entailment rules (Informative)</h3>
+<section class="appendix"><h3>Entailment rules (Informative)</h3>
-<p>(This section is based on work described more fully in [[terHorst1]], [[terHorst2]], which should be consulted for technical details and proofs.) </p>
+<p>This section is based on work described more fully in [[terHorst1]], [[terHorst2]], which should be consulted for technical details and proofs. </p>
<p> The RDF and RDFS entailment patterns listed in the above tables can be viewed as left-to-right rules which add the entailed conclusion to a graph. These rule sets can be used to check RDF- (or RDFS-) entailment between graphs S and E, by the following sequence of operations:</p>
-<p>1. Add to S all the RDF (and RDFS) axiomatic triples except those containing the container membership property IRIs <code>rdf:_1, rdf:_2, ...</code>.<br/>
-2. For every container membership property IRI which occurs in E, add the RDF (and RDFS) axiomatic triples which contain that IRI.<br/>
-3. Apply the RDF (and RDFS) inference patterns as rules, adding each conclusion to the graph, to exhaustion; that is, until they generate no new triples. <br/>
+<p>1. Add to S all the RDF (or RDF and RDFS) axiomatic triples except those containing the container membership property IRIs <code>rdf:_1, rdf:_2, ...</code>.<br/>
+2. For every container membership property IRI which occurs in E, add the RDF (or RDF and RDFS) axiomatic triples which contain that IRI.<br/>
+3. Apply the RDF (or RDF and RDFS) inference patterns as rules, adding each conclusion to the graph, to exhaustion; that is, until they generate no new triples. <br/>
4. Determine if E has an instance which is a subset of the set, i.e. whether the enlarged set simply entails E.</p>
-This process is clearly correct, in that if it gives a positive result then indeed S does RDF-(RDFS-) entail E. It is not, however, complete: there are cases of S entailing E which are not detectable by this process. Examples include:</p>
+This process is clearly <a>correct</a>, in that if it gives a positive result then indeed S does RDF-(RDFS-) entail E. It is not, however, <a>complete</a>: there are cases of S entailing E which are not detectable by this process. Examples include:</p>
<table border="1" >
<tbody>
@@ -1006,9 +988,9 @@
<tr>
- <td><code>ex:a ex:p "string"^^xsd:string .<br/>
+ <td class="othertable"><code>ex:a ex:p "string"^^xsd:string .<br/>
ex:b ex:q "string"^^xsd:string .</code></td>
- <td><code>ex:a ex:p _:b .<br/>
+ <td class="othertable"><code>ex:a ex:p _:b .<br/>
ex:b ex:q _:b .<br/>
_:b rdf:type xsd:string .</code> </td>
</tr>
@@ -1020,16 +1002,16 @@
</tr>
<tr>
- <td><code>ex:a rdfs:subPropertyOf _:b .<br/>
+ <td class="othertable"><code>ex:a rdfs:subPropertyOf _:b .<br/>
_:b rdfs:domain ex:c .<br/>
ex:d ex:a ex:e .</code></td>
- <td><code>ex:d rdf:type ex:c .</code> </td>
+ <td class="othertable"><code>ex:d rdf:type ex:c .</code> </td>
</tr>
</tbody>
</table>
-<p> Both of these can be handled by allowing the rules to apply to a generalization of the RDF syntax, in which literals may occur in subject position and blank nodes may occur in predicate position. </p>
-<p>Define a <dfn>generalized RDF triple</dfn> to be a triple <x, y, z> where x and z can be an IRI, a blank node or a literal, and y can be an IRI or a blank node; and extend this to the rest of RDF, so that a generalized RDF graph is a set of generalized RDF triples, etc.. (This extends the generalization used in [[terHorst1]] and follows exactly the terms used in [[OWL2]].) The semantics described in this document applies to the generalized syntax without change, so that the notions of interpretation, satisfiability and entailment can be used freely. Then we can replace the first RDF entailment pattern with the simpler and more direct</p>
+<p> Both of these can be handled by allowing the rules to apply to a generalization of the RDF syntax in which literals may occur in subject position and blank nodes may occur in predicate position. </p>
+<p>Define a <dfn>generalized RDF triple</dfn> to be a triple <x, y, z> where x and z can be an IRI, a blank node or a literal, and y can be an IRI or a blank node; and extend this to the rest of RDF, so that a generalized RDF graph is a set of generalized RDF triples. (This extends the generalization used in [[terHorst1]] and follows exactly the terms used in [[OWL2-SYNTAX]].) The semantics described in this document applies to the generalized syntax without change, so that the notions of interpretation, satisfiability and entailment can be used freely. Then we can replace the first RDF entailment pattern with the simpler and more direct</p>
<div class="tabletitle">G-RDF-D entailment pattern.</div>
<table border="1" >
@@ -1040,10 +1022,10 @@
<th ><strong>then S RDF-D-entails</strong></th>
</tr>
<tr >
- <td>GrdfD1</td>
- <td> xxx aaa <code>"</code>sss<code>"^^</code>ddd <code>.</code> <br/>
+ <td class="othertable">GrdfD1</td>
+ <td class="othertable"> xxx aaa <code>"</code>sss<code>"^^</code>ddd <code>.</code> <br/>
for ddd in D</td>
- <td><code>"</code>sss<code>"^^</code>ddd <code>rdf:type</code> ddd <code>.</code></td>
+ <td class="othertable"><code>"</code>sss<code>"^^</code>ddd <code>rdf:type</code> ddd <code>.</code></td>
</tr>
</tbody>
@@ -1071,7 +1053,8 @@
3. If no triples were added in step 2., add the RDF (and RDFS) axiomatic triples which contain <code>rdf:_1</code>. <br/>
4. Apply the rules GrdfD1 and rdfD2 (and the rules rdfs1 through rdfs13), with D={<code>rdf:langString</code>, <code>xsd:string</code>), to the set in all possible ways, to exhaustion. </p>
-<p>Then we have a the completeness result:<em>S RDF-entails (RDFS-entails) E just when the generalized RDF (RDFS) closure of S simply entails E.</em> </p>
+<p>Then we have the completeness result:</p>
+<p class="fact">If S is RDF-(RDFS-)consistent, then S RDF-entails (RDFS-entails) E just when the generalized RDF (RDFS) closure of S simply entails E.</em> </p>
<p>Since the closures are finite, the generation process is decideable, and of polynomial complexity. Detecting simple entailment is NP-complete in general, but of low polynomial order when E contains no blank nodes. </p>
@@ -1079,32 +1062,79 @@
<p>If it is important to stay within legal RDF syntax, rule rdfD1 may be used instead of GrdfD1, and the introduced blank node can be used as a substitute for the literal in subsequent derivations. The resulting set of rules will not however be complete.</p>
-<p>As noted earlier, detecting D-entailment for larger sets of datatype IRIs has to pay attention to idiosyncratic properties of the particular datatypes.</p>
+<p>As noted earlier, detecting D-entailment for larger sets of datatype IRIs requires attention to idiosyncratic properties of the particular datatypes.</p>
+</section>
+
+<section class="appendix"><h2 id="proofs">Finite interpretations (Informative)</h2>
+<p>To keep the exposition simple, the RDF semantics has been phrased in a way which requires interpretations structures to be larger than absolutely necessary. For example, all interpretations are required to interpret the whole IRI vocabulary, and the universes of all D-interpretations must contain all possible strings and therefore be infinite. This appendix sketches, without proof, how to re-state the semantics using smaller semantic structures, without changing any RDF entailemnts. </p>
+<p>Basically, it is only necessary for an interpretation structure to interpret the names actually used in the graphs whose entailment is being considered, and to have a universe which contains referents for all the names, plus a random member of each nonempty class or type, in order to provide for the truth of existential assertions made using blank nodes. Formally, we can define a <dfn>pre-interpretation</dfn> over a <a>vocabulary</a> V to be a structure I similar to a <a>simple interpretation</a> but with a mapping only from V to its universe IR, and when considering whether G entails E, consider only pre-interpretations over the finite vocabulary of names actually used in G union E. Clearly, any such pre-interpretation may be extended to simple interpretations all of which which will give the same truthvalues for any triples in G or E. Satisfiability, entailment and so on can then be defined with respect to these finite structures, and shown to be identical to the ideas defined in the earlier sections.</p>
+<p>When considering D-entailment, pre-interpretations may be kept finite by weakening the semantic conditions for datatyped literals so that IR need contain literal values only for literals which actually occur in G or E, or a single value in the value space if there are no such literals in the vocabulary. (This preserves the truth of the triple <code> _:x rdf:type </code>ddd <code>.</code> when ddd is recognized.) For RDF-D entailment, only the finite part of the RDF vocabulary which include those container membership properties which actually occur in the graphs need to be interpreted, and the second RDF semantic condition is weakened to apply only to values which are values of literals which actually occur in the vocabulary. For RDFS interpretations, again only that finite part of the infinite container membership property vocabulary which actually occurs in the graphs under consideration needs to be interpreted. In all these cases, a pre-interpretation of the vocabulary of a set of graphs may be extended to a full interpretation of the appropriate type without changing the truthvalues of any triples in the graphs.</p>
+<p>The whole semantics could be stated in terms of pre-interpretations, yielding the same entailments, and allowing finite RDF graphs to be interpreted in finite structures, if this <em>finite model property</em> is considered important.
+
+</section>
+
+
+<section class="appendix"><h2>Proofs of some results (Informative)</h2>
+
+<p class="fact"> The <a>empty graph</a> is entailed by
+ any graph, and does not entail any graph except itself.
+<!-- <a href="#emptygraphlemmaprf" class="termref">[Proof]</a> -->
+</p>
+
+<p>The empty graph is true in all interpretations, so is entailed by any graph. If G contains a triple <a b c>, then any interpretation I with IEXT(I(b))={ } makes G false; so the empty graph does not entail G. QED.</p>
+
+<p class="fact"> A graph entails all its subgraphs.
+<!-- <a href="#subglemprf" class="termref">[Proof]</a> -->
+</p>
+<p>If I satisfies G then it satisfies every triple in G, hence every triple in any subset of G. QED.</p>
+
+<p class="fact"> A graph
+ is entailed by any of its <a>instance</a>s.
+<!-- <a href="#instlemprf" class="termref"> [Proof]</a> -->
+</p>
+<p>Suppose H is an instance of G with the instantiation mapping M, and that I satisfies H. For blank nodes n in G which are not in H define A(n)=I(M(n)); then I+A satisfies G, so I satisfies G. QED.</p>
+
+<p class="fact">Every graph is satisfiable.</p>
+<p>To show this, we construct a interpretation I from the symbols in the graph itself, called a <dfn>Herbrand interpretation</dfn>. IR contains the names and blank nodes which occur in the graph, with I(n)=n for each name n; n is in IP and <a, b> in IEXT(n) just when the triple <a n b> is in the graph. For IRIs which do not occur in the graph, assign them values in IR at random. Then I+A, where A is the identity map on blank nodes, satisfies the graph, by construction. QED.</p>
+
+<p class="fact">
+ G simply entails a graph E if and only if a subgraph of G is an instance of E.
+</p>
+<p>If a subgraph E' of G is an instance of E then G entails E' which entails E, so G entails E. If G entails E, then the <a>Herbrand interpretation</a> I of G satisfies every triple <s p o> in E; that is, for some mapping A from the blank nodes of E to the vocabulary of G, the triple <[I+A](s) I(p) [I+A](o)> occurs in G. But this is an instance of <s p o> under the instance mapping A; so an instance of E is a subgraph of G. QED.</p>
+
+<p class="fact">if E is lean and E' is a proper instance of E, then E does not entail E'.</p>
+<p>Suppose E entails E', then a subgraph of E is an instance of E', which is a proper instance of E; so a subgraph of E is a proper instance of E, so E is not lean. QED.</p>
+<p class="fact">If E contains an IRI which does not occur in S, then S does not entail E.</p>
+<p>IF S entails E then a subgraph of S is an instance of E, so every IRI in E must occur in that subgraph, so must occur in S. QED.</p>
+<br/>
+
+<p class="fact">For any graph H, if sk(G) entails H there there is a graph H' such that G entails H' and H=sk(H').</p>
+<p>The skolemization mapping sk substitutes a unique new IRI for each blank node, so it is 1:1, so has an inverse. Define ks to be the inverse mapping which replaces each skolem IRI by a unique blank node, different from all other blank nodes. Since sk(G) entails H, a subgraph of sk(G) is an instance of H, say A(H) for some instance mapping A on the blank nodes in H. Then ks(A(H)) is a subgraph of G; and ks(A(H))=A(ks(H)) since the domains of A and ks are disjoint. So ks(H) has an instance which is a subgraph of G, so is entailed by G; and H=sk(ks(H)). QED.</p>
+
+<p class="fact">For any graph H which does not contain any of the "new" IRIs introduced into sk(G), sk(G) simply entails H if and only if G simply entails H.</p>
+<p>Using the terminology in the previous proof: if H does not contain any skolem IRIs, then H=ks(H). So if sk(G) entails H then G entails ks(H)=H; and if G entails H then sk(G) entails G entails H, so sk(G) entails H. QED.</p>
</section>
-
-<section class="appendix" id="MTintro"><h2 id="model_theory">Introduction to model theory (Informative)</h2>
-///
-</section>
-<section class="appendix"><h2 id="proofs">Proofs of Lemmas (Informative)</h2>
-///interpolation lemma is now slightly less trivial to prove. Check for possible consequences of this.///
-</section>
+
+
<section class="appendix" id="whatnot"><h2 id="non_semantics">What the semantics does not do (Informative)</h2>
<p class="issue">Something in here about datasets having no specified semantics, and why. Why using a graph name need not refer to the graph.</p>
-<h3 id="rdf_vocabulary">The RDF vocabulary</h3>
+
<p>The RDF semantic conditions do not place formal constraints on the meaning
of much of the RDF vocabulary which is intended for use in describing containers and bounded collections,
- or the reification vocabulary intended to enable an RDF graph to describe RDF triples. In this appendix we briefly review the intended meanings of this vocabulary. </p>
+ or the reification vocabulary intended to enable an RDF graph to describe RDF triples. This appendix briefly reviews the intended meanings of this vocabulary. </p>
<p>The omission of these conditions from the formal semantics is a design decision
to accommodate 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>
+
+<section>
<h3><a id="Reif">Reification</a></h3>
@@ -1131,10 +1161,10 @@
<p>and suppose that this graph is identified by the IRI <code>ex:graph1</code>. Exactly how this identification is achieved is external to the RDF model, but it might be by the IRI resolving to a concrete syntax document describing the graph, or by the IRI being the associated name of a named graph in a dataset. Assuming that the IRI can be used to refer to the triple, then the reification vocabulary allows us to describe the first graph in another graph:</p>
- <p><code><ex:graph1> rdf:type rdf:Statement .<br/>
- <ex:graph1> rdf:subject <ex:a> .<br/>
- <ex:graph1> rdf:predicate <ex:b> .<br/>
- <ex:graph1> rdf:object <ex:c> .</code></p>
+ <p><code>ex:graph1 rdf:type rdf:Statement .<br/>
+ ex:graph1 rdf:subject ex:a .<br/>
+ ex:graph1 rdf:predicate ex:b .<br/>
+ ex:graph1 rdf:object ex:c .</code></p>
<p>The second graph is called a <i><a href="#glossReify"
class="termref"><em>reification</em></a></i> of the triple in the first
@@ -1170,19 +1200,21 @@
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/>
+ _: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>
+ _: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>
+ <p><code>_:yyy ex:property ex:foo .</code></p>
+</section>
+<section>
<h4 id="containers">RDF containers</h4>
@@ -1211,15 +1243,13 @@
<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,
+ would typically be supplied by a programming language. 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
+ are not formally sanctioned by the RDF formal semantics. 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>
@@ -1245,16 +1275,16 @@
the elements of an <code>rdf:Bag</code> in a different order. For example,</p>
<p><code>_:xxx rdf:type rdf:Bag .<br/>
- _:xxx rdf:_1 <ex:a> .<br/>
- _:xxx rdf:_2 <ex:b> .</code></p>
+ _: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><code>_:xxx rdf:_1 ex:b .<br/>
+ _:xxx rdf:_2 ex:a .</code></p>
<p>Notice that if this conclusion were <a>valid</a>, then the result of
- conjoining it to the original graph would be <a>entailed</a> by the graph, and this would assert that both elements were in both
+ adding it to the original graph would be <a>entailed</a> by the graph, and this would assert that both elements were in both
positions. This is a consequence of the fact that RDF is a purely
assertional language.</p>
@@ -1262,11 +1292,11 @@
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
- it is not a <a>contradiction</a> to assert that something is both an <code>rdf:Bag</code> and an <code>rdf:Seq</code>.
+ it is not <a>inconsistent</a> to assert that something is 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>
+ _:xxx rdf:_1 ex:a .<br/>
+ _:xxx rdf:_3 ex:c .</code></p>
<p>does not entail</p>
@@ -1278,7 +1308,9 @@
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>
+</section>
+<section>
<h4 id="collections">RDF collections</h4>
@@ -1307,7 +1339,7 @@
<code><br/>
<br/>
_:c1 rdf:first aaa .<br/>
- _:c1 rdf:rest _:c2</code></p>
+ _:c1 rdf:rest _:c2 .</code></p>
<p>where the final item is indicated by the use of <code>rdf:nil</code> as the
@@ -1321,15 +1353,15 @@
guarantee that the similar collection with the items permuted also exists:
<code>
<br/><br/>
- _:c1 rdf:first <ex:aaa> .<br/>
+ _:c1 rdf:first ex:aaa .<br/>
_:c1 rdf:rest _:c2 .<br/>
- <span > _:c2 rdf:first</span> <ex:bbb> .<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/>
+<p><code>_:c3 rdf:first ex:bbb .<br/>
_:c3 rdf:rest _:c4 .<br/>
- <span >_:c4 rdf:first</span> <ex:aaa> .<br/>
+ <span >_:c4 rdf:first</span> ex:aaa .<br/>
_:c4 rdf:rest rdf:nil .
</code></p>
@@ -1338,9 +1370,9 @@
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/>
+<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>
@@ -1348,9 +1380,9 @@
by failing to specify its <code>rdf:rest</code> property value.</p>
-<p>Semantic extensions MAY
+<p>Semantic extensions may
place extra syntactic well-formedness restrictions on the use of this vocabulary
- in order to rule out such graphs. They MAY
+ in order to rule out such graphs. They may
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
@@ -1361,7 +1393,8 @@
<p> The RDFS semantic conditions 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>
-
+</section>
+<section>
<h3><a id="rdfValue"></a>rdf:value</h3>
<p>The intended use for <code>rdf:value</code> is <a href="http://www.w3.org/TR/rdf-primer/#rdfvalue">explained
@@ -1376,338 +1409,17 @@
meaning of <code>rdf:value</code> may vary from application to application.
Even when the intended meaning is clear from the context in the original graph document, it may be
lost when graphs are merged or when conclusions are inferred.</p>
+</section>
</section>
-<section class="appendix" id="glossary"><h2>Glossary of Terms (Informative)</h2>
- <p><strong><a
- 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 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 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.</p>
-<p><strong><a
- id="glossComplete"></a>Complete</strong> (adj., of an inference system). (1)
- Able to detect all <a
- href="#glossEntail" class="termref">entailment</a>s between any two expressions.
- (2) Able to draw all <a href="#glossValid"
- class="termref">valid</a> inferences. See <a href="#glossInference"
- class="termref"><em>Inference</em></a>. Also used with a qualifier: able to
- detect entailments or draw all <a href="#glossValid"
- class="termref">valid</a> inferences in a certain limited form or kind (e.g.
- between expressions in a certain normal form, or meeting certain syntactic conditions.)</p>
-<p>(These definitions are not exactly equivalent, since the first requires that
- the system has access to the consequent of the entailment, and may be unable
- to draw 'trivial' inferences such as (p and p) from p. Typically, efficient
- mechanical inference systems may be complete in the first sense but not necessarily
- in the second.) </p>
-
- <p><strong><a
- 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
- id="glossConsistent"></a>Consistent</strong> (adj., of an expression) Having
- a satisfying <a href="#glossInterpretation"
- class="termref">interpretation</a>; not internally contradictory. (Also used
- of an inference system as synonym for <em>Correct</em>.) </p>
-<p><strong><a
- id="glossCorrect"></a>Correct</strong> (adj., of an inference system). Unable
- to draw any invalid inferences, or unable to make false claims of entailment. See <em>Inference</em>.</p>
-<p><strong><a id="glossDecidable"></a>Decidable</strong>
- (adj., of an inference system). Able to determine for any pair of expressions,
- in a finite time with finite resources, whether or not the first entails the
- second. (Also: adj., of a logic:) Having a decidable inference system which
- is complete and correct for the semantics of the logic.</p>
-<p>(Not all logics can have inference systems which are both complete and decidable,
- and decidable inference systems may have arbitrarily high computational complexity.
- The relationships between logical syntax, semantics and complexity of an inference
- system continue to be the subject of considerable research.)</p>
-
- <p><strong><a 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 id="glossEquivalent"></a>Equivalent</strong> (prep., with
- <em>to</em>; also <em>logically</em> equivalent) 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 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
- 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 id="glossIff"></a>Iff</strong>
- (conj.) Conventional abbreviation for 'if and only if'. Used to
- express necessary and sufficient conditions.</p>
-<p><a
- id="glossInconsistent"></a><strong>Inconsistent</strong> (adj.) False under
- all interpretations; impossible to <a
- href="#glossSatisfy" class="termref">satisfy</a>. <strong>Inconsistency</strong>
- (n.), any inconsistent expression or graph.</p>
-<p>(<a
- href="#glossEntail" class="termref">Entailment</a> and inconsistency are closely
- related, since A entails B just when (A and not-B) is inconsistent, c.f. the
- second definition for <a
- href="#glossEntail" class="termref">entailment</a>. This is the basis of many
- mechanical inference systems. </p>
-<p>Although the definitions of <a href="#glossConsistent" class="termref">consistency</a>
- and inconsistency are exact duals, they are computationally dissimilar. It is
- often harder to detect consistency in all cases than to detect inconsistency
- in all cases<a
- href="#glossEntail" class="termref"></a>.)</p>
-<p><strong><a
- id="glossIndexical"></a>Indexical</strong> (adj., of an expression) having
- a meaning which implicitly refers to the context of use. Examples from English
- include words like 'here', 'now', 'this'.</p>
-<p><strong><a
- 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
- 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
- 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 an <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 id="glossLogic"></a>Logic</strong>
- (n.) A formal language which expresses <a href="#glossProposition"
- class="termref">propositions</a>.</p>
- <p><a
- id="glossMetaphysical"></a><strong>Metaphysical</strong> (adj.).
- Concerned with the true nature of things in some absolute or
- fundamental sense.</p>
-
- <p><a
- 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
- 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
- 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
- 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
- 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 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
- 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
- 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
- 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 id="glossSkolemization"></a>
-<!-- <a href="#skolemlemprf"> -->
-<strong>Skolemization</strong> (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 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
- 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 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 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><dfn>Well-formed</dfn> (adj., of an
- expression). Syntactically legal.</p>
-
- <p><strong><a 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>
-
-
-</section>
<section class='appendix'>
<h2 id="acknolwedgements">Acknowledgements</h2>
<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>///Herman ter Horst for rule style, Li Ding for complete graphs, Antoine for no-vocabulary and general input. Others?///</p>
+<p>// Herman ter Horst for rule style, Li Ding for complete graphs, Antoine for no-vocabulary and general input. Others?///</p>
<p>
Many thanks to Robin Berjon for making our lives so much easier with his cool tool. You betcha.
</p>