ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] Ontologies vs Theories / Axioms vs Rules

To: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Ali SH <asaegyn+out@xxxxxxxxx>
Date: Thu, 20 Oct 2011 21:57:05 -0400
Message-id: <CADr70E0Avn0B72tHXawxqRUVkiEcgq2LJ225F16tgginZqf94A@xxxxxxxxxxxxxx>
On Thu, Oct 20, 2011 at 4:08 PM, Bijan Parsia <bparsia@xxxxxxxxxxxx> wrote:
[BP] If so, then it probably doesn't need the extra expressivity. In expressive logics, size is less important than complexity. Euclid's Theorems don't make for a *large* KB, but good luck writing a reasoner that can return the rest of the Elements :)

[AH] Ummmm, not quite.
[BP] Actually quite.

Hmmmm, sorry, not so quite. ;)

I think though that we're talking at cross purposes. By fragment, I meant that which is given by definition 13 in http://stl.mie.utoronto.ca/publications/colore-fois.pdf

Namely (though see the paper for proper formatting and symbols): 

Definition (13 in paper)
A class of structures M is reducible to the classes of structures N1, ..., Nn
iff there is a set of surjections Pi : M \rightarrow Ni such that if M \in M and M = M1 U ... U Mn
then Mi is weakly definable in Pi(Mi) and Pi(Mi) is weakly definable in Mi

which leads to the theorem:

Theorem (6 in paper)
Let T be a theory and let T1, ... , Tn be a set of modules in the repository.

Mod(T ) is reducible to Mod(T1),..., Mod(Tn) iff
  •  T faithfully interprets each theory Ti , and   
  • T1 U ... U Tn is definably equivalent to a subtheory T* \subset T such that
Mod(T ) \subset Mod(T')

... Basically, see section 3.4 in that paper for a proper treatment of what I meant by fragment. It is in this sense that T* is a fragment of T.
[AH] There are many applications where you might have captured the domain in an expressive ontology, and have ensured consistency (perhaps off-line)
[BP] I would like to know how they've done that, if the ontology is truly using a high level of expressivity and is reasonably large. "Off line" doesn't work if the reasoning problem takes a billion years.

 If it can then be factored (without approximation) into tractable fragments, I'll be pretty surprised or bet that the modelling doesn't really exploit the expressivity.

Sure, imagine an ontology that is a union of modules for a subclass taxonomy, time and geo-spatial components. The theory that combined all these modules requires at least first order expressivity to capture intuitions about the domain. It is tractable, but answers take on the order 3-20 minutes to return based on a kb and a general purpose FOL reasoner. However, properties of each of the modules are also known, and they each have a dedicated reasoners just in case the system receives a query involving vocabulary singularly to do with one of the sub-modules. For example, if a query involves language only drawn from the taxonomic sub-module, then the FOL reasoner need not be called, and instead something optimized for traversing trees might be invoked. Alternatively, if a query involved solely geospatial terms, then perhaps no reasoner would actually be called, but the query would be computed algebraically.

It is my (perhaps faulty) understanding that the Cyc system does something broadly similar to this.

For another example, consider the PSL-core ontology which is reducible to simpler theories, and these more simple models can be used to construct models of the PSL-core ontology (section 3.5 of the paper referenced above).

[AH] So for example, for real-time interactions of a subset of that ontology, you deploy fragments of it.  
[BP As I said, size doesn't necessarily determine difficulty of reasoning in expressive logics. This is just a brute mathematical fact (EXPTIME logics have relatively small theories that take, well, an infeasibly long time to reason with).

Thanks, I know this, and I haven't been talking about size... 

[BP]Indeed, I've encountered OWL ontologies which have fragments which are *harder* to reasoner over than the whole ontology! (Typically because the reasoner can exploit information in the whole which prunes the search space).

...

Right, so the problem of tractability is part of the domain moreso than an inherent part of a representation language. FOL for all its semi-decidability might still be quite tractable and fast, and OWL for all its decidability might take a super long time... It's more to do with what you're modelling than your language.B ut this is beside the point here. The rest of your response continues to assume that I'm simply talking about "size" which is certainly not the case.
 
[BP] Ok. I don't care at all about OOR.

Funny that you're on the OOR mailing list then :P.

Ah sure, you mean standard notions such as conservative extension. Well, CE for sure will be nasty (undecidable) for OWL alone, so detecting such relations is probably unlikely in the near future. If you have an approximation algorithm, however, you might be able to put some guarantees on the output. And in the OWL world we've worked on various approximations of CE related notions (cf locality based modules).

Though in contrast with most DL research, we've focused more on flavours of non-conservative extensions. I'll see if there is a pre-print version of an upcoming Applied Ontology paper, though there's a very preliminary sketch of such a procedure for generating reducibility between (i.e. factoring) ontologies in Chapter 5 of https://tspace.library.utoronto.ca/bitstream/1807/17512/1/Hashemi_Ali_200906_MASc_thesis.pdf. I should reiterate that it has been *significantly* updated in the more recent paper, and I will link the pre-print once it is available.

Cheers,
Ali 

_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J    (01)

<Prev in Thread] Current Thread [Next in Thread>