- From: Jeremy Carroll <jjc@hpl.hp.com>
- Date: Mon, 28 Apr 2008 16:55:07 +0100
- To: "Web Ontology Language ((OWL)) Working Group WG" <public-owl-wg@w3.org>
We have discussed a different approach to comprehension, which was perhaps poorly branded as 'solipistic' .... Peter and others have described this as a big change; the point of this message is to argue to the contrary that it is small - both in the amount of text of the spec that changes, and in the amount of code that changes as a result. In fact, I suggest that 0-lines of code change. Hence, this would be a backward compatible change. ===== Current state OWL1: + Comprehension principles + Theorem 2 These give a weak alignment of DL entailment and Full entailment Full reasoners (such as Jena Rules) partially implement this, by in some circumstances introducing terms that match the constructs in the comprehension principles. Possible alternative: Comprehension principles remain, not as model theoretic principles, but as reasoning principles. Theorem 2 is modified from approx: If A DL-entails B where A and B are in the syntactic subset then A Full-entails B. To approx. If A DL-entails B where A and B are in the syntactic subset then B = B' & B'' where B'' is a conjunct of terms matching comprehension principles and A & B'' Full-entails B ===== This modifies the comprehension principles from being model-theoretic statements, to play a role in theorem 2 that speaks more to the proof-theory. Since OWL Full implementations implement rules (i.e. proofs) this proof-theoretic variant of comprehension is closer to what the implementations already do, and there is no backward compatibility problem. (Backward compatibility is about OWL implementations and OWL documents, not about OWL specifications). Also, the textual change to the spec is slight - the comprehension principles remain - but their role in the OWL Full semantics is modified. Jeremy
Received on Monday, 28 April 2008 15:56:56 UTC