ConDOR: Consequence-Driven Ontology Reasoning

Ontologies, and ontology based vocabularies, are becoming increasingly important. They provide a common vocabulary together with computer accessible descriptions of the meaning of relevant terms through relationships with other terms. For example, in an ontology describing human anatomy the vocabulary could include terms such as [Organ], [Circulatory System], [Heart], etc., and one can define a term [Muscular Organ] as an [Organ] that is a part of the [Muscular System] and a term [Heart] as a [Muscular Organ] that is a part of the [Circulatory System].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. One of the most important aspects 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 require reasoning tools that can derive new knowledge from the knowledge explicitly stated in ontologies. For example a reasoning tool should be able to derive that [Heart] is a part of the [Muscular System] which is not explicitly stated in the anatomical ontology but is a logical consequence of the above definitions for [Heart] and [Muscular Organ].Most existing ontology reasoners do not derive logical consequences of ontological axioms explicitly, but instead they check whether it is possible to construct a model of the ontology where the target consequence does not hold, e.g., they try to construct a situation where [Heart] would be a part of the [Circulatory System] but not a part of the [Muscular System]. If such a situation is not possible, then it is concluded that the target consequence follows from the axioms in the ontology. One problem with this technique is that when an ontology expresses long and possibly cyclic dependencies between terms, e.g., [Heart] is a part of [Circulatory System] which has a part [Lung] which is a part of [Respiratory System] which has a part [Trachea], etc., then the reasoner has to construct very large models. For some existing medical ontologies, the models are so big that they do not fit into the main memory of a computer. Another problem is that the ontology may potentially have a large number of different models, each of which must be independently explored by the reasoner. Ontology languages provide for constructors called 'number restrictions', which result in a particularly large number of models. Number restrictions are used to specify quantitative information in ontologies and are often used in bio-chemical ontologies, for example to express that a molecule of [Ethanol] contains {exactly 6} [Hydrogen Atoms]. These limitations of model-building reasoners, therefore, pose a serious problem for the development of large medical and bio-chemical ontologies---without efficient reasoning tools, for example, the users of such ontologies may not be able to obtain the information that they are interested in.In this project we investigate alternative consequence driven reasoning procedures that do not build models but explicitly derive logical consequences of ontological axioms. Our preliminary investigations suggest that both problems mentioned above can be avoided for consequence-driven reasoning procedures: there is no need to keep track of large models, and the number of logical consequences of ontological axioms is typically much smaller than the sizes and the number of the models.