Fwd: Re: bug in semantics (was Re: intersectionOf and subClassOf)

Still testing really - I am having config difficulties

----------  Forwarded Message  ----------

Subject: Re: bug in semantics (was Re: intersectionOf and subClassOf)
Date: Sun, 11 May 2003 23:43:00 +0300
From: Jeremy Carroll <jjc@hpl.hp.com>
To: www-webont-wg@w3.org

(resend, with two extra paragraphs at beginning of rationale, and two more at
end)

With a little bit of thought I am pretty clear this is a bug in the (OWL
 Full) semantics not the mapping rules

I assume that the change we are discussing impacts owl:complementOf
owl:unionOf owl:intersectionOf owl:oneOf and would amount to

s/then if <x,y> in EXTI(SI(E)) then/<x,y> in EXTI(SI(E)) iff/

above the table of semantic conditions for these properties.

I believe we should do:
> 2/ Leave the mapping the way it is and upgrade owl:intersectionOf from a
>    syntactic relationship to a semantic one.

not

> 1/ Change the mapping back to the way it was, so that, for example, classes
>    are not related to their ``definition'' by owl:intersectionOf
>    relationships.  Instead there would be an anonymous intersection class
>    related to the named class by an equivalence link.

Rationale:

A) too many examples in the guide would either be in OWL Full or would have
 to change significantly with the proposed changes to the mapping rules.

B) The proposed changes to the OWL Full semantics makes various intuitive
entailments hold (the ones that are currently in doubt)

I give some examples, under the current semantics these are all OWL DL
entailments and OWL Full non-entailments.
Peter's fix 1/ (change the mapping rules) makes these non-OWL DL, and hence
leaves them as non-entailments in OWL Full. (Thus fixing the rpoblems with
the correspondence proof). However, since they do not fit with the design
rationale of OWL Full (as I understand it) they make OWL Full harder to use
(no clear design rationale as to when iff and when if-then in the semantics).

1) finite set examples

The current semantics does not support intuitive entailments, (while I never
liked this, it is a design goal of the OWL semantics as I understand it)

<owl:Class rdf:about="#colors">
  <owl:oneOf rdf:parseType="Collection">
   <owl:Thing rdf:about="#red"/>
   <owl:Thing rdf:about="#green"/>
   <owl:Thing rdf:about="#blue"/>
  </owl:oneOf>
</owl:Class>


currently neither (OWL Full) entails not is entailed by:

<owl:Class rdf:about="#colors">
  <owl:unionOf rdf:parseType="Collection">
    <owl:Class>
     <owl:oneOf rdf:parseType="Collection">
        <owl:Thing rdf:about="#red"/>
        <owl:Thing rdf:about="#green"/>
     </owl:oneOf>
    </owl:Class>
    <owl:Class>
     <owl:oneOf rdf:parseType="Collection">
        <owl:Thing rdf:about="#blue"/>
     </owl:oneOf>
    </owl:Class>
  </owl:unionOf>
</owl:Class>


2: singleton unionOf's intersectionOf's.

I would expect

<owl:Class rdf:about="#c" >

to entail

<owl:Class rdf:about="#c">
   <owl:intersectionOf rdf:parseType="Collection">
     <owl:Class rdf:about="#c"/>
   </owl:intersectionOf>
</owl:Class>

etc ..
Currently this is an OWL DL entailment and an OWL Full non-entailment.

3: owl:complentOf should be symmetric.

I would expect

owl:complementOf rdf:type owl:SymmetricProperty .

to be ttrue in OWL Full i.e.

<owl:Class rdf:about="#c">
  <owl:complementOf>
    <owl:Class rdfabout="#notC" />
  </owl:complementOf>
</owl:Class>

should entail

<owl:Class rdf:about="#notC">
  <owl:complementOf>
    <owl:Class rdfabout="#c" />
  </owl:complementOf>
</owl:Class>


Note on B1 B2 proof.
=================

I believe that such a change makes the B1 B2 proof easier, and I would
 suggest that the WG is less dependent upon Peter to produce it. (i.e. I
 believe that Herman, Pat or myself, for example, with this change to OWL
 Full semantics, given the proof without B1 B2, could prove the B1 B2 result,
 with say a day's work [Herman and Pat, less than a day :) ]) I think this
 proof could be done with a first line: "given the theorem when all
 descriptions map to distinct blank nodes" so that the two tasks can be done
 in parallel [updating the correspondence proof with the change in OWL Full
 semantics and the B1 B2 step]

I dare to say that the reason the B1 B2 proof seemed so difficult is that the
result was untrue, because of this bug.

Either fix 1/ or 2/ results in a system where the only possible triples in
which a bnode representing a description or restriction appears as object is
one with iff semantics based on the class extension (made a little more
complicated with the lists in owl:unionOf and owl:intersectionOf) That seems
to be enough to permit an inductive argument ...

-------------------------------------------------------

Received on Sunday, 11 May 2003 17:54:05 UTC