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

Hello,

I would like to second Bijan's observations and present further arguments why prohibiting finite models might be a bad idea.

We are currently experimenting with novel reasoning techniques for OWL (1.1) DL that are based on the fact that most OWL DL
ontologies actually can be satisfied in a finite model. Namely, we observed that the axioms that rule out finite models are usually
quite strange and rarely occur in knowledge bases; hence, we are currently trying to exploit this in the reasoning calculus in order
to gain efficiency. I can't yet point to hard and fast evidence that our techniques will work and be beneficial; however, I have
some very encouraging preliminary results and I hope to write a paper about it in not so distant future (a couple of months).

To summarize, I believe that allowing the interpretation domain to be finite is beneficial for at least two reasons. First,
finiteness of the domain is natural: most things that people model are finite. Second, even if our technique turns out not to work,
I am confident finiteness of the domain can be exploited to improve efficiency of reasoning.

Thus, I strongly advocate leaving the semantics of OWL 1.1 DL as it is.

Regards,

	Boris


> -----Original Message-----
> From: public-owl-wg-request@w3.org [mailto:public-owl-wg-request@w3.org] On Behalf Of Bijan Parsia
> Sent: 10 January 2008 21:25
> To: Web Ontology Language ((OWL)) Working Group WG
> Subject: 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 Friday, 11 January 2008 10:16:48 UTC