- From: Sandro Hawke <sandro@w3.org>
- Date: Tue, 02 Sep 2008 09:57:25 -0400
- To: "Michael Schneider" <schneid@fzi.de>
- cc: "Ian Horrocks" <ian.horrocks@comlab.ox.ac.uk>, "W3C OWL Working Group" <public-owl-wg@w3.org>
> * 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