B1 B2 proof

We can weaken the constraint on blank nodes corresponding to descriptions 
and dataranges to be that all directed cycles of such nodes must have an 
owl:equivalentClass or owl:disjointWith triple.


Sketch
======
We assume that Peter shows the correspondence
theorem without any reuse of bnodes.
We show that any two identical descriptions are
equivalent classes.
The only possible syntactic uses of bnodes
corresponding to descriptions in OWL DL occur
either in triples whose OWL Full semantics
depends only on the class extension of the bnode,
or on rdf:first triples in lists which are the object
of owl:unionOf and owl:intersectionOf triples.
In the first case we can replace a bnode by an
equivalent one, in the second case, given an equivalent
bnode we can use the comprehension axioms to construct
an equivalent list, and then use that since the
semantics of the owl:unionOf and owl:intersectionOf
triples only depend on the class extensions.
These permit us to proceed by induction on the number
of bnodes reused.


B1 B2 Proof
===========


Preliminaries:
We add to the preamble to the mapping rules words like:
[bnode reuse]
"When processing an abstract syntax construct corresponding
to either the description, restriction or dataRange construct
then, if that exact instance of the construct has already
occurred then there is at least one blank
node already corresponding to the construct. In such a case,
the mapping may nondeterministically use any previous result
(a blank node) or may apply the mapping rues to the new occurrence."

Lemma: Simplified EquivalentClass and DisjointClasses construct.
Given the new mapping rules, if G is a graph corresponding to
an abstract syntax tree A then G corresponds to A' in which
all occurrences of EquivalentClass and DisjointClasses have
at most two descriptions.

Proof:
We form A' from A by copying the ontology
and modifying the EquivalentClass and DisjointClasses
axioms.
Take each
EquivalentClass( d1 .... dn ) n > 2
and
if
T(di) owl:equivalentClass T(dj) . is in G
add
EquivalentClassses(di dj)
and delete each EquivalentClasses( d1 ... dn ) n > 2
Similary for DisjointWith( d1 ... dn )
We can take the mapping T:A -> G and use it to map
A'->G, using the new clause in the preamble of the mapping rules.

Lemma: Blank description usage.
If A is an OWL DL abstract syntax tree and G
is a corresponding RDF graph and b is some blank node
in G, for which the mapping rule that created b
was one of those with an optional rdf:type owl:Class
or rdf:type owl:Restriction or rdf:type owl:DataRange
triple; suppose t is a triple containing b then t
matches one of:

A)
b rdf:type rdfs:Class .
b rdf:type owl:DataRange .
b rdf:type owl:Restriction .
b rdf:type owl:Class .
B)
XX rdf:first b .
(moreover XX forms part of a list
where that list is the object of a
triple with predicate owl:unionOf
or owl:intersectionOf).
C)
b owl:disjointWith XX .
XX owl:disjointWith b .
XX owl:equivalentClass b .
b owl:equivalentClass XX .
XX owl:someValuesFrom b .
XX owl:allValuesFrom b .
XX owl:complementOf b .
XX rdf:type b .
D)
b owl:intersectionOf XX .
b owl:unionOf XX .
b owl:complementOf XX .
b owl:oneOf XX .
b owl:onProperty XX .
b owl:cardinality XX .
b owl:minCardinality XX .
b owl:maxCardinality XX .
b owl:someValuesFrom XX .
b owl:allValuesFrom XX .

Proof: by inspection

Definition: The bnode reuse count BRC or a graph G
is the amount of bnodes usage more than once each i.e.

BRC(G) = | { <s, p, b > in G: b blank }|
         + | { <b, owl:equivalentClass, o> in G: b blank }|
         + | { <b, owl:disjointWith, o> in G: b blank }|
         - | { b : b blank and
                     <s, p, b> in G or
                     <b, owl:equivalentClass, o> in G or
                     <b, owl:disjointWith, o> in G   }|


Terminology: we will say that a triple *using* b
is one that either has object b, or has subject b
and  and predicate owl:equivalentClass
or owl:disjointWith.

Theorem: to be proved by Peter,
If graph G corresponds to an
abstract ontology A
and the mapping from A to G does not
involve any bnode reuse, then the correspondence
theorem holds.



Lemma: If graph G corresponds to an
abstract ontology A and BRC(G)=0
then the correspondence theorem holds.

Proof:
Let T be the mapping from A to G.
All bnodes in G are the object of at most one
triple. bnode reuse can only occur for
bnodes corresponding to the EquivalentClass(d1)
construct, which generates a bnode that can be
reused that is the object of no triples (or
alternatively may reuse a bnode without making it
the object of any triple). Let us call an
axiom of this form redundant if T(d1) is the
object of a triple, or if it is not the first
axiom in the ontology mapping to that bnode.
Let A' be A with all redundant axioms deleted.
A' corresponds to G by the restriction of T to A'.
A' has no bnode reuse so Peter's result holds,
between A' and A. The vocabulary usage of A' and
A are identical; and A and A' are logically
equivalent by the direct semantics.
Thus the correspondence theorem holds between A
and G.


Lemma: identical descriptions.
If A is an abstract ontology
and G corresponds to A under T, and d and d'
are two occurrences of an identical description
in A with T(d) != T(d') and with the mapping
of the subdescriptions of d and d' also not sharing
bnodes then all interpretations
of G are interpretations of
   T(d) owl:equivalentClass T(d') .

Proof:
Let A1 = ontology( EquivalentClass(d) EquivalentClass(d') )
Let A2 = ontology( EquivalentClass(d d') )
By the direct semantics A1 entails A2.
Extending and restricting T we map A1 to G1, a subgraph of G
and we map {A2} to G1 union
{   <T(d) owl:equivalentClass T(d') > }
Since the mapping of T(d) and T(d') do not share bnodes
both the mapping T:A1 -> G1 and T:A2 -> G2 are covered
by the correspondence theorem without bnode reuse.
Thus we have that any interpretation of G1 is an
interpretation of
   T(d) owl:equivalentClass T(d') .
Since G1 is a subgraph of G we are done.

Theorem: The correspondence theorem holds.

Proof: by induction on BRC.
Initial case, BRC(G) = 0, by Peter's result.
Suppose n > 0, and the result holds for all G with
BRC(G) < n.
Suppose BRC(G) = n, with A corresponding to G by mapping T.
T(A)=G
w.l.o.g. A does not contain an EquivalentClass
or DisjointClasses with n > 2 (see lemma).
Since BRC(G) > 0 we have there is a blank node b
such that two triples in G use b.
This must be by use of the bnode reuse
clause of the preamble. (We have explicitly excluded
the two mappings rules EquivalentClass, DisjointClasses,
which introduce multiple copies of bnodes).
The bnode b hence corresponds to two identical descriptions
d and d' within A.

Form A' by adding a final axiom EquivalentClass(d'')
with d'' = d' = d
Extend T to T' to map A' by mapping the new axiom
without invoking the bnode reuse clause.
Let G' = T'(A'), this is a superset of G.

Let G'' be G' with one of the triples using b to be
replaced by a similar triple using T'(d'').
BRC(G'') = n - 1.
We can construct a mapping T'' of A to G'' by
not using the bnode reuse clause on one of the
occassions where we had used it.
By the inductive hypothesis the correspondence
theorem holds between A and G''. We now show that
any interpretation of G'' is an interpretation of G
and we are done.
By the identical descriptions lemma we have that
any interpration of G'' is an interpretation of
G'' union { < T'(d'') owl:equivalentClass T(d) > }
The only triple in G which is not in G''
is the triple using T(d) which has been
replaced by that using T'(d''). Looking at the
blank description usage lemma, and the definition
of 'using' we see that this triple must have the
form of section (B) or (C) in the blank description
usage lemma.
If it is of form (C) then the truth of the triple
is a function of the class extension of the
interpretation of the blank node, and does not depend
on the interpretation of the blank node itself. Since
the replacement triple in G'' has a blank node with
identical class extension, then any interpretation
of G'' is also an interpretation of the replaced triple.

If it is of form (B),  it is the object of an
rdf:first triple. This rdf:first triple is part of
a well-formed list, and that list is the object of
an owl:unionOf or owl:intersectionOf triple, t.
Under the RDF semantics the blank nodes in the list
are understood as existentials. By the first comprehension
axiom for lists, there is such a list and so the set of
rdf:first & rdf:rest triples forming the list are true.
The truth of t depends on the semantics of owl:unionOf
and owl:intersectionOf which have necessary and sufficient
conditions that depend only on the class extensions
of the subject and the elements in the list formed
by the object.
Given an interpretation of G'' then this shows that there
is some mapping of the blank nodes making t true in G''.
There is some other mapping of the blank nodes that makes
G - { t } true, i.e. which maps the blank nodes
of the list which is the object of t differently.
Under this interpretation all the members of the list have
the same class extension and so t is still true. Thus this
is an interpreation of G. The proof is complete.

Received on Wednesday, 4 June 2003 13:36:16 UTC