- From: Jeremy Carroll <jjc@hpl.hp.com>
- Date: Sun, 11 May 2003 23:54:19 +0300
- To: www-archive@w3.org
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