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

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.

- 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:14:32 UTC