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

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 Thursday, 10 January 2008 21:22:53 UTC