REOL: Reasoning for Expressive Ontology Languages

Ontologies, and ontology based vocabularies, have become increasingly important. They provide a common vocabulary together with computeraccessible descriptions of the meaning of relevant terms and relationships between these terms. Ontologies play a major role in the Semantic Web and in e-Science where they are widely used in, e.g., bio-informatics, medical terminologies and other knowledge management applications. They are also of increasing importance in the Grid, where they may be used, e.g., to support semantic based discovery, execution and monitoring of Grid services. One of the most important aspect of ontologies is that they contain knowledge structured in a special way. The users of ontologies are typically interested in obtaining information about relationships between concepts described in ontologies and querying the ontologies. Both tasks requires reasoning tools: tools that can derive new knowledge from the ontological knowledge. To represent knowledge in ontologies, one needs very very expressive languages. Reasoning with such languages is a very hard combinatorial problem. The existing reasoning tools can only work with less expressive languages, so there is currently a gap between the languages used in modern ontologies and tools that can be used for reasoning. There are systems, called theorem provers, that can in principle be used for reasoning with very expressive languages but proved to be inefficient for ontologies. The proposal aims at developing new methods of reasoning with large ontologies using very expressive languages, implementation of these methods as extensions of the best ontology reasoners and theorem provers, and case studies of the use of the newly developed tools with very large ontologies.