W3C home > Mailing lists > Public > public-owl-wg@w3.org > May 2008

Re: [FULL] ISSUE-119: the other approach

From: Ian Horrocks <ian.horrocks@comlab.ox.ac.uk>
Date: Mon, 19 May 2008 19:14:02 +0100
Message-Id: <7D95E8DE-292C-4761-B1AE-A0E4319FECBA@comlab.ox.ac.uk>
Cc: "Web Ontology Language ((OWL)) Working Group WG" <public-owl-wg@w3.org>, Jeremy Carroll <jjc@hpl.hp.com>
To: Michael Schneider <schneid@fzi.de>

I talked to Peter about this and we agreed that Jeremy's proposal  
looks promising.

I would like to hear from Michael as to what he thinks about this  
proposal.

Ian


On 28 Apr 2008, at 16:55, Jeremy Carroll wrote:

>
> 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, 19 May 2008 18:14:51 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 19 May 2008 18:14:53 GMT