Re: B1 B2 proof

Here are my comments on Jeremy's proof.  

The summary is that there are significant holes in the proof.  I don't know
whether they can be fixed.

peter



| 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.

| 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.

| 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 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.
- 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')) > }
       ^^    ^                     ^^     ^
| 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')) .
     ^^    ^                     ^^     ^
| Since G1 is a subgraph of G we are done.

It might be easier to do this directly.

| 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.

You haven't shown this.

| 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.

You haven't shown that BRC(G') = BRC(G) 
or that BRC(G'') = BRG(G') - 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.

| 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)) > }
                ^^      ^                      ^^    ^
- 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 Wednesday, 11 June 2003 15:51:59 UTC