Permalink
Browse files

updated biospatial

  • Loading branch information...
carmenchui committed Jun 8, 2016
1 parent 6166e13 commit 8411f1ec276384d8e5e1fe3ed925529af940bb0f
@@ -3,6 +3,9 @@
(cl-comment 'Author: Anthony G. Cohn')
(cl-comment 'Paper: Formalising Bio-Spatial Knowledge')
(cl-comment 'This ontology imports RCC')
(cl-imports http://colore.oor.net/rcc_continuous_process/rcc_state.clif)
(cl-comment 'Axiom numbering corresponds to numbering found in the paper.')
(cl-comment 'Axiom ID: A1')
@@ -245,11 +248,42 @@
(Guanine p)
(Thymine p))))))))))
(cl-comment 'stopped at D21, page 6')
(cl-comment 'fix exclamation marks axioms d14 d15 d10')
(cl-comment 'Axiom ID: D21')
(cl-comment 'to do!')
(cl-comment 'Axiom ID: D22')
(forall (z1 z2)
(iff (ChainLinked2 z1 z2)
(exists (s g)
(and (PhosphateGroup g)
(5CSugar s)
(CoValLinked s g)
(Part g z1)
(Part s z2)))))
(cl-comment 'Axiom ID: D23-25')
(cl-comment 'Axiom ID: A13')
(forall (x)
(if (Close x y)
(DC x y)))
(cl-comment 'Axiom ID: D26')
(forall (x)
(iff (Bead x)
(exists (t)
(and (Tunnel t (sp x))
(or (T x)(C x)(A x)(G x))))))
(cl-comment 'Axiom ID: D27')
(forall (t x)
(iff (Tunnel t x)
(exists (t1 t2 t3)
(Tunnel t t1 t2 t3 x))))
Binary file not shown.
@@ -36,7 +36,9 @@ formulas(assumptions).
% Reading from file /stl/cchui/colore/ontologies//bipartite_incidence/p9/weak_loopless.p9
% Reading from file /stl/cchui/colore/ontologies//tripartite_incidence/p9/coplanar_double_collinear.p9
(all x all y all z all w all q all l1 all l2 all l3 (plane(q) & point(x) & point(y) & point(z) & point(w) & in(x,q) & in(y,q) & in(z,q) & in(w,q) & line(l1) & in(l1,q) & in(x,l1) & in(y,l2) & line(l2) & in(l2,q) & in(x,l2) & in(z,l2) & line(l3) & in(l3,q) & in(x,l3) & in(w,l3) -> w = z | y = z | w = y)).
(all x all y all z all w all q all l1 all l2 all l3 (plane(q) & point(x) & point(y) & point(z) & point(w) &
in(x,q) & in(y,q) & in(z,q) & in(w,q) & line(l1) & in(l1,q) & in(x,l1) & in(y,l2) & line(l2) & in(l2,q)
& in(x,l2) & in(z,l2) & line(l3) & in(l3,q) & in(x,l3) & in(w,l3) -> w = z | y = z | w = y)).
% Reading from file /stl/cchui/colore/ontologies//tripartite_incidence/p9/double_pendant.p9
(all q all x all y all z (planar_pendant(x,q) & planar_pendant(y,q) & planar_pendant(z,q) -> x = y | y = z | z = x)).
@@ -85,7 +85,9 @@ end_of_list.
formulas(goals).
(all x all y all z all w all q all l1 all l2 all l3 (plane(q) & point(x) & point(y) & point(z) & point(w) & in(x,q) & in(y,q) & in(z,q) & in(w,q) & line(l1) & in(l1,q) & in(x,l1) & in(y,l2) & line(l2) & in(l2,q) & in(x,l2) & in(z,l2) & line(l3) & in(l3,q) & in(x,l3) & in(w,l3) -> w = z | y = z | w = y)).
(all x all y all z all w all q all l1 all l2 all l3 (plane(q) & point(x) & point(y) & point(z) & point(w)
& in(x,q) & in(y,q) & in(z,q) & in(w,q) & line(l1) & in(l1,q) & in(x,l1) & in(y,l2) & line(l2) & in(l2,q)
& in(x,l2) & in(z,l2) & line(l3) & in(l3,q) & in(x,l3) & in(w,l3) -> w = z | y = z | w = y)).
end_of_list.
@@ -111,6 +111,7 @@
(cl-comment 'Axiom ID: MR-ax-12')
(cl-comment 'If there are two distinct functional groups, there exists an atom that is only in one of the groups and not the other.')
(cl-comment 'provable from mr-ax-11, we don't need this')
(forall (x y)
(if (and (functional_group x)
(functional_group y)

0 comments on commit 8411f1e

Please sign in to comment.