- From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>
- Date: Wed, 11 Jun 2003 15:51:46 -0400 (EDT)
- To: jjc@hplb.hpl.hp.com
- Cc: www-webont-wg@w3.org
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