Re: B1 B2 proof

Quickish response ... I suspect a little discussion at the telecon might 
then permit us to see which way to go.


Peter F. Patel-Schneider wrote:

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


Thanks for the review.
My summary is that there is an "M" that seems to be flying around somewhat 
loosely - at first glance it just looks like a complex typo; and a couple 
of places where Peter would like me to lengthen the proofs by taking 
smaller jumps; but nothing too serious.

I doubt I'll have time to move on either before the telecon tomorrow.


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


Not sure which lemma you mean: The one above is needed because the current 
mapping rules effectively allow bnode reuse (as counted by the BRC formula 
below), in some sense they could be simplified with bnode reuse to only 
have n=2. The proof works with n=2, and the lemma permits that restriction 
w.l.o.g.

The lemma below is needed to describe which triples the blank nodes that 
might be reused may appear in - this is pretty fundamental to the proof - 
since these triples (particularly parts B and C) have semantic conditions 
that depend in a necessary and sufficient way on the class extensions.


> 
> | 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 it does not take into account any triples which the bnodes are subject 
of, except owl:equivalentClass or owl:disjointWith. The optional type 
triples are wholly irrelevant, since they are only permitted on bnodes 
which must have a more constrained class.

The other triples, e.g. those with predicate owl:onProperty or the required 
type triple, are part of the structure corresponding to the description or 
restriction in the abstract syntax, rather than the use of the description 
or restriction in the abstract syntax.


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


Hmm, I'm not sure what that M is ...


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


Assuming this is the sentence above "Since BRC(G) > 0 ... "
That's straightforward ... I can add another lemma for it.


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


I can spell that out, both follow by construction.


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


OK I can spell that out too, it makes it somewhat longwinded, sigh.


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


Yes that's worth saying (I do need to work out what this M thing is)


> 
> | 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 16:22:36 UTC