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.
The objectives of the project are:
1. To develop unsatisfiability-checking methods for such languages based on the extension, specialisation and optimisation of existing theorem proving methods for FOL that enable them to cope with ontologies having hundreds of thousands of axioms.
2. To develop satisfiability-checking methods for such languages based on extensions of existing tableaux algorithms for decidable fragments of FOL, on improving the performance of theorem provers on satisfiable problems and on optimised finite model building techniques.
3. To develop efficient reasoning systems for such languages based on a combination of our satisfiability and unsatisfiability-checking methods, and to evaluate the performance of these systems using ontologies derived from real applications in e-Science.
