This section shows that the definition of a graph as triples
is sufficient to ensure that the graph also falls under the definition of
a graph via the abstract syntax and the mapping rules.
We start by defining terms, and then move into the proof.
 acceptable
 An RDF graph is accceptable if it meets the constraints specified for
a graph as triples
 mappable
 An RDF graph is mappable if there is an abstract syntax
tree in the abstract ontology that maps to it.
 correspondences between abstract syntax trees and node categorizations

A correspondence is a 3tuple
< g, t, C >
where g is
a graph which is both acceptable and mappable,
t is an abstract syntax tree that maps to g,
and C is a
categorization
of the nodes of g
which shows that it is acceptable.
Moreover, in a correspondence,
every uriref has the same categorization
in the abstract syntax as in C.
 corresponds
 An acceptable graph g, with categorization C corresponds to an
abstract syntax tree
t
if there is a correspondence
< g, t, C >
.
Under such a correspondence a subtree u of t corresponds to
a node n in g if the mapping of t involves
mapping u and returning n.
The goal of this section is to show that a graph is
acceptable iff it is mappable.
However, due to time pressure, I omit showing that
mappable graphs are acceptable: this is the easier
direction since the triple tables have been generated
from the mapping rules.
Hence, we aim to show the following:

Sufficiency Theorem

Every acceptable graph is mappable.
In fact the following stronger result is proved:

Correspondence Theorem

Every acceptable graph corresponds to
an abstract syntax tree.
The structure of the proof is inductive.
The initial case from which the induction starts is
the empty graph.

Empty Graph Lemma

The empty graph corresponds to
Ontology()
.
The inductive step involves a number of distinct cases.
To structure the proof we introduce the concept of reducible.
 reducibility

An acceptable graph g is reducible, if there is a
related
graph h with fewer triples, which is also acceptable,
such that if h corresponds to t
then g corresponds to some defined transformation
of t.
Usually h is a proper subgraph of g.
The rest of this section gives:
 Reduction lemmas,
each
showing that an acceptable graph with a certain characteristic
is reducible.
 Structural lemmas, which combine the reduction lemmas
paying special attention to the structure of the blank nodes.

The proof of the main theorem, which simply combines the structural
lemmas with the reduction lemmas into an inductive argument.
Before we start on the reduction lemmas, we present three results
that are frequently needed.

Description Lemma

If a graph g corresponds to t
and contains
a description, an unnamedDataRange or a restriction node n
that is not the object of any
triple then n corresponds to
a directive in t
 Proof:

n is blank and
hence must arise from one of the mapping rules
that introduces a blank node. Moreover, by considering
the
rdf:type
triples with n as subject,
the only mapping rules to consider are those
for the description dataRange or restriction construct from the abstract
syntax.
These mapping rules can only be invoked in certain contexts
[ ... enumerate contexts, automatic needed? ... ];
in all of these the returned node becomes the object of a triple,
except for the context transforming a directive within the
ontology construct link to mapping rule.
A similar result holds for unnamed individuals.

Unnamed Individual Lemma

If a graph g corresponds to t
and contains
an unnamedIndividual node n
that is not the object of any
triple then n corresponds to
a directive in t
 Proof:

n is blank and
hence must arise from one of the mapping rules
that introduces a blank node. Moreover, by considering
the
rdf:type
triples with n as subject,
the only mapping rules to consider are those
for the individual construct from the abstract
syntax.
These mapping rules can only be invoked in certain contexts
[ ... enumerate contexts, automatic needed? ... ];
in all of these the returned node becomes the object of a triple,
except for the context transforming a directive within the
ontology construct link to mapping rule.
The reduction lemmas all involve taking a subgraph of an acceptable
graph. Most subgraphs of acceptable graphs are themselves acceptable.
The precise relationship is:

Subgraph Lemma

Given a graph h such that:
Then h is acceptable.
 Proof:
 Given an acceptable graph g with
subgraph h, take the
categorization of
the nodes of g and restrict it to be
a categorization of the nodes of h.
In a typical mapping of an abstract syntax tree,
explicit type triples get generated many times over.
To avoid complications from this we use the following result.

Explicit Type Lemma

If n is a node in an acceptable graph g
then either n is a builtin uriref or when it
has a category found in the table
below g contains an explicit type triple as shown.
 Proof:
 By the first condition on acceptable graphs
there is some such an explicit type triple, moreover
it cannot have object
rdf:Property
,
rdfs:Class
,
owl:FunctionalProperty
,
owl:DeprecatedProperty
,
owl:DeprecatedClass
, and must appear
in one of the triple tables.
By inspection of the triple tables,
many categories have only one such explicit type triple
and these are listed below.
add machine generated table
The typical reduction lemma has an acceptable
graph g and a subgraph h.
We need to show that h is acceptable, and
that given a correspondence involving h we can form
a correspondence of g.
Using the subgraph lemma
we only need to consider whether h
is explicitly typed and whether the blank nodes in h
meet the structural requirements.
Such requirements
on a blank node b in h
are characterised by the set of triples with b as their subject.
Most nodes in an acceptable graph require explicit type triples.
In general, the induction works by first reducing all other triples
involving a node, and then by reducing the explicit type triple.
This does not work for most blank nodes which are treated differently.
We first consider the case where of a ground explicit type triple.

Ground Explicit Type Reduction Lemma

If g is an acceptable graph
containing some ground, explicit type triple tr
with subject n
which appears in no other triple, except other explicit type triples,
then g
can be reduced by removing that triple.
 Proof:

Let h be g  { tr }.
Every node in h is explicitly typed in g
and hence also explicitly typed in h (if n is
in h, then it has multiple explicit type triples in g
and hence has at least
one
of them in h).
For any blank node
b in h the set:
{ s : s ∈ h, s has subject b }
is the same as the set:
{ s : s ∈ g, s has subject b }
Since g is acceptable, this set of triples
meets the structural requirements.
So by the subgraph lemma
,
h is acceptable.
We use the table
below to look up the triple and find a directive in the abstract syntax.
This table has been constructed such that the directives
map to the given explicit type triple and
possibly other explicit type triples that are required by the
explicit type lemma
.
Given an abstract syntax tree corresponding to h
we can form a tree corresponding to g by adding the additional
directive found in the table.
add machine generated table
We now consider the case where the explicit type is a blank node.

Blank Explicit Type Reduction Lemma

If g is an acceptable graph
containing some explicit type triple tr
with uriref subject n
which appears in no other triple, except for other
explicit type triples,
and the object of tr is a blank node b,
then g
can be reduced by removing that triple.
 Proof:

As before, h is acceptable.
b
must be
a description or a restriction (by inspection
of the triple tables).
We use the table below to find a directive corresponding
to tr. Each entry contains one unexpanded nonterminal
from the abstract syntax grammar; this being
either restriction
or description
.
Since b is
the
object of at most one triple
in g,
and that triple is tr which is not in h, we have
that b is not the object of any triple in h.
Hence, the
description lemma
applies and a directive
d
in any abstract syntax tree corresponding to h
corresponds to d.
Thus a new abstract syntax tree can be formed, by cutting d
from the old tree and pasting it into the partially unexpanded directive,
and adding this new directive into the tree.
add machine generated table
Other ground triples can be treated similarly.

Ground Triple Reduction Lemma

If g is an acceptable graph
containing a ground triple tr,
which is not an explicit type triple, then g
can be reduced by removing that triple.
 Proof:

As before, h is acceptable.
We use the table below, to look up the triple tr
and find a directive to be added
to an abstract syntax tree corresponding to h,
to form an abstract syntax tree corresponding to g.
This table has been constructed such that the directives
map to the given ground triple and
possibly explicit type triples that are known to
be in g by the
explicit type lemma
.
add machine generated table
Triples with a ground subject and blank object
where that object is a restriction, description, unnamedDataRange or unnamedIndividual
node
can be treated failry similarly; using the
description lemma
or the
unnamed individual lemma
.
We refer to these triples as GroundGroundBlank (GGB) triples.

GGB Triple Reduction Lemma

If g is an acceptable graph
containing a triple tr,
with ground subject, and blank object b, such that:
b does not have explicit type
rdf:List
;
and tr
is not an explicit type triple, then g
can be reduced by removing that triple.
 Proof:

As before, h is acceptable.
Take an abstract syntax tree t corresponding to h.
By inspection of the triple table b must
have category unnamedIndividual,
unnamedDataRange, descriptionor restriction.
Similarly to in the
blank explicit type reduction lemma
using either the description lemma
or the
unnamed individual lemma
we find a directive d
in t corresponding to b.
We can form a tree corresponding to g by:
 finding tr in the table below.
 modify the directive found in the table
by substituting d appropriately.
 modifying t by
deleting d and adding the new directive
modified from the table below.
add machine generated table
Blank nodes with explicit type rdf:List
are treated somewhat differently.
Instead of forming a subgraph we form a smaller graph
by deleting three triples and
replacing the object of a fourth triple.

First List Reduction Lemma

If g is an acceptable graph
containing a node n
of explicit type
rdf:List
such that n is not the object of
a triple with predicate rdf:rest
,
and n is the subject of
a triple with predicate rdf:first
and a uriref
or literal object uuu, then it is reducible.
 Proof:

By the structural
constraints on n in g there must be nodes
sss, lll and uriref ppp
such that the following triples are in g.
sss ppp n .
n rdf:type rdf:List
.
n rdf:first
uuu .
n rdf:rest
lll .
Moreover, there are no other occurrences of n
in g.
Let h be g with these four triples deleted,
and the following triple added:
sss ppp lll .
h is acceptable with the same categorization as
g because:
 the node n has been
excised completely, and so cannot contribute to nonacceptability,
 ppp is not rdf:type, (since there is no match in the triple tables)
and so no explicit type triples, other than for n
have been excised.

lll is either
rdf:nil
or of
the same category as n, by considering the triple
tables for rdf:rest
. Either way
since
sss ppp n .
is in the triple tables, so is
sss ppp lll .
 Any other contravention of the acceptability of h
would
not involve the new or deleted triples, and
hence also be a contravention of the acceptability of
g.
Given an abstract syntax tree t corresponding to
h then since the node lll
is either of a list category or rdf:nil
,
it must arise from one of the Seq mapping rules.
Moreover ppp is not rdf:rest, and so the context in which
that mapping rule was invoked is not one of the tail recursion
rules add list of rules.
Thus the mapping rule that gave lll as a result
must have been invoked from add list of rules.
In each of these rules, the sequence construct arises from a repeated
construct in an abstract syntax rule one of:
 { individualID }
 { description }
 { Super( description ) }
 { dataLiteral }
Modifying t by adding the uriref
or literaluuu
at the beginning of the appropriate matching subtree
results in an abstract syntax tree corresponding to g.
add machine generated table
We now consider the case where the
first item in the list is a blank node.

Second List Reduction Lemma

If g is an acceptable graph
containing a node n
of explicit type
rdf:List
such that n is not the object of
a triple with predicate rdf:rest
,
and n is the subject of
a triple with predicate rdf:first
and a blank object bbb, then it is reducible.
 Proof:

We construct h similarly to the
first list reduction lemma
.
The triples
sss ppp n .
n rdf:type rdf:List
.
n rdf:first
bbb .
n rdf:rest
lll .
found in g are replaced by the single triple:
sss ppp lll .
in h.
h similarly is acceptable. However, since bbb is blank,
the node n must be of category listOfDescription.
So ppp must be owl:intersectionOf
or owl:unionOf
.
Given an abstract syntax tree t corresponding to
h As in lemma 1 the mapping rule that invoked the rule that
created lll must be one of add smaller list of rules.
In each of these rules, the sequence construct arises from a repeated
construct in an abstract syntax rule of
{ description } or { Super( description ) }.
Since bbb is the
object of at most one triple
in g
and that triple has been deleted, it is not the object of any triple
in h and the description lemma
applies.
Thus we can
modify t by cutting the toplevel
description or restriction
that
corresponds to bbb and pasting it
at the beginning of the appropriate matching subtree,
possibly inside a Super( )
construct.
The resulting abstract syntax tree corresponds to g.
add machine generated table
We now consider unnamedIndividual nodes.
These behave quite similarly to individualID nodes,
but need to be treated slightly differently.
With individualIDs the uriref can link multiple
directives in the abstract syntax; with unnamed individuals
it is necessary to ensure that everything that
needs to be said about the individual is said in a single
directive.
Nearly as before, we first consider a solitary explicit type triple,
dividing it into two cases: a named or an unnamed type.
Then we consider the other triples (including multiple explicit type triples).
We first consider the case where the type is not a blank node

First Unnamed Individual Explicit Type Reduction Lemma

If g is an acceptable graph
containing some explicit type triple tr
with subject n
which is an unnamed individual,
and has a uriref node as object, and
n appears in no other triple, then g
can be reduced by removing that triple.
 Proof:

Let h be g  { tr }.
Every node in h is explicitly typed in g
and hence also explicitly typed in h (n is
not in h).
For any blank node
b in h the set:
{ s : s ∈ h, s has subject b }
is the same as the set:
{ s : s ∈ g, s has subject b }
Since g is acceptable, this set of triples
meets the structural requirements,
and by the subgraph lemma
,
h is acceptable.
Given an abstract syntax tree corresponding to h
we can form a tree corresponding to g by adding the additional
directive Individual(Type(classID))
where classID
is the object of the tr
. This new tree corresponds to g.
The case where the type is a blank node is similar.

Second Unnamed Individual Explicit Type Reduction Lemma

If g is an acceptable graph
containing some explicit type triple tr
with subject n
which is an unnamed individual,
and has a blank node as object, and
n appears in no other triple, then g
can be reduced by removing that triple.
 Proof:

h is acceptable as before.
Given an abstract syntax tree t corresponding to h,
as in the blank explicit type reduction lemma
, we can find a
directive in t which corresponds to the type of n.
We can form a tree corresponding to g from t
by deleting that directive
and adding the additional
directive Individual(Type(expr))
where expr
is the restriction or description directive deleted from t.
This new tree corresponds to g.
We now consider some other triples with
an unnamed individual as subject and a uriref or literal
as object

First Unnamed Individual Triple Reduction Lemma

If g is an acceptable graph
containing a triple tr
with subject n such that:
n
which is an unnamed individual;
there is some other explicit type triple for n in g;
tr has a uriref or literal node as object;
and n is not the object of any triple,
then g
can be reduced by removing tr.
 Proof:

We show h is acceptable, as in
first unnamed individual explicit type reduction lemma
, with the following additional considerations.
n does have an explicit type in h,
moreover since it has category unnamedIndividual, it does
not violate the structural constraints.
Given an abstract syntax tree t corresponding to h
we can form a tree corresponding to g by:
 finding tr in the table below
 using the unnamed individual lemma
to find
the directive in t corresponding to
n, this has form
Individual( … )
.
 modifying t by adding into the
Individual( … )
expression the syntactic expression found with tr
in the table below.
add machine generated table
We now consider some other triples with
an unnamed individual as subject and a blank node
as object

Second Unnamed Individual Triple Reduction Lemma

If g is an acceptable graph
containing a triple tr
with subject n such that:
n
is an unnamed individual;
there is some other explicit type triple for n in g;
tr has a blank node b as object;
and n is not the object of any triple,
then g
can be reduced by removing tr.
 Proof:

h is acceptable, as in
first unnamed individual triple reduction lemma
.
Take an abstract syntax tree t corresponding to h.
By inspection of the triple table b must
have category unnamedIndividual, description
or
restriction
and so by the description lemma
or the
unnamed individual lemma
we find a directive d
in t corresponding to b.
We can form a tree corresponding to g by:
 finding tr in the table below.
 modify the syntax expression found in the table
by substituting d appropriately.
 using the unnamed individual lemma
to find
the directive in t corresponding to
n, this has form
Individual( … )
.
 modifying t by adding into the
Individual( … )
expression the modified syntactic expression from the table below.
add machine generated table
We now consider some other blank nodes.

First Structure Reduction Lemma

If g is an acceptable graph
containing a blank node n such that:
n is of category
allDifferent, unnamedDataRange, description or restriction;
there are no triples
with subject n and object being
a blank node;
n is not the object of any
triple; n is not the subject of a triple with predicate
owl:equivalentClass
or owl:disjointWith
.
Then g can be reduced by removing
all the triples involving n.
 Proof:

As before, h is acceptable.
The triple tables impose significant
structural requirements on
all nodes satisfying the premises of this lemma.
The table below gives an exhaustive listing of
the possibilties, along with a corresponding directive
from the abstract syntax.
As before we can modify an
abstract syntax tree corresponding to h
by adding the appropriate directive, to get an
abstract syntax tree corresponding to g.
add machine generated table
We also consider some cases where a restriction or
description has a second restriction or description embedded
within it.

Second Structure Reduction Lemma

If g is an acceptable graph
containing a blank node n such that:
n is of category
description or restriction;
there is exactly one triple
with subject n with object being
a blank node b;
b is of
category description or restriction;
n is not the object of any triple;
n is not the subject of a triple with predicate
owl:equivalentClass
or owl:disjointWith
.
Then g can be reduced by removing
all the triples involving n to form h.
 Proof:

As before, h is acceptable.
Given an abstract syntax tree t
corresponding to h, as
in the blank explicit type reduction lemma
we can find a
directive d that corresponds to b.
We use the table below to look up the node n,
and find a directive, into which we substitute
the directive d appropriately.
We then modify t by deleting d and
adding the new modified directive from the table.
This then corresponds to g.
add machine generated table
We finally consider the case of a restriction or
description compared with some other node.

Description Comparison Reduction Lemma

If g is an acceptable graph
containing a blank node n such that:
there is a triple tr
with subject n and with predicate
owl:equivalentClass
or owl:disjointWith
;
tr has object b.
Then g can be reduced by removing
tr to form h.
 Proof:

The only triples in the triple tables
matching tr are ones in which n is of category
description or restriction.
We note that n meets the structural constraints
in h,
because it meets those constraints in g and the deleted triple
is not relevant to those constraints.
Thus, as before, h is acceptable.
Given an abstract syntax tree t
corresponding to h, as
in the
blank explicit type reduction lemma
we can find a
directive d_{1} in t that corresponds to n.
Note, that since g is appropriate, and n is the subject
of an owl:equivalentClass
or owl:disjointWith
triple, then n is not the object of any triple in neither
g nor h.
If b is blank, then it is a restriction or description node,
and we similarly can find a directive
d_{2} in t that corresponds to b.
We use the table below to look up the triple tr,
and find a directive, into which we substitute
the description or restriction d_{1} and either the classID uriref
b or the description or restriction d_{2} appropriately.
We then modify t by adding the new modified directive
and by deleting d_{1},
and if applicable d_{2}.
This then corresponds to g.
add machine generated table
This section further explores the constraints
on blank nodes in an acceptable graph.

Blank Node Lemma

If an acceptable graph g
contains a blank node then it contains
either a blank node that is the object
of a triple with a uriref subject, or
it contains a blank node which is the object
of no triples.
 Proof:

Define a partial function on the blank nodes
of g mapping
a blank node
b_{i} in g
which is the object of a triple tr
to the subject of that triple
b_{i+1}.
Since g contains a first blank node
b_{1}, we can form a sequence
b_{1},
b_{2}
…
Since g is finite, and
does not contain any cycles
of blank nodes, this sequence must terminate.
The last element of this sequence, must either be a blank
node that is not the object of any triple, or a uriref
node that is the subject of a triple with a blank node as
object.
Lists can always be reduced.

List Lemma

An acceptable graph g
containing a node of explicit type
rdf:List
is reducible.

Proof:

We define a partial function from a node
b_{i}
of explicit type
rdf:List
that returns the subject
b_{i+1}
of the triple
with predicate rdf:rest
and object
b_{i+1}.
As before the sequence
b_{1},
b_{2}
…
terminates, furnishing a node
b_{n}
that has explicit type rdf:List
and is not the object of an rdf:rest
triple.
Hence, either
the
first list reduction lemma
or the
second list reduction lemma
apply to g.
We can also combine
the reduction lemmas for unnamed individuals:

Unnamed Individual Reduction Lemma

An acceptable graph
with
an unnamed individual node that is not the object
of any triple can be reduced.
 Proof:

One of the following must apply:
The final stages of the proof.

Ground Reducible Graph Lemma

A ground nonempty acceptable graph
can be reduced by one of the reduction rules.
 Proof:

Either
the
ground explicit type reduction lemma
or
the
ground triple reduction lemma
applies.

Reducible Graph Lemma

A nonempty acceptable graph
can be reduced by one of the reduction rules.
 Proof:

Suppose not. Then by
the ground reducible graph lemma
we have that there must be a blank node
b.
Moreover,
by the list lemma
b cannot be of type
rdf:List
.
Hence, if b were the object of
a triple with a uriref subject, we can apply either
the
ggb triple reduction lemma
or the
blank explicit type reduction lemma
.
Thus, by the blank node lemma
,
without loss of generality, we have that b is
not the object of any triple.
Since b is not of type
rdf:List
, it must be of
category
unnamedIndividual, allDifferent,
unnamedDataRange, description, or restriction.
By the unnamed individual lemma
the first possibility is excluded.
Since the description comparison reduction lemma
does not apply, b is not the subject of a triple
with predicate owl:disjointWith
,
or owl:equivalentClass
.
The conditions on b and g
now meet the premises of the
structured nodes lemma
and so g is, after all, reducible.
We now can prove the main results:

Correspondence Theorem

Every acceptable graph corresponds to
an abstract syntax tree.
 Proof:

By induction, with initial step furnished
by the
empty graph lemma
and inductive step by the
reducible graph lemma
.
 Corollary:
Sufficiency Theorem

Every acceptable graph is mappable.