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

On 2 Sep 2008, at 14:57, Sandro Hawke wrote:

>
>> * 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.

This is slightly misleading. Conformant reasoners may return True  
*only* when the entailment is valid according the the RDF-based  
semantics. So, C1 may only use a random number generator when it  
knows the correct answer is true, but that this wouldn't be computed  
by the RL/RDF rule set. Deciding to return a random answer in this  
case seems at best obtuse. Moreover, because of the above mentioned  
condition on conformant reasoners, if a conformant reasoner ever says  
"True" then I know that this is the correct answer -- so if two  
conformant reasoners (or the same one) ever disagree, I know that the  
correct answer is True.

It is also worth emphasising that this situation only arises w.r.t.  
valid OWL Full entailments that are not detected by the OWL RL/RDF  
rules. This case can be syntactically detected, and implementations  
MAY issue a warning.


>
> 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.

We could say this or something like it.

>
> 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.

Implementations may choose to provide a "strict" (minimal?) mode in  
which only the RL/RDF rules are used. I'm not sure if we could or  
should insist on this. If we wanted to be more strict w.r.t.  
conformance, we could strengthen the statement about warning users  
when they are asking questions that the implementation may not be  
able to answer correctly, i.e., state that they SHOULD or MUST issue  
such a warning.

>
> 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

I don't think we need to distinguish shades of truth, because  
conforming implementations can return True *only* when the entailment  
holds.

>
>  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".

This all sounds terribly complicated. If you really wanted to be  
"perfect", then you could have "Don't Know" as a possible answer, and  
insist that False is returned only when the entailment really doesn't  
hold. In view of what I explained above, however, I'm not sure that  
any of this is necessary -- users are, after all, free to treat False  
as Don't Know when the completeness guarantee can't be made.

Ian



>
>        -- Sandro

Received on Tuesday, 2 September 2008 17:45:19 UTC