Re: Proposal to close ISSUE-73 (was Re: My ACTION-64 (to propose closing ISSUE-29))

On 14 Jan 2008, at 12:51, Jeremy Carroll wrote:

>
> I was a little surprised when an action to propose closing one  
> issue, result in a proposal to close another issue which has had  
> very little discussion.
>
> I do not find Bijan's message as compelling on the main points  
> which are:
>
> - the Web context is not one that can be given a finite bound. Any  
> ontology that tries to do so is limiting its interoperability with  
> other ontologies.
>

Just a remark: we should distinguish between

a) giving things a finite bound "a priori", e.g., saying that there  
are atmost 30,000 elements in an interpretation domain, and

b) requiring that something is finite, but not fixing a bound.

In my understanding, the web is always finite (since there are, at  
all times, only finitely many computers with finite memory), but I  
wouldn't try to give it an a priori bound.

Cheers, Uli

> - OWL Full compatibility; while I would agree that OWL Full is  
> necessarily infinite largely due to technical accidents rather than  
> design, the Web context argument was always seen as one that made  
> this a happy accident rather than a mistake.
>
> I hope we can have adequate discussion before voting on this one.
>
> Jeremy
>
>
> Bijan Parsia wrote:
>> I propose closing ISSUE-73 by rejecting the proposal.
>> First I must backtrack from the conclusions in:
>>     <http://www.w3.org/mid/35A1BE3A-54A9-4D53- 
>> A7A2-543EA2891B35@cs.man.ac.uk> Uli and I had a brain fart. We  
>> don't need to rule out all the finite models, we just need to show  
>> that there is an infinite model. *If you have a SHIF reasoner*,  
>> you can, in principle, implement this *I THINK* by source  
>> preprocessing and an existing OWL reasoner. You can always check  
>> whether an ontology has a infinite model by adding a fresh class  
>> (using only fresh vocabulary) which is only infinitely  
>> interpretable. You can make it inconsistent by making a fresh  
>> individual a member of that class. You can  examples of such  
>> classes in various places:
>>     http://lists.w3.org/Archives/Public/public-owl-dev/2007AprJun/ 
>> 0129.html
>>     http://lists.w3.org/Archives/Public/public-owl-dev/2007AprJun/ 
>> 0130.html
>>     http://lists.w3.org/Archives/Public/public-owl-dev/2007AprJun/ 
>> 0131.html
>>     http://lists.w3.org/Archives/Public/public-owl-dev/2007AprJun/ 
>> 0133.html
>> Note that Uli, Peter, and I were several times over the past  
>> couple of days confused by this. Maybe we're stupid, but it was a  
>> strange way to have to think. I've personally spend far far too  
>> many hours on this. I think that's prima facie evidence that this  
>> is not a trivial move. Thus it requires pretty extra-ordinary  
>> justification.
>> Note that you only need this for ontologies in logics that lack  
>> the infinite model property (i.e., that if they have a model, then  
>> they have an infinite model). ALC has the infinite model property.  
>> I think only logics with nominals (and sufficient other resources  
>> to constraint the domain) lack the infinite model property.
>> However, it's very unclear what the impact on performance will be  
>> in those ontologies (aside from making some inconsistent).
>> I strongly object to this proposal. The only given motivation is  
>> ideological: To align the semantics of OWL 1.1 with OWL Full.  
>> While the implementation of satsfiability "looks" ok, it's not  
>> clear that it will turn out to be ok (the raiser, Jeremy, has done  
>> no work, afaik, to check this; the fragments he implements have  
>> the infinite model property). Furthermore, it's *very* much  
>> unclear how this will affect the wide array of new and interesting  
>> services being worked on (e.g., approximate module extraction).
>> There was a modeling argument against finiteable owl:Thing, e.g.,:
>> Jim claimed that he didn't know of any use cases in "real"  
>> applications:
>>     http://www.w3.org/mid/50F0B246-12F4-4CDF-9FF4-DD31A0F0C223% 
>> 2540cs.rpi.edu including:
>>     "I note  that  some of the border cases for other issues come  
>> when the  extension of owl:thing is finite"
>> but there is no listing of how the border cases work or even what  
>> they are.
>>  And Jeremy:
>>     """From a modelling point of view, any model with a finite  
>> domain of discourse, would model that domain as a subclass of  
>> owl:Thing; and the domain owl:Thing would be reserved as  
>> everything in a Web context, for which it is difficult to give a  
>> finite bound."""
>> One obvious real use is for domain closure when modeling database  
>> or other systems where you want CWA in various forms. Even if you  
>> are working with a subclass of thing, the system may infer that it  
>> is equivalent to Thing and that might have been what you were  
>> looking for.
>> As for the "Web context" argument, I don't understand why, even if  
>> it were true that it is "difficult to give a finite bound" in such  
>> a context (but really, we need more detail about the Web Context  
>> and why it imposes this difficulty -- or whether it imposes an  
>> impossibility!), we aren't defining an *ontology of the Web*, but  
>> a *language for writing Ontologies which are shared on the Web*.  
>> Surely we can all *imagine* finite universes? Even imagine finite  
>> universes of size 1, or size 2? Why should we forbid people from  
>> describing such universes with their ontologies? Note that, in  
>> this case, OWL DL is *more expressive* than OWL Full because it  
>> allows people to describe, directly, both finite and infinite  
>> universes.
>> Finally, what is the *use case* for requiring infinite universes  
>> (thus making OWL *very* non standard from a first order logic  
>> perspective)? Actually, I've not heard anyone advocating this give  
>> one. The reason that owl:Thing in OWL Full is necessarily infinite  
>> is a *purely technical trick*. There was never an argument that we  
>> had to make owl:Thing infinite because...er...the Web was  
>> infinite. (That was a post facto rationale.) It's *just* a  
>> technical trick. It is a trick related to a very technically  
>> dubious feature of OWL Full: syntax reflection, which is known to  
>> be very semantically dangerous (that is, it risks Russell's  
>> paradox as theorem) and has strong implementation consequences in  
>> weaker cases (e.g., it makes *ALC* undecidable). And no actual  
>> users (under that semantics; syntax punning, now, that's a bit  
>> different.)
>> While I know lots of people who finitely size the universe (if  
>> just for fun; though, as I said, I do seriously use), I don't know  
>> of anyone who forces infinite models. I don't know what you would  
>> use that *for*? (It *doesn't* help impose a CWA.) If anyone needs  
>> infinite model reasoning for their application, then can import  
>> the following ontology:
>>     http://www.cs.man.ac.uk/~bparsia/owl/examples/make-thing- 
>> infinite.owl
>> The absence of general knowledge of this trick suggests that  
>> people do not generally require only infinite universes for their  
>> work with OWL.
>> Thus, we should close this issue rejecting the request.
>> Cheers,
>> Bijan.
>
>

Received on Monday, 14 January 2008 13:55:05 UTC