-
Notifications
You must be signed in to change notification settings - Fork 35
/
most_bridges.clif
126 lines (112 loc) · 4.01 KB
/
most_bridges.clif
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
/*******************************************************************************
* Copyright (c) University of Toronto and others. All rights reserved.
* The content of this file is licensed under the Creative Commons Attribution-
* ShareAlike 4.0 Unported license. The legal text of this license can be
* found at http://creativecommons.org/licenses/by-sa/4.0/legalcode.
*
* Contributors:
* Carmen Chui, Michael Gruninger - initial implementation
*******************************************************************************/
(cl-text http://colore.oor.net/most/most_bridges.clif
(cl-imports http://colore.oor.net/most/definitions/most_bridges_definitions.clif)
(cl-imports http://colore.oor.net/most/most_attachment.clif)
(cl-comment 'Axiom: MBR-1')
(cl-comment 'Uniqueness of spiro connection.')
(exists (a1)
(forall (g1 g2 a2)
(if (and (spiro g1 g2 a1)
(spiro g1 g2 a2))
(= a1 a2))))
(cl-comment 'Axiom: MBR-2')
(cl-comment 'Uniqueness of tether connection.')
(exists (b1)
(forall (g1 g2 b2)
(if (and (tether g1 g2 b1)(tether g1 g2 b2))
(= b1 b2))))
(cl-comment 'Axiom: MBR-3')
(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)
(exists (a1 a2)
(and (fusedAtom a1 g1 g2)
(fusedAtom a2 g1 g2)
(not (= a1 a2))))))
(cl-comment 'Axiom: MBR-4')
(cl-comment 'There are at most two bridgeheads in a group.')
(forall (a1 a2 a3 g1 g2)
(if (and (bridgehead a1 g1 g2)(bridgehead a2 g1 g2)(bridgehead a3 g1 g2))
(or (= a1 a2)(= a1 a3)(= a2 a3))))
(cl-comment 'Axiom: MBR-5')
(cl-comment 'Potential Extension Axiom: one group can be multiply fused with one other group.')
(forall (g1 g2 g3)
(if (and (not (= g1 g2))
(multiply_fused g1 g2)
(multiply_fused g2 g3))
(= g1 g2)))
(cl-comment '========================================================================')
(cl-comment '======= MOST_BRIDGES DEFINITIONS =======')
(cl-comment '========================================================================')
(cl-comment 'Axiom: MBRD-1')
(cl-comment 'Definition: multiply_fused is a relation that indicates that two groups are multiply fused together if and only if there are two or more bonds that are in both groups.')
(forall (g1 g2)
(iff (multiply_fused g1 g2)
(and (group g1)
(group g2)
(not (= g1 g2))
(exists (b1 b2)
(and (bond b1)
(bond b2)
(not (= b1 b2))
(mol b1 g1)
(mol b1 g2)
(mol b2 g1)
(mol b2 g2))))))
(cl-comment 'Axiom: MBRD-2')
(cl-comment 'Definition of fused atom: an atom that is in bonds of different groups.')
(forall (a1 g1 g2)
(iff (fusedAtom a1 g1 g2)
(and (atom a1)(group g1)(group g2)
(mol a1 g1)(mol a1 g2)
(not (= g1 g2))
(exists (b1 b2)
(and (bond b1)(bond b2)
(mol a1 b1)(mol a1 b2)
(mol b1 g1)(mol b2 g2))))))
(cl-comment 'Axiom: MBRD-3')
(cl-comment 'Definition for bridge atom: an atom a in a group g1 is in the bridge of the molecule if the group is fused along multiple edges of another group g3.')
(forall (a g1 g3)
(iff (bridge a g1 g3)
(and (atom a)
(group g1)
(group g3)
(mol a g1)(mol a g3)
(forall (g2)
(if (and (group g2)
(mol a g2))
(= g1 g2)))
(multiply_fused g1 g3))))
(cl-comment 'Axiom: MBRD-4')
(cl-comment 'Definition: A bridgehead atom is an atom in the ring system g1 that participates in bond with three or more non-hydrogen skeletal atoms. This is equivalent to junction in the tripartite theories.')
(forall (a g1 g2)
(iff (bridgehead a g1 g2)
(and (atom a)
(group g1)
(group g2)
(not (= g1 g2))
(exists (b b1 b2)
(and (bond b)
(bond b1)
(bond b2)
(not (= b1 b2))
(not (= b b1))
(not (= b b2))
(mol a b)
(mol a b1)
(mol a b2)
(mol b g1)
(mol b g2)
(mol b1 g1)
(not (mol b1 g2))
(not (mol b2 g1))
(mol b2 g2))))))
)