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

Date: Wed, 04 Jun 2003 18:36:00 +0100

Message-ID: <3EDE2E00.5050507@hplb.hpl.hp.com>

To: www-webont-wg@w3.org

Date: Wed, 04 Jun 2003 18:36:00 +0100

Message-ID: <3EDE2E00.5050507@hplb.hpl.hp.com>

To: www-webont-wg@w3.org

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. 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 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 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. Extending and restricting T we map A1 to G1, a subgraph of G and we map {A2} to G1 union { <T(d) owl:equivalentClass 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 T(d) owl:equivalentClass T(d') . Since G1 is a subgraph of G we are done. 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. 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. 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. 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 { < T'(d'') owl:equivalentClass T(d) > } 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, 4 June 2003 13:36:16 GMT

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