The OBO-Edit Reasoner

A reasoner is a piece of software that examines an ontology and infers links that have not been explicitly stated by a curator. The structure and relationships of the ontology encode knowledge. Each relationship type has specific relations, and a reasoner uses these to deduce further information about the ontology.

The OBO-Edit reasoner is a very simple (but relatively fast) reasoning tool that relies on a small set of rules to make inferences about the ontology.

The reasoner deduces every single implied fact in an ontology. Every non-redundant ontology encodes a lot of implicit information, so the reasoner can use a lot of memory as it makes this implicit information explicit. See The Configuration Plugin for information about how to increase the memory available to OBO-Edit.

Reasoner Rules

This section documents all the rules OBO-Edit uses for reasoning. Realize that all these rules interact. If an implied link is discovered, that implied link may be used to discover yet other implied links.

Rule 1: Transitivity

A transitive relation is one where if there is a link "A -transitive_relation-> B" and "B -transitive_relation-> C", then "A -transitive_relation-> C". part_of is a transitive relation, so if "finger -part_of-> hand" and "hand -part_of-> arm", then it is implied that "finger -part_of-> arm". Transitive relationships are always preserved over is_a links, so if "A -transitive_relation-> B" and "B -is_a-> C" then "A -transitive_relation-> C". See An Introduction to OBO Ontologies for more information.

The OBO-Edit reasoner infers all the relationships in an ontology that are implied by transitivity but not explicitly stated. Consider the following simple ontology:

is_a and part_of are transitive relations, so the reasoner will deduce the following implied links:

Rule 2: Simple Genus/Differentia Implications

This is an extremely simple rule. It says that if a term has a cross product definition, the relationships in that definition hold true for the term itself at all times.

For example, let's say the following cross-product is defined for "cell development":

The reasoner will determine that "cell differentiation" has an implied affects relationship to "cell", because of the cross product definition. It will also assume that "cell differentiation" has an implied is_a relationship to "development" because of the genus section of the cross product definition.

Rule 3: Cross Product Definition Resolution

This rule infers is_a links implied by cross product definitions. One way of understanding this is to say that some terms in an ontology may "match" some other term's cross product defintion. If a term matches another term's cross product defintion, an is_a link is created between the terms.

A term matches a cross product definition when:

Recall that once the reasoner is running, implied links can be used by reasoner rules to discover new implied links. Therefore, this reasoner rule has access to all the links that were generated by the transitivity rule. These extra links can lead to useful (and sometimes unexpected) implications from the reasoner.

Evidence

Every time the reasoner discovers a new link, that discovery is based on some supporting links in the ontology. These supporting links are called the evidence or explanation for the new implied link.

Link evidence consists of two parts: The rule that was used to discover the implied link, and the links that were used to support the discovery. Implied links can be used as evidence for other implied links, so the evidence for one link might have its own evidence.

Every link in an ontology has evidence, even non-implied links. Links that were explicitly created by a human user are explained with the special evidence GIVEN. This piece of evidence means that the link was made by a human, not the reasoner.

It is possible for a link to have more than one explanation. A link may be implied by transitivity, and multiple collections of links can be used to support that implication. The reasoner records every possible explanation for an implied link.

See The Explanation Plugin to learn how to see the evidence for implied links.

Reasoner Checks

The reasoner has the capability to check the ontology for certain kinds of problems. In the future, the reasoner will support many different checks, but right now the reasoner only checks for:

Redundant Links

Redundant links are links that were explicitly created by a human but are unncessary because that link is implied by other facts in the ontology. Consider this version of our elephant ontology:

The link "tusk -part_of-> animal" is redundant, because that relationship is already implied by transitivity.

Formally, a redundant link is any link with multiple explanations, one of which is GIVEN. This definition works because if a link has multiple explanations, the reasoner must have discovered at least one of them, and if one of the explanations is GIVEN, a human must have created the link. Therefore, a human has created a link that the reasoner was able to infer automatically, making the link redundant.

By default, redundant links are shown with a red arrow. It is possible to create special searches, filters and renderers for redundant links. See Link Filters for more information.

Reasoner Limitations

The OBO-Edit reasoner is very limited at the moment. Things that it currently cannot do include:

These capabilities will be slowly added in future versions of OBO-Edit.