Permalink
Browse files

added comments for most_attachment (will be checked later)

  • Loading branch information...
carmenchui committed Oct 11, 2017
1 parent e136980 commit 43526e1c73473d378ba40c743da03220cf027f59
Showing with 10 additions and 1 deletion.
  1. +10 −1 ontologies/most/most_attachment.clif
@@ -13,6 +13,7 @@
(cl-imports http://colore.oor.net/most/most_root.clif)
(cl-imports http://colore.oor.net/most/def_most_attachment.clif)
(cl-comment 'an artefact of bridges discussion? ')
(cl-comment 'most version of twin junction in tripartite incidence -- need ENG version')
(forall (b g1 g2)
(if (and (group g1)(group g2)
@@ -23,6 +24,7 @@
(spiro g1 g2 a2)
(not (= a1 a2))))))
(cl-comment 'is this axiom deprecated? or too strong?')
(cl-comment 'For a bond found in two groups, it must mean the two groups are spiroed at an atom common between them.')
(forall (a1 a2 a3 b g1 g2)
(if (and (atom a1)(atom a2)(atom a3)
@@ -37,11 +39,13 @@
(= a1 a3)
(= a2 a3))))
(cl-comment 'too strong?')
(cl-comment 'A fused atom is in at most two groups. Uniqueness of fusion connection.')
(forall (a1 a2 a3 g1 g2)
(if (and (fusedAtom a1 g1 g2)(fusedAtom a1 g1 g2)(fusedAtom a3 g1 g2))
(or (= a1 a2)(= a1 a3)(= a2 a3))))
(cl-comment 'is this axiom deprecated?')
(cl-comment 'For two groups that are fused together, there is a unique fused atom. Something we should be able to prove.')
(forall (g1 g2)
(if (fused g1 g2)
@@ -72,6 +76,7 @@
(mol b1 g2)(mol b2 g2))
(and (tether g1 g2 b1)(tether g1 g2 b2))))
(cl-comment 'Entailed by unique fusion/spiro/tether')
(cl-comment 'most version of weak face intersect in tripartite incidence -- need ENG version')
(forall (g1 g2 a1 a2)
(if (and (group g1)
@@ -87,6 +92,7 @@
(exists (b)
(and (bond b)(mol b g1)(mol b g2)))))
(cl-comment 'Entailed by unique fusion/spiro/tether')
(cl-comment 'There do not exist two functional groups x and y, and 3 atoms such that those three atoms are in functional groups x and y. Any two functional groups intersect at AT MOST two atoms.')
(not (exists (x y a b c)
(and (group x)
@@ -101,13 +107,15 @@
(not (= b c))
(not (= a c)))))
(cl-comment 'Entailed by unique fusion')
(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.')
(forall (x y)
(if (and (group x)(group y)(not (= x y)))
(exists (a)
(and (atom a)(mol a x)(not (mol a y))))))
(cl-comment 'If two functional groups intersect at two distinct atoms, then the atoms are in the same bond.')
(cl-comment 'Entailed by unique fusion and unique spiro')
(cl-comment 'If two functional groups intersect at two distinct atoms, then the atoms are in the same bond.')
(forall (g1 g2 a1 a2)
(if (and (atom a1)(atom a2)
(group g1)(group g2)
@@ -119,6 +127,7 @@
(mol b g1)(mol b g2)
(mol a1 b)(mol a2 b)))))
(cl-comment 'Entailed by unique fusion')
(cl-comment 'Functional groups cannot be coextensive. Two groups cannot have the exact same set of atoms.')
(forall (g1 g2 a1 a2)
(if (and (group g1)(group g2)(not (= g1 g2))

0 comments on commit 43526e1

Please sign in to comment.