Re: B1 B2 proof

Jeremy Carroll wrote:

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

OK. Will add this to the telecon agenda under agenda item 3.
Guus

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

-- 
NOTE: new affiliation per April 1, 2003

Free University Amsterdam, Computer Science
De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands
Tel: +31 20 444 7739/7718
E-mail: schreiber@cs.vu.nl
Home page: http://www.cs.vu.nl/~guus/ [under construction]

Received on Wednesday, 11 June 2003 18:41:53 UTC