REOL: Reasoning for Expressive Ontology Languages

本体和基于本体的词汇表变得越来越重要。它们提供了一个共同的词汇，以及有关术语的含义和这些术语之间的关系的计算机可用描述。本体在语义网和e-Science中扮演着重要的角色，它们被广泛应用于生物信息学、医学术语和其他知识管理应用中。它们在网格中也越来越重要，在网格中可以使用它们来支持基于语义的网格服务的发现、执行和监控。本体论最重要的一个方面是，它们包含以特殊方式构建的知识。本体的用户通常对获取关于在本体中描述的概念之间的关系的信息和查询本体感兴趣。这两项任务都需要推理工具：能够从本体论知识中推导出新知识的工具。要在本体论中表示知识，需要非常非常有表现力的语言。用这种语言进行推理是一个非常困难的组合问题。现有的推理工具只能与表现力较弱的语言一起使用，因此目前现代本体论中使用的语言和可用于推理的工具之间存在差距。有一些系统，称为定理证明器，原则上可以用于用非常有表现力的语言进行推理，但事实证明，对于本体论来说效率很低。该提案旨在开发使用非常有表现力的语言对大型本体进行推理的新方法，将这些方法作为最好的本体推理器和定理证明器的扩展来实现，并对使用新开发的工具进行非常大型本体的案例研究。

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.