On 20 Oct 2011, at 19:43, Ali SH wrote:
Dear Bijan,
[AH] I would hope that with the current work under way by the Bremen group (HeTS) and the Toronto group (COLORE), a CL ontology could be factored into more tractable fragments.
[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 :)
Ummmm, not quite.
Actually quite.
There are many applications where you might have captured the domain in an expressive ontology, and have ensured consistency (perhaps off-line)
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.
and are using that ontology to drive the development of software or other services.
Of course, exactly how they are doing that makes a difference.
So for example, for real-time interactions of a subset of that ontology, you deploy fragments of it.
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).
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).
Again, in expressive logics (really, anything with a non-polynomial reasoning problem), there's no simple relation between size and time to process.
Try googling "Ontology Driven Software Engineering".
As I've written papers on ODSE, I'm not feeling a strong need to google, thanks.
It's also irrelevant to the question at hand. Why people are doing something is a bit orthogonal to what they are actually doing. And frankly, what they *think* they are doing may not be what they *are* doing. If you have a concrete example which shows your point I'd be happy to look at it.
The point is that "Oh, I'll make my theory smaller and it will be (more) tractable" does not straightforwardedly hold for expressive logics. If you *can* separate it into less expressive fragments (while preserving all entailments) then you likely aren't really using the expressivity of the union. For example:
Let O1 be an ontology in SHIQ and O2 be an ontology in SHOQ with disjoint signatures and with O2 not sizing the domain (e.g., to being finite). Then, O1 union O2 will be in SHOIQ, which is NEXPTIME complete for satisfiability (whereas SHIQ and SHOQ are both EXPTIME). And look, I can factor that union back into O1 and O2. But obviously, there was no real interaction between the inverses, nominals, and counting quantifiers. Thus, though the union was "using" a more expressive logic, it wasn't using that expressivity to *model* anything.
Of course, many subsets of an ontology will be very easy to reason with. Assuming short, singularly inexpressive axioms, every singleton subset will be easy peasy.
[AH] Of course, not to mention a number of CL reasoners currently under development
[BP] Such as? First order theorem proving is pretty hard and existing ones are pretty good. None that I know of are targeting CL per se or ontologies, really.
There have been mentions of at least 3 efforts on the Common Logic mailing list. Off the top of my head, I believe there is a group working with Fabian Neuhaus, another with Tara Athan, and another with Randall Schulz.
I'm not familiar with any of them, nor does a quick google reveal anything useful (esp. about their relation to the ATP community). Pointers? "common logic reasoner" in google gives me nothing.
It's not impossible to come out of nowhere and build a credible reasoner (I did with OWL), but it's really non trivial. I'll be shocked if they produce sound and complete reasoners for FOL++ that are credible.
[AH] but I certainly was confused as to what people meant by Rule, and clarifications such as this thread can help avoid pointless future confusion when talking to different groups of people :D. Further, in the context of the OOR and using the OMV to tag various registered ontologies and create web-services and workflows around what is in the OOR, these distinctions could come to bear.
[BP] I'd be surprised. But I don't know what OOR and OMV are.
OOR is the Open Ontology Repository, the list through which this initial discussion was sparked and we were previously emailing. OMV is the Ontology Metadata Vocabulary, as per:
http://omv2.sourceforge.net/
Ok. I don't care at all about OOR. OMV looks rather overengineered for my tastes but nice to have on my radar. I had to laugh at :
Name hasFormalityLevel
Definition Level of formality of the ontology
Thanks! Snow is white!
Further, if OWL+SWRL or OWL+RIF ontologies will becoming more prevalent,
I doubt that they will be a significant fraction of OWL ontologies for a while, if ever.
then at the very least, these rule formalisms would need to be incorporated into the Hets logic graph.
Er..if you say so. SWRL should be easy if you have FOL. RIF less so, depending on what dialects you care about.
[AH] and what is the nature of their relationship (using OMV or an extension) to the OWL ontologies? What is the nature of a subset of some CL ontology that maps to some OWL+SWRL combo?
[BP]I don't really understand the question(s). Presumably the nature will be, oh, equivalence? What "nature"? Different equivalent formulations can have distinct computational issues, of course, but..."nature"?
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).
Bijan.