From: Guus Schreiber <schreiber@cs.vu.nl>

Date: Wed, 11 Jun 2003 23:41:37 +0100

Message-ID: <3EE7B021.50507@cs.vu.nl>

To: Jeremy Carroll <jjc@hplb.hpl.hp.com>

CC: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>, www-webont-wg@w3.org

Date: Wed, 11 Jun 2003 23:41:37 +0100

Message-ID: <3EE7B021.50507@cs.vu.nl>

To: Jeremy Carroll <jjc@hplb.hpl.hp.com>

CC: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>, www-webont-wg@w3.org

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 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Monday, 7 December 2009 10:58:01 GMT
*