RDF语义 推荐标准-8
TransWiki - W3CHINA.ORG开放翻译计划（OTP）
摘要_文档状态_目录 第0节 第1节 第2节 第3节 第4节 第5节 第6节 第7节 附录_参考文献
| 目录 |
Appendix A: Proofs of Lemmas (Informative)
"One of the merits of a proof is that it instills a certain doubt as to the result proved." -Bertrand Russell
Empty Graph Lemma. The empty set of triples is entailed by any graph, and does not entail any graph except itself.
Proof. 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. QED.
This means that most of the subsequent results are trivial for empty graphs, which is what one would expect.
Subgraph Lemma. A graph entails all its subgraphs.
Proof. Obvious, from definitions of subgraph (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#defsubg) and entailment (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#defentail). 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. QED
Merging lemma. The merge (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#defmerge) of a set S of RDF graphs is entailed by S, and entails every member of S.
Proof. Obvious, from definitions of entailment (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#defentail) and merge. All members of S are true if and only if all triples in the merge of S are true. QED.
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.
Instance Lemma. A graph is entailed by all its instances.
Proof. Suppose I satisfies (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#defsatis) E' and E' is an instance (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#definst) 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 name (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#defname) 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' entails (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#defentail) E. QED.
Skolemization is a syntactic transformation routinely used in automatic inference systems in which existential variables are replaced by 'new' functions - function names not used elsewhere - applied to any enclosing universal variables. In RDF, Skolemization amounts to replacing every blank node in a graph by a 'new' name, i.e. a URI reference which is guaranteed to not occur anywhere else. In effect, it gives 'arbitrary' names to the anonymous entities whose existence was asserted by the use of blank nodes: the arbitrariness of the names ensures that nothing can be inferred that would not follow from the bare assertion of existence represented by the blank node. (Using a literal would not do. Literals are never 'new' in the required sense.)
To be precise, a Skolemization of E (with respect to V) is a ground instance of E with respect to V with a 1:1 instance mapping that maps each blank node in G to a URI reference that does not appear in G (so the Skolem vocabulary V must be disjoint from the vocabulary of E)
While not itself strictly a valid (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossValid) operation, Skolemization adds no new content to an expression, in the sense that a Skolemized expression has the same entailments as the original expression provided they do not contain names from the Skolem vocabulary:
Skolemization Lemma. 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 .
Proof. sk(E) entails E by the instance lemma.
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.
QED.
Intuitively, this lemma shows that asserting a Skolemization expresses a similar content to asserting the original graph, in many respects. However, a graph should not be thought of as being equivalent to its Skolemization, since these 'arbitrary' names would have the same status as any other URI references once published. Also, Skolemization would not be an appropriate operation when applied to anything other than the antecendent of an entailment. A Skolemization of a query would represent a completely different query. Nevertheless, for many purposes when proving results about entailment, we need only consider ground graphs: for provided E does not contain any Skolem vocabulary, S entails E iff S' entails E.
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 Herbrand (http://www-groups.dcs.st-andrews.ac.uk/%7Ehistory/Mathematicians/Herbrand.html)'s idea; we here modify it slightly to handle literals appropriately.) Given a nonempty graph G, the (simple) Herbrand interpretation of G, written Herb(G), is the interpretation defined as follows.
LVHerb(G) = the set of all plain literals in G; |
Clearly Herb(G)+B, where B is the identity map on blank nodes in G, satisfies every triple in G, by construction, so Herb(G) satisfies G.
Herbrand interpretation (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#defherbinterp)s treat URI references and typed literals (and blank nodes) in the same way as plain literals, i.e. as denoting their own syntactic forms. Of course this may not be what was intended by the writer of the RDF, but the construction shows that any graph can be interpreted in this way. This therefore establishes that any RDF graph has a satisfying (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossSatisfy) simple interpretation, i.e. there cannot be a simple inconsistency in RDF.
Notice that the universe of the Herbrand interpretation of G contains the blank nodes of G; they are 'standing for' the entities that they assert the existence of, in effect. Since blank nodes must be interpreted to denote themselves in order to satisfy the graph, the Herbrand interpretation of a Skolemization of a graph is isomorphic with the Herbrand interpretation of the graph together with the blank node mapping: Herb(sk(G)) = Herb(G)+B (using a familiar abuse of notation where a blank node in a Herbrand interpretation is treated as a Skolem name.)
Interpolation Lemma. S entails E if and only if a subgraph of S is an instance of E.
Proof. 'if' follows from the subgraph and instance lemmas.
'only if' uses the Herbrand construction. Suppose S simply entails E. Herb( (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#defHerb)S) satisfies S, so Herb( (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#defHerb)S) satisfies E, i.e. for some mapping A from the blank nodes of E to IRHerb(S), [Herb (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#defHerb)(S)+A] satisfies every triple
s p o .
in E, so S must contain the triple
[Herb( (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#defHerb)E)+A](s) p [Herb( (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#defHerb)E)+A](o) .
which is the instance of the previous triple under the instance mapping A. So the set of all such triples is a subgraph of S which is an instance of E.
QED
The following are direct consequences of the interpolation lemma:
Anonymity lemma. Suppose E is a lean (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#deflean) graph and E' is a proper instance of E. Then E does not entail E'.
Proof. Suppose E entails E', then a subgraph of E is an instance of E' and therefore a proper instance of E; so E is not lean (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#deflean) , contrary to hypothesis. So E does not entail E'.
QED
Compactness Lemma. If S entails E and E is a finite graph, then some finite subset S' of S entails E.
Proof. By the interpolation lemma, a subgraph S' of S is an instance of E; so S' is finite, and S' entails E.
QED
Although compactness is trivial for simple entailment, it becomes progressively less trivial in more elaborate semantic extensions.
Monotonicity Lemma. Suppose S is a subgraph of S' and S entails E. Then S' entails E. (Special case of general monotonicity lemma (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#GeneralMonotonicityLemmaprf)) QED
General monotonicity lemma. 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.
Proof. 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.
QED
Both of the following proofs follow a common pattern which generalizes that used in the proof of the interpolation lemma, by using a modification of the Herbrand construction applied to a 'closure' obtained by applying rules to exhaustion. The proofs operate by showing that the resulting interpretation is both appropriate to the vocabulary and also acts similarly to the Herbrand interpretation (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#defHerb). Much of the complexity of the proofs arises from the need to adapt the Herbrand construction in order to take proper account of literal values. Herbrand interpretations ignore literal typing and treat all typed literals as non-literal values; this is irrelevant when considering simple entailment, which treats typed literals simply as denoting names; but more care will be needed when considering rdf- and rdfs-interpretations.
Both proofs use a single basic idea which requires rather an awkward notation but is basically straightforward to understand. The simple Herbrand interpretation treats all vocabulary items as denoting themselves, and builds the interpretation out of these syntactic items. The semantic conditions on rdf- and rdfs-interpretations do not permit this in all cases: XML literals in particular are required to denote other kinds of entity. We therefore distinguish between the 'real' semantic values and their syntactic 'surrogates' in these cases, by defining a mapping sur from the universe of the intepretation to the vocabulary of the graph (plus blank nodes) which is as close as possible to being an identity mapping, but which when applied to these special literal values, identifies the particular blank node which acts as a witness for that value in the graph. In the case of RDFS, the surrogate mapping is extended to all literal values, since the blank node allocated to the literal can occur in a subject position, and hence record information about the literal value which must be applied back to that value in the interpretation.
''''RDF entailment lemma. S rdf-entails (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rdf_entail) E if and only if there is a graph which can be derived from S plus the RDF axiomatic triples (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#RDF_axiomatic_triples) by the application of rule lg (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#ruleslg) and the RDF entailment rules (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#RDFRules) and which simply entails E.
Proof. To show 'if' one has only to check that the rules are rdf-valid, which is left as an exercise for the reader; and if S or E is empty then the result follows trivially; so suppose they are both non-empty.
To establish 'only if', the proof proceeds by constructing an rdf Herbrand interpretation RH of S which serves the same role for rdf-interpretations that the simple Herbrand interpretation does for simple interpretations. The construction follows the Herbrand construction as far as possible, but interprets well-formed XML literals so as to satisfy the RDF semantic conditions, guided by the triples in the RDF closure, C, defined to be the graph resulting from the following process:
add to S all the RDF axiomatic triples (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#RDF_axiomatic_triples);
apply [http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#simpleRules ]rule lg (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#ruleslg) to any triple containing a well-typed XML literal until the graph is unchanged by the rule;
apply rule rdf2 (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rulerdf2) until the graph is unchanged;
apply rule rdf1 (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rulerdf1) until the graph is unchanged.
Note that C contains precisely one new blank node _:nnn allocated (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#defallocated) to each literal in S by the rule rule lg (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#ruleslg), and that the subgraph of triples in S containing any well-typed XML literal is reproduced exactly in C with this blank node replacing the literal and with the extra triple
_:nnn rdf:type rdf:XMLLiteral .
introduced by rule rdf2 (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rulerdf2). Note also that the proof only requires that rule lg (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#ruleslg) is used on well-typed XML literals, so that it actually establishes a slightly tighter result.
Blank nodes introduced by rule lg (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#ruleslg) stand as surrogates for well-formed XML literals in the subject position of a triple. (In the proof of the next lemma, this will be extend to all literals.) In order to construct an RDF interpretation, XML literals and their surrogates must be replaced by the appropriate literal values in the domain of the interpretation, but the proof requires that each XML literal value be uniquely associated with a lexical item that denotes it. This requires some delicacy in the following construction.
If lll is a well-formed XML literal, let xml(lll) be the XML value of lll; and for each XML value x of any well-formed XML literal in C, let sur(x) be the blank node allocated to that XML literal by rule lg (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#ruleslg); and extend sur to be the identity mapping on URI references, blank nodes and all other literals in C.
RH is then defined by:
LVRH = all plain literals in C plus {xml(x): x a well-typed XML literal in S} |
Define a mapping B on blank nodes in C as follows: B(x)=xml(lll) if x is allocated to a well-formed XML literal lll, otherwise B(x)=x, then clearly [RH+B] satisfies C and therefore S, so RH satisfies S.
Since C contains all the required RDF axiomatic triples, RH satisfies them.
It is easy to see that J satisfies the first two RDF semantic conditions, by construction; for the triples introduced by rule rdf2 (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rulerdf2) require that IEXTRH(rdf:type) contains <xml(lll),rdf:XMLLiteral> for every well-typed XML literal lll.
The third RDF semantic condition (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rdfsemcond3) is the only negative semantic condition which cannot be satisfied simply by construction, but it is satisfied trivially. Ill-typed XML literals denote themselves in RH, and so are excluded from LVRH by construction. The pair <lll, rdf:XMLLiteral> cannot occur in IEXTRH(rdf:type) because a literal cannot occur in subject position; so the condition is satisfied, so RH is an rdf-interpretation.
Since S rdf-entails E, RH satisfies E: so for some mapping A from the blank nodes of E to IRRH, [RH+A] satisfies every triple
s p o .
in E, i.e. IEXTRH(p) contains <[RH+A](s),[RH+A](o)>, i.e.C contains a triple
sur([RH+A](s)) p sur([RH+A](o)).
but this is an instance of the first triple under the instantiation mapping x -> sur(A(x)); so a subgraph of C is an instance of E; so C simply entails E.
QED
This lemma also shows that any graph has a satisfying rdf-interpretation, and the proof illustrates how to construct it from a Herbrand interpretation of the closure, by interpreting well-formed XML literals appropriately and allowing the possible existence of properties which have no extensions. Note that if E is finite then the derived subgraph of C is also finite.
The proof of the RDFS entailment lemma is similar in structure and uses closely similar definitions, but is of course longer and requires a more elaborate construction to ensure that the class extensions of rdfs:Literal and rdfs:Resource contain all literal values.
RDFS entailment lemma. S rdfs-entails (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rdfs_entailment) E if and only if there is a graph which can be derived from S plus the RDF (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#RDF_axiomatic_triples) and RDFS axiomatic triples (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#RDFS_axiomatic_triples) by the application of rule lg (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#ruleslg), rule gl (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rulesgl) and the RDF (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#RDFRules) and RDFS entailment rules (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#RDFSRules) and which either simply entails E or is an XML clash.
Proof. Again, to show 'if' it is sufficient to show that the RDFS entailment rules (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#RDFSRules) are rdfs-valid, which is again left as an exercise; and again, the empty cases are trivial.
The proof of 'only if' is similar to that used in the previous lemma, and similar constructions and terminology will be used, except that the RDFS closure, D, is defined to be the graph resulting from the following process:
add to S all the RDF (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#RDF_axiomatic_triples) and RDFS axiomatic triples (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#RDFS_axiomatic_triples);
apply [http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#simpleRules ]rule lg (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#ruleslg) to any triple containing a literal until the graph is unchanged by the rule;
apply rules rdf2 (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rulerdf2) and rdfs1 (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rulerdfs1) until the graph is unchanged;
apply rule rdf1 (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rulerdf1), rule gl (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rulesgl) and the remaining RDFS entailment rules (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#RDFSRules) until the graph is unchanged.
Unlike the previous lemma, this proof requires that rule lg (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#ruleslg) is applied to all literals, even ill-typed XML literals, and it requires the inverse rule gl (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rulesgl). Rule gl (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rulesgl) needs to be used only after an application of rules rdfs6 (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rulerdfs6) or rdfs10 (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rulerdfs10), since those are the only rules which can move a blank node from subject to object position. Note that D contains precisely one new blank node _:nnn allocated (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#defallocated) to each literal in S by the rule rule lg (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#ruleslg), and that the subgraph of triples in S containing any literal is reproduced exactly in D with this blank node replacing the literal and with the extra triple
_:nnn rdf:type rdfs:Literal .
introduced by rule rdfs1 (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rulerdfs1), and possibly also
_:nnn rdf:type rdf:XMLLiteral .
introduced by rule rdf2 (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rulerdf2) when appropriate. This means that after this point in the construction, literals can effectively be ignored, since any of the subsequent rules which applies to triples containing a literal will also apply equally well to the similar triples where the literal is replaced by its allocated blank node. The rest of the proof uses this by requiring literal values in the interpretation to satisfy just the semantic conditions imposed on the blank nodes allocated to the corresponding literal, and ignoring triples in the graph which contain literals. The use of rule gl (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rulesgl) ensures that D contains any triple containing a literal if and only if it contains the similar triple with the literal replaced by its allocated blank node.
As in the previous proof, if lll is a well-formed XML literal, let xml(lll) be the XML value of lll; the surrogate mapping sur is then extended as follows. First, the domain of sur is the set containing just the URI references, literals and blank nodes occurring in D and all XML values of well-formed XML literals in D. (This is the universe of the rdfs-Herbrand interpretation, defined below.) Now, if lll is a well-formed XML literal in D, let sur(xml(lll)) be the blank node allocated to lll by rule lg (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#ruleslg); for any other literal lll in D, let sur(lll) be the blank node allocated to lll by rule lg (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#ruleslg), and for all URI references and blank nodes in D, let sur(x) = x . Note that the range of sur contains only URI references and blank nodes which occur in D.
The rdfs-Herbrand interpretation SH of S is then constructed similarly to the previous lemma.
LVSH = {x: D contains the triple: sur(x) rdf:type rdfs:Literal .} |
Define B(x) as follows: if x is a blank node allocated to a well-formed XML literal lll in D then B(x) = xml(lll); if it is allocated to any other literal lll in D then B(x)=lll; and otherwise B(x)=x; then clearly [SH+B] satisfies D and therefore S, so SH satisfies S.
As in the previous lemma, SH satisfies all the required RDF and RDFS axiomatic triples and the first two RDF semantic conditions by construction.
SH satisfies the third RDF semantic condition just in case D does not contain an XML clash. Note that the presence of surrogates for ill-typed XML literals invalidates the argument used in the previous lemma to the effect that this condition is trivally satisfied. So assume that D does not contain an XML clash.
As noted in the text, we can regard the first RDFS semantic condition as defining ICEXT and IC: we will do so without further comment and describe all the conditions in terms of IEXT. To show that SH satisfies the remaining RDFS semantic conditions we argue case by case, using the minimality of the Herbrand interpretation and the completeness of the closure.
All of these conditions can be mirrored by a corresponding sequence of rule applications. The general form of the argument can be illustrated with the case of the second RDFS semantic condition (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rdfssemcond2). Suppose <x,y> is in IEXTSH(rdfs:domain) and <u,v> is in IEXTSH(x); then D must contain the triples
sur(x) rdfs:domain sur(y) .
sur(u) x sur(v).
so x must be a URIref, so sur(x)=x; and then by rule rdfs2 (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#rulerdfs2), it must also contain the triple
sur(u) rdf:type sur(y).
so IEXTSH(rdf:type) contains <u,v> ; so the condition is satisfied.
The other cases proceed similarly, by translating the semantic condition into a derivation using the rules and axiomatic triples. The argument forms are summarized in the following table. Some of the semantic conditions split into several subconditions, and some also have special subcases.
RDFS semantic condition | Derivation | |
if x in IR then | URIref or bnode in subject: |
|
Literal: |
| |
URIref or bnode in object: |
| |
URIref in predicate: |
| |
x in LV iff | well-typed XML literal lll: |
|
other literal lll : |
| |
if | x rdfs:domain y . |
|
if | x rdfs:range y . |
|
if | x rdf:type rdf:Property |
|
if | x rdfs:subPropertyOf y |
|
if | x rdfs:subPropertyOf y |
|
if | x rdf:type rdfs:Class |
|
if | x rdfs:subClassOf y |
|
if | x rdf:type rdfs:Class |
|
if | x rdfs:subClassOf y |
|
if | x rdf:type rdfs:ContainerMembershipProperty |
|
if | x rdf:type rdfs:Datatype |
|
so SH is an rdfs-interpretation.
Since S rdfs-entails E, SH satisfies E: so for some mapping A from the blank nodes of E to IRSH, [SH+A] satisfies every triple
s p o .
in E, i.e. IEXTSH(p) contains <[SH+A](s),[SH+A](o)>, i.e.D contains a triple
sur([SH+A](s)) p sur([SH+A](o)).
which is an instance of the first triple under the instantiation mapping x -> sur(A(x)), unless o is a literal. If o is a literal, then sur([SH+A](o) is the blank node allocated to o, and so D also contains the triple
sur([SH+A](s)) p o .
which is an instance of the first triple under the instantiation mapping x -> sur(A(x)). So a subgraph of D is an instance of E under the instantiation mapping x -> sur(A(x)); so D simply entails E.
So either D contains an XML clash or D simply entails E, so D satisfies the conditions of the lemma.
QED
Note that if E is finite, or if D contains an XML clash, then a finite subgraph of D also satisfies the conditions of the lemma.
Appendix B: Glossary of Terms (Informative)
Antecedent (n.) In an inference (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossInference), the expression(s) from which the conclusion (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossConsequent) is derived. In an entailment (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossEntail) relation, the entailer. Also assumption.
Assertion (n.) (i) Any expression which is claimed to be true. (ii) The act of claiming something to be true.
Class (n.) A general concept, category or classification. Something[http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossResource ] used primarily to classify or categorize other things. Formally, in RDF, a resource (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossResource) of type rdfs:Class with an associated set of resources (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossResource) all of which have the class as a value of the rdf:type property. Classes are often called 'predicates' in the formal logical literature.
(RDF distinguishes class from set, although the two are often identified. Distinguishing classes from sets allows RDF more freedom in constructing class hierarchies, as explained earlier (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#technote).)
Complete (adj., of an inference system). (1) Able to detect all entailment (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossEntail)s between any two expressions. (2) Able to draw all valid (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossValid) inferences. See Inference. Also used with a qualifier: able to detect entailments or draw all valid (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossValid) inferences in a certain limited form or kind (e.g. between expressions in a certain normal form, or meeting certain syntactic conditions.)
(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.)
Consequent (n.) In an inference, the expression constructed from the antecedent (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossAntecedent). In an entailment relation, the entailee. Also conclusion.
Consistent (adj., of an expression) Having a satisfying interpretation (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossInterpretation); not internally contradictory. (Also used of an inference system as synonym for Correct.)
Correct (adj., of an inference system). Unable to draw any invalid inferences, or unable to make false claims of entailment. See Inference.
Decideable (adj., of an inference system). Able to determine for any pair of expressions, in a finite time with finite resources, whether or not the first entails the second. (Also: adj., of a logic:) Having a decideable inference system which is complete and correct for the semantics of the logic.
(Not all logics can have inference systems which are both complete and decideable, and decideable inference systems may have arbitrarily high computational complexity. The relationships between logical syntax, semantics and complexity of an inference system continue to be the subject of considerable research.)
Entail (v.), entailment (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 interpretation (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossInterpretation) which satisfies (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossSatisfy) the first also satisfies the second. (Also used between a set of expressions and an expression.)
Equivalent (prep., with to) True under exactly the same conditions; making identical claims about the world, when asserted. Entails (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossEntail) and is entailed by.
Extensional (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 Intensional.
Formal (adj.) Couched in language sufficiently precise as to enable results to be established using conventional mathematical techniques.
Iff (conj.) Conventional abbreviation for 'if and only if'. Used to express necessary and sufficient conditions.
Inconsistent (adj.) False under all interpretations; impossible to satisfy (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossSatisfy). Inconsistency (n.), any inconsistent expression or graph.
(Entailment (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossEntail) and inconsistency are closely related, since A entails B just when (A and not-B) is inconsistent, c.f. the second definition for entailment (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossEntail). This is the basis of many mechanical inference systems.
Although the definitions of consistency (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossConsistent) 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[http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossEntail ].)
Indexical (adj., of an expression) having a meaning which implicitly refers to the context of use. Examples from English include words like 'here', 'now', 'this'.
'Infer'ence (n.) An act or process of constructing new expressions from existing expressions, or the result of such an act or process. Inferences corresponding to entailments (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossEntail) are described as correct or valid. Inference rule, formal description of a type of inference; inference system, organized system of inference rules; also, software which generates inferences or checks inferences for validity.
Intensional (adj., of a logic) Not extensional (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossExtensional). A logic which allows distinct entities with the same extension.
(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.)
Interpretation (of) (n.) A minimal formal description of those aspects of a world (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossWorld) which is just sufficient to establish the truth or falsity of any expression of a logic.
(Some logic texts distinguish between a interpretation structure, which is a 'possible world' considered as something independent of any particular vocabulary, and an interpretation mapping from a vocabulary into the structure. The RDF semantics takes the simpler route of merging these into a single concept.)
Logic (n.) A formal language which expresses propositions (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossProposition).
Metaphysical (adj.). Concerned with the true nature of things in some absolute or fundamental sense.
Model Theory (n.) A formal semantic theory which relates expressions to interpretations.
(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.)
Monotonic (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 valid (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossValid) entailment.
(All logics based on a conventional model theory (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossModeltheory) and a standard notion of entailment are monotonic. Monotonic logics have the property that entailments remain valid (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossValid) outside of the context in which they were generated. This is why RDF is designed to be monotonic.)
Nonmonotonic (adj.,of a logic or inference system) Not monotonic (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossMonotonic). Non-monotonic formalisms have been proposed and used in AI and various applications. Examples of nonmonotonic inferences include default reasoning, where one assumes a 'normal' general truth unless it is contradicted by more particular information (birds normally fly, but penguins don't fly); negation-by-failure, commonly assumed in logic programming systems, where one concludes, from a failure to prove a proposition, that the proposition is false; and implicit closed-world assumptions, 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.)
(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 valid (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossValid) 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.)
Ontological (adj.) (Philosophy) Concerned with what kinds of things really exist. (Applied) Concerned with the details of a formal description of some topic or domain.
Proposition (n.) Something that has a truth-value; a statement or expression that is true or false.
(Philosophical analyses of language traditionally distinguish propositions from the expressions which are used to state them, but model theory does not require this distinction.)
Reify (v.), reification (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.
Resource (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.
Satisfy (v.t.), satisfaction,(n.) satisfying (adj., of an interpretation). To make true. The basic semantic relationship between an interpretation and an expression. X satisfies Y means that if the world (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossWorld) conforms to the conditions described by X, then Y must be true.
Semantic (adj.) , semantics (n.). Concerned with the specification of meanings. Often contrasted with syntactic to emphasize the distinction between expressions and what they denote.
Skolemization (n.) A syntactic transformation in which blank nodes are replaced by 'new' names.
(Although not strictly valid (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossValid), 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. T. Skolem (http://www-gap.dcs.st-and.ac.uk/~history/Mathematicians/Skolem.html))
Token (n.) A particular physical inscription of a symbol or expression in a document. Usually contrasted with type, the abstract grammatical form of an expression.
Universe (n., also Universe of discourse) 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.
Use (v.) contrasted with mention; to use a piece of syntax to denote or refer to something else. The normal way that language is used.
("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." - Alfred Tarski (http://www.philosophypages.com/dy/t.htm))
Valid (adj., of an inference or inference process) Corresponding to an entailment (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossEntail), i.e. the conclusion of the inference is entailed by the antecedent of the inference. Also correct.
Well-formed (adj., of an expression). Syntactically legal.
World (n.) (with the:) (i) The actual world. (with a:) (ii) A way that the actual world might be arranged. (iii) An interpretation (http://www.w3.org/TR/2004/REC-rdf-mt-20040210/#glossInterpretation) (iv) A possible world.
(The metaphysical status of 'possible worlds (http://plato.stanford.edu/entries/actualism/possible-worlds.html)' 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.)
Appendix C: Acknowledgements
This document reflects the joint effort of the members of the RDF Core Working Group (http://www.w3.org/2001/sw/RDFCore/). 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.
The basic idea of using an explicit extension mapping to allow self-application without violating the axiom of foundation was suggested by Christopher Menzel.
Peter Patel-Schneider and Herman ter Horst found several major problems in earlier drafts, and suggested several important technical improvements.
Patrick Hayes' work on this document was supported in part by DARPA under contract #2507-225-22.
References
Normative
[RDF-CONCEPTS]
Resource Description Framework (RDF): Concepts and Abstract Syntax (http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/), Graham Klyne and Jeremy J. Carroll, Editors, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/ . Latest version (http://www.w3.org/TR/rdf-concepts/) available at http://www.w3.org/TR/rdf-concepts/ .
[RDF-SYNTAX]
RDF/XML Syntax Specification (Revised) (http://www.w3.org/TR/2004/REC-rdf-syntax-grammar-20040210/), Dave Beckett, Editor, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-syntax-grammar-20040210/ . Latest version (http://www.w3.org/TR/rdf-syntax-grammar/) available at http://www.w3.org/TR/rdf-syntax-grammar/ .
[RDF-TESTS]
RDF Test Cases (http://www.w3.org/TR/2004/REC-rdf-testcases-20040210/), Jan Grant and Dave Beckett, Editors, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-testcases-20040210/ . Latest version (http://www.w3.org/TR/rdf-testcases/) available at http://www.w3.org/TR/rdf-testcases/ .
[RDFMS]
Resource Description Framework (RDF) Model and Syntax Specification (http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/) , 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 latest version of RDF M&S (http://www.w3.org/TR/REC-rdf-syntax/) is available at http://www.w3.org/TR/REC-rdf-syntax/.
[RFC 2119]
RFC 2119 - Key words for use in RFCs to Indicate Requirement Levels (http://www.ietf.org/rfc/rfc2119.txt) , S. Bradner, IETF. March 1997. This document is http://www.ietf.org/rfc/rfc2119.txt.
[RFC 2396]
RFC 2396 - Uniform Resource Identifiers (URI): Generic Syntax (http://www.isi.edu/in-notes/rfc2396.txt) Berners-Lee,T., Fielding and Masinter, L., August 1998
[XSD]
XML Schema Part 2: Datatypes (http://www.w3.org/TR/xmlschema-2/), Biron, P. V., Malhotra, A. (Editors) World Wide Web Consortium Recommendation, 2 May 2001
Non-Normative
[OWL]
OWL Web Ontology Language Reference (http://www.w3.org/TR/2004/REC-owl-ref-20040210/), Mike Dean and Guus Schreiber, Editors, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-owl-ref-20040210/ . Latest version (http://www.w3.org/TR/owl-ref/) available at http://www.w3.org/TR/owl-ref/ .
[Conen&Klapsing]
A Logical Interpretation of RDF (http://nestroy.wi-inf.uni-essen.de/rdf/logical_interpretation/index.html), Conen, W., Klapsing, R..Circulated to RDF Interest Group (http://lists.w3.org/Archives/Public/www-rdf-interest/2000Aug/0122.html), August 2000.
[DAML]
Frank van Harmelen, Peter F. Patel-Schneider, Ian Horrocks (editors), Reference Description of the DAML+OIL (March 2001) ontology markup language
[Hayes&Menzel]
A Semantics for the Knowledge Interchange Format (http://reliant.teknowledge.com/IJCAI01/HayesMenzel-SKIF-IJCAI2001.pdf), Hayes, P., Menzel, C., Proceedings of 2001 Workshop on the IEEE Standard Upper Ontology (http://reliant.teknowledge.com/IJCAI01/), August 2001.
[KIF]
Michael R. Genesereth et. al., Knowledge Interchange Format, 1998 (draft American National Standard).
[Marchiori&Saarela]
Query + Metadata + Logic = Metalog (http://www.w3.org/TandS/QL/QL98/pp/metalog.html), Marchiori, M., Saarela, J. 1998.
[LBASE]
Lbase: Semantics for Languages of the Semantic Web (http://www.w3.org/TR/2003/NOTE-lbase-20031010/), Guha, R. V., Hayes, P., W3C Note, 10 October 2003.
[McGuinness&al]
DAML+OIL:An Ontology Language for the Semantic Web (http://www.ksl.stanford.edu/people/dlm/papers/daml-oil-ieee-abstract.html), McGuinness, D. L., Fikes, R., Hendler J. and Stein, L.A., IEEE Intelligent Systems, Vol. 17, No. 5, September/October 2002.
[RDF-PRIMER]
RDF Primer (http://www.w3.org/TR/2004/REC-rdf-primer-20040210/), Frank Manola and Eric Miller, Editors, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-primer-20040210/ . Latest version (http://www.w3.org/TR/rdf-primer/) available at http://www.w3.org/TR/rdf-primer/ .
[RDF-VOCABULARY]
RDF Vocabulary Description Language 1.0: RDF Schema (http://www.w3.org/TR/2004/REC-rdf-schema-20040210/), Dan Brickley and R. V. Guha, Editors, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-schema-20040210/ . Latest version (http://www.w3.org/TR/rdf-schema/) available at http://www.w3.org/TR/rdf-schema/ .
Appendix D: Change Log. (Informative)
Changes since the 15 December 2003 Proposed Recommendation (http://www.w3.org/TR/2003/PR-rdf-mt-20031215/).
An error in the wording of the RDFS entailment lemma in appendix A was corrected. Some typos in the glossary and main text were corrected.
After considering comments by ter Horst (http://lists.w3.org/Archives/Public/www-rdf-comments/2003OctDec/0233.html), the definition of D-interpretation has been modified so as to apply to an extended vocabulary including the datatype names.
Older entries in the change log were removed. They can be found in the previous version. (http://www.w3.org/TR/2003/PR-rdf-mt-20031215/#change)
(http://www.w3.org/TR/2004/REC-rdf-mt-20040210/metadata.rdf)
(http://validator.w3.org/check/referer)
(http://jigsaw.w3.org/css-validator/)
