Re: Abstract Syntax and Semantics: review comments / Correspondence between OWL DL and OWL Full

Peter Patel-Schneider wrote on 20 Dec:

> From: herman.ter.horst@philips.com
> Subject: Abstract Syntax and Semantics: review comments
> Date: Fri, 20 Dec 2002 16:47:18 +0100
> 
> > Abstract Syntax and Semantics: 
> > review comments about version of 19 December

> [...]

> > - Correspondence between OWL DL entailment and OWL Full entailment.
> > The Bristol consensus on semantics already expressed the need for a 
> > characterization of the situation that DL and Full (in those days, 
fast
> > and large) entailment coincide [2].  There is now an informative 
appendix
> > with a brief sketch in this direction.
> > I do not understand how the theorem given there follows from the 
lemma.
> > It does not seem to follow from the statement of the lemma alone: if I 
is 
> > an
> > OWL Full interpretation that satisfies K, then it needs to be proved 
that
> > I satisfies C.  Getting another OWL DL interpretation I' that 
> > satisfies K, shows that I' satisfies C.  And then?
> > 
> > Until we can really view the lemma and the theorem and its converse 
> > as proved, we do not really know about the correspondence between 
> > OWL DL entailment and OWL Full entailment.
> 
> The theorem follows from the proof of the lemma, namely that the mapping
> between OWL-interpretations and OWL/DL-interpretations is uniform for a
> given separated vocabulary.  I will strengthen the statement of the 
lemma
> accordingly.

I looked at the new version in the Semantics document draft of 
31 December, and agree that the theorem in Appendix A.2 follows formally 
from the new statement of the lemma.

I looked further at this appendix.
I believe that Appendix A.2 is too short (about half a page) to do 
justice to the importance of its subject: Correspondence between 
OWL DL and OWL Full.  This appendix should contain the technical 
basis underlying, for example, the important claim underlying OWL
which appears early in the Guide document:
"Every valid OWL DL conclusion is a valid OWL Full conclusion."

The lemma already mentioned forms the main basis for the implication
DL entailment => Full entailment.
Unfortunately, the proof of this lemma is labeled as a "proof sketch", 
unlike the proofs in Appendix A.  The proof of this lemma refers to the
proofs in Appendix A.1, which I have not yet been able to review.

I noticed that it is not clear from the text whether the lemma is 
considered to be really proved, in view of the sentences that 
introduce Appendix A.2:

>  "This section contains a poof [by the way, a typo] sketch concerning 
>  the relationship between OWL/DL and OWL/Full. This proof has not been 
>  fully worked out.  Significant effort may be required to finish the 
proof 
>  and some details of the relationship may have to change."

It should be made explicit in the document whether the lemma in Appendix 
A.2
is considered to be (true and) completely proved;
- if it is, then the proof sketch should in my view be upgraded to a full
proof, as is done consistently in Appendix A.1.
- if it is not, then the document has a serious gap, in view of the claim
made in the Guide document.

The document does state explicitly that the converse of the theorem is 
open.
That is, it is unknown whether, within the syntactic constraints of OWL 
DL,
OWL Full entailment implies OWL DL entailment.

Herman ter Horst
Philips Research

[...]