[FULL] ISSUE-119: the other approach

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