Reasoning with OBO Format
Jump to navigation
Jump to search
The following rules work for all OBO files. These rules are implemented by the OE RBR
Rules are written in prefix notation for unary relations (is_transitive, is_reflexive). For example:
id: X is_transitive: true
becomes: is_transitive(R)
relationships are written in infix; so
id: X is_a: Y relationship: R Z
becomes:
- X is_a Y
- X R Z
intersection and union tags are treated as list expressions
Graph Closure
Facts:
- is_transitive(is_a)
- is_reflexive(is_a)
these facts are built-in and cannot be modified
Rules:
- is_transitive(R), X R Y, Y R Z -> X R Z
- is_reflexive(R) -> X R X
- X is_a Y, Y R Z, not(is_class_level(R)) -> X R Z
- X R Y, Y is_a Z, not(is_class_level(R)) -> X R Z
- X R Y, Y S Z, transitive_over(R,S) -> X R Z
- X R1 Y, Y R2 Z, holds_over_chain(R,R1,R2) -> X R Z
- X R Y, R is_a S -> X S Y
- Y union_of (X, ...) -> X is_a Y
Classification
Classification rules do not need to be applied if the ontology has been pre-classified.
- X intersection_of (Y, ...) -> X is_a Y
- X intersection_of (R Y, ...) -> X R Y
- X intersection_of (G1,G2,...,R1 D1, R2 D2, ...), Y is_a G1, Y is_a G2, ..., Y R1 D1, Y R2 D2, ... -> Y is_a X
Consistency checking
- X disjoint_from Y, A is_a X, A is_a Y -> inconsistent.