RE: ACTION-210: Review on "Conformance" section

Hello again!

Here is one additional point concerning entailment checkers, and the result
values "False" and "Unknown".
 
In general, all entailment checkers must say "False" only if entailment does
not hold, and I perfectly agree with this. So if an entailment checker
cannot tell for sure that some entailment does /not/ hold, it has to return
"Unknown" in order to avoid getting non-conformant.

For those RL-checkers, which only use the RL-RDF-rules, it seems to me that
it is virtually impossible to ever find out for sure that some entailment
does /not/ hold. Even if we restrict our discussion to those "simple" cases
which are covered by Theorem 1 in the profiles document, it keeps difficult:
For those cases, O1 does /not/ entail O2, iff there does not exist any
sequence of rule applications which leads from O1 to O2. But how can a
triple-rule-based RL-reasoner find out that there is no such sequence?
 
OWL 2 Full entailment checkers have better options, but in general they
won't be able to say "False" in every case, either.

Generally, I wonder why we discourage the result "Unknown" at all ("an
entailment checker SHOULD NOT return Unknown"). Isn't this a perfectly
legitimate result? Those entailment checkers, which really never say
"Unknown", may call themselves "complete", or even "complete and
terminating", which are additional quality predicates.

So my suggestion is: Drop the "SHOULD NOT" sentence from all conformance
classes, and also the "MAY" sentence from the RL conformance class (the
latter doesn't provide very helpful information, IMO). 


Regards,
Michael

>-----Original Message-----
>From: Michael Schneider
>Sent: Sunday, September 21, 2008 1:44 PM
>To: public-owl-wg@w3.org
>Subject: ACTION-210: Review on "Conformance" section
>
>Dear all,
>
>this mail is to fulfill my ACTION-210 (related to ISSUE-130) on
>reviewing the "Conformance" section based on version
>
>
><http://www.w3.org/2007/OWL/wiki/index.php?title=Conformance&oldid=12922
>>
>
>However, there are still a few points which I like to check in more
>depth later this day. So it may happen that I come up with a second mail
>tomorrow.
>
>
>* Start of sec. 1
>  """
>  This section uses the words
>  MUST, MUST NOT, SHOULD and MAY
>  as in [RFC 2119].
>  """
>
>We now have some standard text used in many of our documents (e.g. in
>sec. 1.1 of the Syntax). This should be used here, too, I think.
>
>Afterwards, everywhere in the text the rendering of the occurrences of
>these keywords have to be changed, accordingly.
>
>* 1.1.1: Syntactic Conformance
>  """
>  Any RDF document [RDF Syntax] is an OWL 2 Full ontology document.
>  [...]
>  An OWL 2 Full ontology document is an OWL 2 DL ontology document iff
>[...]
>  """
>
>What is with non-RDF documents, such as documents in Functional Syntax
>or OWL/XML? These are not treated by the definition of "syntactical
>conformance".
>
>* 1.1.2: Semantic Conformance
>  """
>  In OWL 2, semantic conditions are defined
>  with respect to a datatype map [OWL 2 Specification].
>  This MUST be either the OWL 2 Datatype map [OWL 2 Specification]
>  or an extension of the OWL 2 Datatype map
>  to include additional datatypes.
>  """
>
>The headline "semantic conformance" seems a bit broad to me, given that
>the requirements stated in this section are restricted to datatype maps.
>
>Further, there are certain restrictions on the datatype map at least for
>OWL 2 RL, see
>
>  <http://www.w3.org/2007/OWL/wiki/Fragments_Proposal#Entities_3>
>
>  "The following predefined OWL 2 datatypes
>  MUST NOT be used in OWL 2 RL: ..."
>
>This sounds to me as if an OWL 2 RL reasoner cannot be semantically
>conformant!?
>
>* 1.2.1: Entailment Checker
>  """
>  An OWL 2 entailment checker takes as input two
>  OWL 2 ontology documents [...]
>  """
>
>The term "OWL 2 ontology document" is undefined. It should perhaps be
>said that this is some kind of "collective term" for those terms defined
>in the "syntactic conformance" section.
>
>* 1.2.1 Entailment Checker
>  """
>  Five different conformance classes of
>  OWL entailment checker are defined
>  """
>
>Should be: "OWL /2/ entailment checker/s/".
>
>(I guess this was in to check the reviewers? ;-))
>
>* 1.2.1 Entailment Checker, Conformance Classes
>
>Just as a note (probably no action needed): All five entailment checker
>classes now allow for trivial checkers which never terminate or which
>always return "UNKNOWN" (in spite of the explicit "SHOULD NOT"). That's
>sort of strange, but maybe there is no way to deal with this situation
>in a meaningful way.
>
>Regards,
>Michael

--
Dipl.-Inform. Michael Schneider
FZI Forschungszentrum Informatik Karlsruhe
Abtl. Information Process Engineering (IPE)
Tel  : +49-721-9654-726
Fax  : +49-721-9654-727
Email: Michael.Schneider@fzi.de
Web  : http://www.fzi.de/ipe/eng/mitarbeiter.php?id=555

FZI Forschungszentrum Informatik an der Universität Karlsruhe
Haid-und-Neu-Str. 10-14, D-76131 Karlsruhe
Tel.: +49-721-9654-0, Fax: +49-721-9654-959
Stiftung des bürgerlichen Rechts
Az: 14-0563.1 Regierungspräsidium Karlsruhe
Vorstand: Rüdiger Dillmann, Michael Flor, Jivka Ovtcharova, Rudi Studer
Vorsitzender des Kuratoriums: Ministerialdirigent Günther Leßnerkraus