Reasoning for Expressive Ontology Languages (REOL)
REOL is a research project funded by EPSRC, reference EP/C537211/1. The project started on 01st of October 2005 and will last until 30th of September 2008.
Background
In recent years, ontologies have been applied in numerous fields in computer science. A significant momentum in research and application of ontology technologies was gained from the development of Ontology Web Language (OWL) -- a W3C standard for building ontologies on the Web. OWL is a language that allows to formally annotate online resources with semantics. This, in turn, makes the resources machine-processable, enabling a higher degree of automation in information processing.
The formal underpinnings of OWL are provided by Description Logics (DLs) -- a family of knowledge representation formalisms with a long tradition in both formal research and building practical reasoning systems. It has widely been accepted that building reasoning systems is easier if the underlying logic is decidable; therefore, one of the main research challenges in DL research is to design languages that are expressive but yet decidable. However, the experience gathered in the past years by applying OWL to practical problems suggests that many applications of ontologies need the expressivity that cannot be captured by decidable languages.
Project Goals
The primary goal of this project is to develop techniques that address the expressivity requirements of various applications. This is to be achieved by a synergy between two previously disjoint techniques. Currently, tableaux algorithms are the state-of-the-art for reasoning with DL ontologies. However, in recent years, great progress has been made in designing resolution-based algorithms for reasoning with ontologies. These two types of algorithms seem to enjoy two complementary properties: tableaux are model-building calculi that seem to perform well on satisfiable problems, whereas resolution is a refutation calculus that seems to perform well on unsatisfiable problems. The main idea of this project is to extend both calculi and provide a common framework for integrating them.
This project also deals with providing nonmonotonic extensions to ontology languages. Namely, the experience in building OWL applications has revealed that many applications require expressivity that goes beyond what can be axiomatized in first-order logic. For example, many applications require constraints (statements specifying which databases are correctly formed) or exceptions. It is widely conjectured that this requirement can be addressed by integrating ontology languages with rule-based formalisms, such as logic programming. Currently, the Rule Interchange Format Working Group of W3C is working on a possible standard that would integrate the two formalisms. In this project, we are working on a formal theory and practical reasoning algorithms that would enable such an integration.
