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

Bijan-
  unclear to me CWA is really a use case, as i still don't see a  
mechanism where it can be used with an owl reasoner (i.e. I don't see  
finite universes solving what you used to call the Decker paradox),  
but that said, I don't feel strongly about this - far as I can tell,  
it will have very little impact on any communities I feel I  
represent, so barring arguments I haven't yet heard, I would happily  
abstain on the closing of this one
  -JH


On Jan 10, 2008, at 4:24 PM, 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.
>

"If we knew what we were doing, it wouldn't be called research, would  
it?." - Albert Einstein

Prof James Hendler				http://www.cs.rpi.edu/~hendler
Tetherless World Constellation Chair
Computer Science Dept
Rensselaer Polytechnic Institute, Troy NY 12180