OBO-Edit:Rule Based Reasoner: Difference between revisions

From GO Wiki
Jump to navigation Jump to search
No edit summary
 
(3 intermediate revisions by the same user not shown)
Line 3: Line 3:
[[OBO-Edit:Rule Based Reasoner]] (RBR). Successor to LPR.
[[OBO-Edit:Rule Based Reasoner]] (RBR). Successor to LPR.


OBO relations are treated as binary predicates R1, ... Rn, and edges in the OBO graph as facts R(A,B). Additional unary predicates include transitive/1, class_level/1
OBO relations are treated as binary predicates R1, ... Rn, and edges in the OBO graph as facts R(A,B). Additional unary predicates include transitive/1, class_level/1 corresponding the boolean tags of the same name in obo-format. logical/cross-product definitions are treated as facts using the equivalent/2 predicate.


* Transitivity
* Transitivity
Line 11: Line 11:
** not class_level(R),is_a(X,Y),R(Y,Z) -> R(X,Z)
** not class_level(R),is_a(X,Y),R(Y,Z) -> R(X,Z)
* Intersection_of
* Intersection_of
** D =def A1^A2^...^An ==> Tr(x,A1),Tr(x,A2),...,Tr(x,An) -> is_a(x,D)
** equivalent(D, A1^A2^...^An) ==> Tr(x,A1),Tr(x,A2),...,Tr(x,An) -> is_a(x,D)
** Tr(x,R(Z)) ==> R(x,Z)
** Tr(x,R(Z)) ==> R(x,Z)
** Tr(x,Z) ==> is_a(x,Z)
** Tr(x,Z) ==> is_a(x,Z)
* Subrelations
* union_of (partial semantics)
** equivalent(D, A1\/A2\/...\/An) ==> is_a(A1,D),...,is_a(An,D)
* Subrelations (note obo format uses the is_a tag for relation subsumption)
** R(X,Y),is_a(R,R2) -> R2(X,Y)
** R(X,Y),is_a(R,R2) -> R2(X,Y)
* [[transitive_over]] and arbitrary [[Relation_composition]]
* [[transitive_over]] and arbitrary [[Relation_composition]]
Line 30: Line 32:
   intersection_of: r c
   intersection_of: r c


is translated to the logical axioms:
is written in predicate form as
 
  equivalent( a, b^r(c) )
 
and is macro-translated to the logical axioms:


   is_a(x,b), r(x,c) -> is_a(x,a)
   is_a(x,b), r(x,c) -> is_a(x,a)
   is_a(a,b)
   is_a(a,b)
   r(a,c)
   r(a,c)


== Implementation ==
== Implementation ==

Latest revision as of 13:40, 22 August 2010

oboedit_rbr

OBO-Edit:Rule Based Reasoner (RBR). Successor to LPR.

OBO relations are treated as binary predicates R1, ... Rn, and edges in the OBO graph as facts R(A,B). Additional unary predicates include transitive/1, class_level/1 corresponding the boolean tags of the same name in obo-format. logical/cross-product definitions are treated as facts using the equivalent/2 predicate.

  • Transitivity
    • transitive(R),R(X,Y),R(Y,Z) -> R(X,Z)
  • Propagation over/under is_a
    • not class_level(R),R(X,Y),is_a(Y,Z) -> R(X,Z)
    • not class_level(R),is_a(X,Y),R(Y,Z) -> R(X,Z)
  • Intersection_of
    • equivalent(D, A1^A2^...^An) ==> Tr(x,A1),Tr(x,A2),...,Tr(x,An) -> is_a(x,D)
    • Tr(x,R(Z)) ==> R(x,Z)
    • Tr(x,Z) ==> is_a(x,Z)
  • union_of (partial semantics)
    • equivalent(D, A1\/A2\/...\/An) ==> is_a(A1,D),...,is_a(An,D)
  • Subrelations (note obo format uses the is_a tag for relation subsumption)
    • R(X,Y),is_a(R,R2) -> R2(X,Y)
  • transitive_over and arbitrary Relation_composition
    • R1(X,Y),R2(Y,Z),holds_over_chain(R,R1,R2) -> R(X,Z)
  • Relation intersections
    • R1(X,Y),R2(X,Y),R=R1^R2 -> R(X,Y)

In the above, -> denotes logical implication, ==> denotes a macro translation

For example

 [Term]
 id: a
 intersection_of: b
 intersection_of: r c

is written in predicate form as

 equivalent( a, b^r(c) )

and is macro-translated to the logical axioms:

 is_a(x,b), r(x,c) -> is_a(x,a)
 is_a(a,b)
 r(a,c)

Implementation

The internal design of the RBR is highly simplified compared to the LPR. It was written entirely by cjm. Note the profile is the same as for the LPR, however, the LPR bug does not arise due to the design of the RBR.

Note that the RBR is currently slow for incremental reasoning. This is because it checks all links after any links are added or deleted. This can easily be fixed in future versions. When it is, the LPR will probably be retired altogether.