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.