Re: problem with B1 B2

The goal of this message is to show that the B1 B2 approach is not 
invalidated by our current difficult example:

(This is weaker than showing that B1 B2 is valid; the political goal is 
merely to show that it isn't a completely lost cause!)

This msg is intended to be sufficiently straight forward and clear to be 
easy to review.

 > Now consider the following ontology
 >
Ontology(
Class(B partial)
Class(A complete
     restriction(rA
       allValuesFrom(
         restriction(r allValuesFrom(B)))))
Class(C complete
     restriction(rC
       allValuesFrom(
         restriction(r allValuesFrom(B)))))
IndividualValuedProperty(r)
IndividualValuedProperty(rC)
IndividualValuedProperty(rA)
)

 >
 > Under the current mapping results in something containing:
 >

X

 > B rdf:type owl:Class .
 > A rdf:type owl:Class .
   rA rdf:type owl:ObjectProperty .
   rC rdf:type owl:ObjectProperty .
   r rdf:type owl:ObjectProperty .
 > A owl:equivalentClass _:r1 .
 > _:r1 rdf:type owl:Restriction .
 > _:r1 owl:onProperty rA .
 > _:r1 owl:allValuesFrom _:r2 .
 > _:r2 rdf:type owl:Restriction .
 > _:r2 owl:onProperty r .
 > _:r2 owl:allValuesFrom B .
 > C rdf:type owl:Class .
 > C owl:equivalentClass _:r3 .
 > _:r3 rdf:type owl:Restriction .
 > _:r3 owl:onProperty rC .
 > _:r3 owl:allValuesFrom _:r4 .
 > _:r4 rdf:type owl:Restriction .
 > _:r4 owl:onProperty r .
 > _:r4 owl:allValuesFrom B .
 >
 >
 > Under the B1/B2 proposal there could be a mapping to:
 >

Y

 > B rdf:type owl:Class .
 > A rdf:type owl:Class .
 > A owl:equivalentClass _:r1 .
 > _:r1 rdf:type owl:Restriction .
 > _:r1 owl:onProperty rA .
 > _:r1 owl:allValuesFrom _:r2 .
 > _:r2 rdf:type owl:Restriction .
 > _:r2 owl:onProperty r .
 > _:r2 owl:allValuesFrom B .
 > C rdf:type owl:Class .
 > C owl:equivalentClass _:r3 .
 > _:r3 rdf:type owl:Restriction .
 > _:r3 owl:onProperty rC .
 > _:r3 owl:allValuesFrom _:r2 .
 >

As before Y simple-entails X.
i.e.
[[
 > (By duplicating some of the triples and substituting the variable _:r2
 > with the new variable _:r4 in some of the triples - both steps being
 > sound according to simple entailment).
]]


To show that X owl-entails Y, we note that from the comprehension axioms:

{The parts of S&AS used are:
IOR subsetOf IOC
and

If exists x in IOOP and w in IOC then exists y in IOR s.t. <y,x> in 
EXT((S(owl:onProperty)) and <y,w> in EXT((S(owl:allValuesFrom)).


}
X simple-entails

   B rdf:type owl:Class .
   rA rdf:type owl:ObjectProperty .
   rC rdf:type owl:ObjectProperty .
   r rdf:type owl:ObjectProperty .

which owl-entails (using comprehesion)

   rA rdf:type owl:ObjectProperty .
   rC rdf:type owl:ObjectProperty .

  _:yr2 rdf:type owl:Restriction .
  _:yr2 owl:onProperty r .
  _:yr2 owl:allValuesFrom B .

  _:yr2 rdf:type owl:Class .

which owl-entails (using comprehesion)

_:yr1 rdf:type owl:Restriction .
_:yr1 owl:onProperty rA .
_:yr1 owl:allValuesFrom _:yr2 .
_:yr3 rdf:type owl:Restriction .
_:yr3 owl:onProperty rC .
_:yr3 owl:allValuesFrom _:yr2 .

Hence X owl-entails


 > B rdf:type owl:Class .
 > A rdf:type owl:Class .
   rA rdf:type owl:ObjectProperty .
   rC rdf:type owl:ObjectProperty .
   r rdf:type owl:ObjectProperty .
 > A owl:equivalentClass _:r1 .
 > _:r1 rdf:type owl:Restriction .
 > _:r1 owl:onProperty rA .
 > _:r1 owl:allValuesFrom _:r2 .
 > _:r2 rdf:type owl:Restriction .
 > _:r2 owl:onProperty r .
 > _:r2 owl:allValuesFrom B .
 > C rdf:type owl:Class .
 > C owl:equivalentClass _:r3 .
 > _:r3 rdf:type owl:Restriction .
 > _:r3 owl:onProperty rC .
 > _:r3 owl:allValuesFrom _:r4 .
 > _:r4 rdf:type owl:Restriction .
 > _:r4 owl:onProperty r .
 > _:r4 owl:allValuesFrom B .
  _:yr2 rdf:type owl:Restriction .
  _:yr2 owl:onProperty r .
  _:yr2 owl:allValuesFrom B .
_:yr1 rdf:type owl:Restriction .
_:yr1 owl:onProperty rA .
_:yr1 owl:allValuesFrom _:yr2 .
_:yr3 rdf:type owl:Restriction .
_:yr3 owl:onProperty rC .
_:yr3 owl:allValuesFrom _:yr2 .


Noting that this then owl-entails

_:yr1 owl:equivalentClass _:r1 .
and
_:yr3 owl:equivalentClass _:r3 .

we can further conclude that

A owl:equivalentClass _:yr1 .
and
C owl:equivalentClass _:yr3 .

and by discarding spurious triples and renaming the blank nodes we have the 
result.

===

I believe that the technique used in the above demonstration can be 
generalized and embedded within the inductive structure of the previous 
flawed proof. However, this is non-trivial.

Jeremy

Received on Thursday, 4 September 2003 10:13:54 UTC