My ACTION-64 (to propose closing ISSUE-29)

Ok, I'm extra confused and I think I get to blame the chair :)  
(Sorry, Alan.)

In the telecon, I was asked to be the champion on this on the basis  
of it being "my issue". But it's not. I am the raiser of record  
because I migrated it from the google code issues list. I'm not up to  
speed on this issue either.

If you look at ISSUE-29,
	http://www.w3.org/2007/OWL/tracker/issues/29
	
Peter and Jeremy have been way active on it, but there still seem to  
be some controversy.

Peter proposed a resolution:
	http://lists.w3.org/Archives/Public/public-owl-wg/2008Jan/0017.html

But I don't understand how it disposes of ISSUE-29.

Hmm. Ok, we have owl:DataRange already...oh, I have trouble bringing  
myself to care :) It looks to me like it doesn't matter because their  
semantic conditions (in the RDFS style model theory) are similar  
(subsets, not necessarily disjoint) of LV_i). And this is basically  
Peter's point 4 (though I don't understand the OWL Full  
restriction...I guess it doesn't matter).

Sigh. This feels like another minor syntax issue made complex by  
forcing reflective semantics upon us.

I'm guessing, but only guessing, that Holger wants the rdf mapping to  
use rdfs:Datatype where it currently uses owl:DataRange (I don't take  
the talk of "modeling" seriously because I don't believe he...or  
anyone...is being sensitive to the subtle potential semantic issues.  
If I'm wrong, please let me know.) I guess we could do that and only  
with dataOneOf *also* add the owl:DataRange triple for backward  
compatibility (if anyone ever used it).

I guess it's back in Jeremy's court qua keeper of the OWL Full  
semantic flame. Whatever solution *has* to not force owl:Thing to be  
always infinite[1] (e.g., by, in non-Full cases, allowing Literals  
and owl:Thing to be disjoint). I guess I don't know if that's likely  
or possible, but these are murky waters to me.

Cheers,
Bijan.

[1] I'd like to make clear why this is a hard requirement, since I've  
heard people express hope that owl:Thing could be made always  
infinite and that the standard obvious counterexample owl:Thing  
subclass of [oneOf (:a)] wasn't a "real" use case (and stronger  
claims that it was silly, wrong headed or semantic weird).

The problem is *much* deeper than that. If we force owl:Thing to be  
infinite (a la OWL Full), then there are no finite models for the  
ontology. In SHOIN/SROIQ it's perfectly possible for an ontology to  
have only finite models (or only infinite models, or a mix of the  
two) (they don't have the finite model property).

So, three cases for SROIQ ontologies:
	OF -> only finite models
	OFI -> both
	OI -> only infinite models

Making owl:Thing infinite would require reasoners to determine  
whether an arbitrary ontology O' was in OF (so it could call them  
inconsistent).

However, all existing reasoners (and known procedures) do NOT KNOW,  
in general, which category O' falls into when they test it for  
consistency. Tableau reasoner build a structure which, if clash free,  
describes sets of models without distinguishing whether they are  
necessarily finite or necessarily infinite. In order to add this  
check we would have to do *finite satisfiability testing* which has  
never been implementing, looks really hard, no known optimizations,  
etc. etc. We'd be starting over from scratch. So, hopeless.

So even if one wanted to bite the semantic bullet (as shown in  
<http://lists.w3.org/Archives/Public/public-owl-wg/2007Dec/ 
0227.html>), it's very hard to see how putting an implementation  
burden that would be worse (in terms of available knowledge and  
likely effort) of writing an OWL 1.1 reasoner *from scratch* is a  
starter :)

Uli and I worked this out the other day and I was horrified by the  
realization. So I had to share!

Sorry for the emailorrehia.

Received on Thursday, 10 January 2008 02:12:22 UTC