Re: ISSUE-130 / ACTION-194 Come up with a proposal for conformance

> * 1.2.1 Analog for "OWL 2 RL entailment checker". But my question is:
> Should it be "OWL 2 /Full/ ontology documents" or "OWL 2 /RL/ ontology
> documents"?
> 
> * 1.2.1
> 
>   """
>   An OWL 2 RL entailment checker
>   [...] MUST return True only when O1 entails O2,
>   and it must return False
>   only when FO(O1) <union> R does not entail FO(O2)
>   under the standard first-order semantics
>   """
> 
> Just to be clear: This means that there can be two conformant OWL 2 RL
> entailment checkers C1 and C2, where for the same query "G_L |= G_R
> ?"  C1 answers "False" (because G_R does not follow from G_L via the
> rules), while C2 answers "True" (because G_R follows from G_L via the
> Full semantics).  I suggest that we state it explictly that this is
> intended. Otherwise people might get confused and think that this is
> a bug.

Oh, that's the clever bit I didn't really think through in the
definition.  I think I get it now.  It's slightly worse than you stated:
we don't need a C2; C1 could use a random number generator to determine
whether to return True or False and it would still be conformant.

We could add this explanitory text:

    Note that conformance is not constrained (results True and False are
    each allowable) in situations where the RL ruleset does not fully
    express the RDF-Based semantics (formally, where O1 entails O2 but
    FO(O1) <union> R does not entail FO(O2)).  This lack-of-constraint
    allows implementors to extend the given rules, adding additional
    (sound) rules, while still having a conformant OWL 2 RL entailment
    checker.  The cost of this freedom is a lack of standardization;
    users cannot rely on the results of RL entailment checkers in these
    situations without getting implementation-specific guidance.

As a user, I don't like this very much.  I'd like to at least be told
whether additional rules were used, and maybe be given the option of
controlling whether they are.

Here's one way I could be told.  This would work whether or not I can
also control the additional reasoning methods/rulesets (the "+" option).

 case 1  FO(O1) <union> R entails FO(O2)
         (which implies O1 entails O2)
         it MAY return "True RL", meaning the entailment is shown by the
         base RL ruleset

 case 2  If O1 entails O2 and 
         FO(O1) <union> R does not entail FO(O2)
         it MAY return "True RL+", meaning that while the entailment is
         not shown by the base RL ruleset, it is still (somehow) known
         to hold 

 case 3  If FO(O1) <union> R does not entail FO(O2)
         it MAY return "False RL", meaning the entailment is not supported by
         the base RL ruleset (but may, in fact, still hold).

 case 4  If FO(O1) <union> R <union> R2 does not entail FO(O2), for some
         R2, it MAY return "False RL+", meaning the entailment is not
         supported by the base RL ruleset, even with some extension.
         (The entailment may, in fact, still hold.)

 case 5  If O1 does not entail O2
         it MAY return "False", meaning the entailment is known not to
         hold.

       Note that whenever "True RL+" is a valid response, "False RL" is
       also a valid response.  It is less helpful, though, and "True
       RL+" SHOULD be returned in these cases, if the entailment is
       known to hold.

(I'm trying to think of better terms for "False RL" and "False RL+".
More accurate and less misleading than false would be "Unprovable" or
"Unsupported", I think.   I guess, myself, I'd go with case 3 and 4
being "Unprovable RL" and "Unprovable RL+".)

I think I would also allow additional characters after the "+" for
implementation-specific purposes, so they can indicate which additional
R2 ruleset was used, like "True RL+RDFS".

       -- Sandro

Received on Tuesday, 2 September 2008 13:58:57 UTC