- From: Jeremy Carroll <jjc@hpl.hp.com>
- Date: Fri, 20 Jun 2003 09:20:34 +0300
- To: www-webont-wg@w3.org
Peter:
>The summary is that there are significant holes in the proof. I don't know
>whether they can be fixed.
Copying from peter's msg, and filling in the holes ...
(i.e. lines beginning | come from jjc
http://lists.w3.org/Archives/Public/www-webont-wg/2003Jun/0017
lines beginning > come from pfps
http://lists.w3.org/Archives/Public/www-webont-wg/2003Jun/0111
lines beginning * are new comments from jjc (this message)
lines beginning - are additions to the proof from pfps
other lines are additions to the proof from jjc (this message)
)
comments?
Jeremy
| 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.
> This lemma appears to be about optional typing.
*No change (this lemma is not about optional typing).
| 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
>I do not believe that this definition works correctly. It doesn't
>correctly take into account the optional type triples, for example.
*No change, optional type triples are not *uses* of the bnode as defined.
*This motivates an editorial change:
*(moved text)
*correction
Definition of "using" and "uses":
| A triple *using* b
| is one that either has object b, or has subject b
| and predicate owl:equivalentClass
| or owl:disjointWith.
| 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 }|
|
|
*Old text concerning using was here.
| 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.
- because d = d'
| Extending and restricting T we map A1 to G1, a subgraph of G
| and we map {A2} to G1 union
| { <M(T(d)) owl:equivalentClass M(T(d')) > }
> ^^ ^ ^^ ^
*correction
{ <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
| M(T(d)) owl:equivalentClass M(T(d')) .
> ^^ ^ ^^ ^
*correction
T(d) owl:equivalentClass T(d') .
| Since G1 is a subgraph of G we are done.
>It might be easier to do this directly.
*Agreed - the indirect fashion has no dependence on the
*exact form of the "theorem to be proved by Peter".
New Lemma: multiple usage of a bnode.
If there is a blank node b such that
two triples in G use b then BRC(G)=0.
Proof:
| { <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 }| > 0
Suppose there is no blank node used by more than one triple.
Then by the definition of using,
"<s, p, b> in G or
<b, owl:equivalentClass, o> in G or
<b, owl:disjointWith, o> in G"
is an exclusive or, so that
| { b : b blank and
<s, p, b> in G or
<b, owl:equivalentClass, o> in G or
<b, owl:disjointWith, o> in G }|
=
| { b : b blank and <s, p, b> in G}|
+
| { b : b blank and <b, owl:equivalentClass, o> in G}|
+
| { b : b blank and <b, owl:disjointWith, o> in G }|
[**]
Moreover, since each blank node is used at most once, and <s,p,b> is a use of
the blank node, we have:
| { b : b blank and <s, p, b> in G}| =
| { <s, p, b> : b blank and <s, p, b> in G}|
and
| { b : b blank and <b, owl:equivalentClass, o> in G}|=
| { <b, owl:equivalentClass, o> :
b blank and <b, owl:equivalentClass, o> in G}|
and
| { b : b blank and <b, owl:disjointWith, o> in G}|=
| { <b, owl:equivalentClass, o> :
b blank and <b, owl:disjointWith, o> in G}|
Substituting these three equations in [**] gives us that BRC(G)=0.
| 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
t and t'
| in G use b.
>You haven't shown this.
*I have added the new lemma above.
, as follows from the multiple usage of a bnode lemma.
| 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.
, with t using T(d) and t' using T(d') (in the overall
application of T, remember b=T(d) = T(d'))
W.l.o.g. we take d to occur before d'.
|
| 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.
*Additional text, addressing Peter's comment below.
The bnodes of G' are the bnodes of G unioned with the bnodes
of T'( EquivalentClass(d'') ). This is a disjoint union,
because the bnode reuse clause was not invoked
in the application of T' to EquivalentClass(d'').
The triples of G' are the triples of G unioned
with the triples of T'( EquivalentClass(d'') ).
Any triple in G that includes a bnode cannot
appear in the triples of T'( EquivalentClass(d'') ),
and conversely.
Since BRC depends on blank nodes and triples
that include blank nodes, we have:
BRC(G') = BRC(G) + BRC(T'( EquivalentClass(d''))
and since T'( EquivalentClass(d'')) does not
involve any bnode reuse we have
BRC(T'( EquivalentClass(d''))= 0
so that
BRC(G') = BRC(G)
*minor wording changes in the next few lines
|
| Let G'' be G' with triple
t' in G'
| using b
| replaced by a similar triple
t'' in G''
| using T'(d'')
by replacing b with T'(d'').
*next line moved down
*| BRC(G'') = n - 1.
>You haven't shown that BRC(G') = BRC(G)
*addressed above
>or that BRC(G'') = BRG(G') - 1
* here goes ...
We start by assuming that t' and t'' only use
one blank node (i.e. that they do not have
predicate owl:disjointWith or owl:equivalentClass
and also both subject and object as blank).
| { t in G'': bb blank, t uses bb }|
=
| { t in G''\t'': bb blank, t uses bb }| + | {t''}|
=
| { t in G'\t': bb blank, t uses bb }| + | {t'}|
=
| { t in G': bb blank, t uses bb }|
(noting that G''\t''=G'\t' and that t'' and t' both use
a blank node)
| { bb : bb blank and
t in G'', t uses bb }|
=
| { bb : bb blank and
t in G''\t'', t uses bb }|+|{T'(d'')}|
=| { bb : bb blank and
t in G'\t', t uses bb }|+1
=| { bb : bb blank and
t in G', t uses bb }|+1
(noting that T'(d'') is used in t'', G''\t''=G'\t',
and that the blank node used by t' is also
used by some other triple in G'\t').
Thus
BRC(G'') =
| { t in G'': bb blank, t uses bb }|
- | { bb : bb blank and
t in G'', t uses bb }|
=
| { t in G': bb blank, t uses bb }|
- (| { bb : bb blank and
t in G', t uses bb }|+1)
= BRC(G') - 1
The other case (where t' and t'' use two blank
nodes, one shared between them) is similar.
i.e.
| 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.
>I'm not convinced of this.
Mirror the construction of A' from A,
in forming A'' from A by adding an initial
axiom EquivalentClass(d'').
T' transforms A' to G', and also transforms A'' to G'
(only the order of application has changed.
The bnode reuse is the only part of the
transformation that has any order dependency,
and EquivalentClass(d'') is transformed without
any bnode reuse).
When we produce t' in G', we invoke
bnode reuse for d' corresponding to b=T(d).
Let T'' transform A'' be defined as T' on A''
except that Instead of reusing T(d) in the mapping
producing t', we reuse
T(d'') instead.
We then restrict T'' to A, noting that when transforming
d' we are now no longer reusing the mapping of d''
but instead this is the first use of that mapping
as provided by T''.
| 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 { < M(T'(d'')) owl:equivalentClass M(T(d)) > }
> ^^ ^ ^^ ^
*Correction
G'' union { < T'(d'') owl:equivalentClass T(d) > }
- because T(d'') and T(d) don't share blank nodes
| 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 Friday, 20 June 2003 03:20:43 UTC