1% -------------------------------------------------------------------------
2% Lex Demo 4
3%
4% This is a more substantial problem based on the x^3 = x problem from
5% ring theory (x^3 = x implies commutativity).
6%
7% In this demo we prove only the intermediate lemma:  3xy + 3yx = E.
8%
9% In addition to lex() and special_unary(), this demo makes use of
10% several Otter features (e.g., age factors, conditional demodulation)
11% and representation tricks (e.g., coefficients, templates for polynomial
12% subtraction).
13%
14% Contributed by Bob Veroff.
15% -------------------------------------------------------------------------
16
17% inference rules
18set(hyper_res).
19clear(order_hyper).
20set(para_into).
21set(para_from).
22set(para_from_left).
23clear(para_from_right).
24set(para_into_left).
25clear(para_into_right).
26
27% equality
28set(order_eq).
29set(dynamic_demod).
30assign(dynamic_demod_depth,1).
31assign(dynamic_demod_rhs,5).
32set(back_demod).
33clear(symbol_elim).
34set(lex_order_vars).
35
36% processing
37assign(demod_limit,250).
38assign(max_weight, 999).
39assign(max_literals, 1).
40
41% printing
42clear(print_kept).
43clear(print_back_sub).
44clear(print_new_demod).
45clear(print_back_demod).
46
47% search
48assign(age_factor,1).
49
50% lexical ordering of terms
51lex([A,B,E,MULT(x,x),INV(x),Coeff(x,x),ADD(x,x)]).
52special_unary([INV(x),Coeff(x,x)]).
53
54list(usable).
55
56   % ring axioms
57   EQ(ADD(x,y),ADD(y,x)).
58   EQ(ADD(ADD(x,y),z),ADD(x,ADD(y,z))).
59   EQ(MULT(MULT(x,y),z),MULT(x,MULT(y,z))).
60   EQ(MULT(ADD(x,y),z),ADD(MULT(x,z),MULT(y,z))).
61   EQ(MULT(x,ADD(y,z)),ADD(MULT(x,y),MULT(x,z))).
62   EQ(ADD(x,E),x).
63   EQ(ADD(E,x),x).
64   EQ(ADD(INV(x),x),E).
65   EQ(ADD(x,INV(x)),E).
66   EQ(x,x).
67
68   % key lemmas
69   EQ(MULT(INV(x),y),INV(MULT(x,y))).
70   EQ(MULT(x,INV(y)),INV(MULT(x,y))).
71   EQ(INV(ADD(x,y)),ADD(INV(x),INV(y))).
72
73   % term identification for polynomial subtraction
74
75   % identify terms without coefficients
76   TID(ADD(x,v),x,v).
77   TID(ADD(x1,ADD(x,v)),x,ADD(x1,v)).
78   TID(ADD(x1,ADD(x2,ADD(x,v))),x,ADD(x1,ADD(x2,v))).
79   TID(ADD(x1,ADD(x2,ADD(x3,ADD(x,v)))),x,
80       ADD(x1,ADD(x2,ADD(x3,v)))).
81   TID(ADD(x1,ADD(x2,ADD(x3,ADD(x4,ADD(x,v))))),x,
82       ADD(x1,ADD(x2,ADD(x3,ADD(x4,v))))).
83   TID(ADD(x1,ADD(x2,ADD(x3,ADD(x4,ADD(x5,ADD(x,v)))))),x,
84       ADD(x1,ADD(x2,ADD(x3,ADD(x4,ADD(x5,v)))))).
85   TID(ADD(x1,ADD(x2,ADD(x3,ADD(x4,ADD(x5,ADD(x6,ADD(x,v))))))),x,
86       ADD(x1,ADD(x2,ADD(x3,ADD(x4,ADD(x5,ADD(x6,v))))))).
87
88   % identify terms with coefficients
89   TID(Coeff(x,z),x,Coeff(x,$DIFF(z,1))) | $NOT($INT(z)).
90   TID(ADD(Coeff(x,z),v),x,ADD(Coeff(x,$DIFF(z,1)),v)) | $NOT($INT(z)).
91   TID(ADD(x1,ADD(Coeff(x,z),v)),x,ADD(x1,ADD(Coeff(x,$DIFF(z,1)),v))) |
92          $NOT($INT(z)).
93   TID(ADD(x1,ADD(x2,ADD(Coeff(x,z),v))),x,
94       ADD(x1,ADD(x2,ADD(Coeff(x,$DIFF(z,1)),v)))) | $NOT($INT(z)).
95   TID(ADD(x1,ADD(x2,ADD(x3,ADD(Coeff(x,z),v)))),x,
96       ADD(x1,ADD(x2,ADD(x3,ADD(Coeff(x,$DIFF(z,1)),v))))) | $NOT($INT(z)).
97   TID(ADD(x1,ADD(x2,ADD(x3,ADD(x4,ADD(Coeff(x,z),v))))),x,
98       ADD(x1,ADD(x2,ADD(x3,ADD(x4,ADD(Coeff(x,$DIFF(z,1)),v)))))) |
99          $NOT($INT(z)).
100   TID(ADD(x1,ADD(x2,ADD(x3,ADD(x4,ADD(Coeff(x,z),v))))),x,
101       ADD(x1,ADD(x2,ADD(x3,ADD(x4,ADD(Coeff(x,$DIFF(z,1)),v)))))) |
102          $NOT($INT(z)).
103
104   % subtraction templates
105   IDENT(x,x).
106   -EQ(w,v) | -TID(w,x1,w1) | -TID(v,x2,v1) |
107      -$RENAME(x1,x2) | -IDENT(x1,x2) | EQ(ADD(INV(w1),v1),E).
108   -EQ(w,E) | -EQ(v,E) | -TID(w,x1,w1) | -TID(v,x2,v1) |
109      -$RENAME(x1,x2) | -IDENT(x1,x2) | EQ(ADD(INV(w1),v1),E).
110
111   % recognize cycles
112   -EQ(Coeff(x,y),E) | EQ(IsCycle(x),y).
113
114end_of_list.
115
116list(sos).
117
118   % special hypothesis
119   EQ(MULT(x,MULT(x,x)),x).
120
121   % denial
122   -EQ(ADD(Coeff(MULT(A,B),3),Coeff(MULT(B,A),3)),E).
123
124end_of_list.
125
126list(demodulators).
127
128   % special conditional demodulator for cycles
129   $GT(x,IsCycle(z)) -> EQ(Coeff(z,x),Coeff(z,$MOD(x,IsCycle(z)))).
130
131   % special hypothesis
132   EQ(MULT(x,MULT(x,x)),x).
133
134   % commutativity of addition
135   EQ(ADD(x,y),ADD(y,x)).
136   EQ(ADD(x,ADD(y,z)),ADD(y,ADD(x,z))).
137
138   % associativity
139   EQ(ADD(ADD(x,y),z),ADD(x,ADD(y,z))).
140   EQ(MULT(MULT(x,y),z),MULT(x,MULT(y,z))).
141
142   % distributivity
143   EQ(MULT(ADD(x,y),z),ADD(MULT(x,z),MULT(y,z))).
144   EQ(MULT(x,ADD(y,z)),ADD(MULT(x,y),MULT(x,z))).
145
146   % identity
147   EQ(ADD(x,E),x).
148   EQ(ADD(E,x),x).
149   EQ(MULT(E,x),E).
150   EQ(MULT(x,E),E).
151   EQ(INV(E),E).
152
153   % INV simplification and canonicalization
154   EQ(INV(INV(x)),x).
155   EQ(MULT(x,INV(y)),INV(MULT(x,y))).
156   EQ(MULT(INV(x),y),INV(MULT(x,y))).
157   EQ(INV(ADD(x,y)),ADD(INV(x),INV(y))).
158   EQ(INV(Coeff(x,y)),Coeff(INV(x),y)).
159
160   % INV cancellation
161   EQ(ADD(x,INV(x)),E).
162   EQ(ADD(x,ADD(INV(x),y)),y).
163
164   % coefficients
165   EQ(ADD(x,x),Coeff(x,2)).
166   $INT(y) -> EQ(ADD(x,Coeff(x,y)),Coeff(x,$SUM(y,1))).
167   $AND($INT(y),$INT(z)) -> EQ(ADD(Coeff(x,y),Coeff(x,z)),Coeff(x,$SUM(y,z))).
168
169   EQ(ADD(x,ADD(x,y)),ADD(Coeff(x,2),y)).
170   $INT(y) -> EQ(ADD(x,ADD(Coeff(x,y),z)),ADD(Coeff(x,$SUM(y,1)),z)).
171   $AND($INT(y),$INT(z)) -> EQ(ADD(Coeff(x,y),ADD(Coeff(x,z),v)),ADD(Coeff(x,$SUM(y,z)),v)).
172
173   % nested coefficients
174   $AND($INT(y),$INT(z)) -> EQ(Coeff(Coeff(x,y),z),Coeff(x,$PROD(y,z))).
175
176   % simplification and canonicalization with coefficients
177   EQ(Coeff(E,x),E).
178   EQ(Coeff(x,0),E).
179   EQ(Coeff(x,1),x).
180   EQ(MULT(x,Coeff(y,z)),Coeff(MULT(x,y),z)).
181   EQ(MULT(Coeff(x,z),y),Coeff(MULT(x,y),z)).
182   EQ(Coeff(ADD(x,y),z),ADD(Coeff(x,z),Coeff(y,z))).
183
184   % ordinary INV cancellation with coefficients
185   $INT(y) -> EQ(ADD(x,Coeff(INV(x),y)),Coeff(INV(x),$DIFF(y,1))).
186   $INT(y) -> EQ(ADD(INV(x),Coeff(x,y)),Coeff(x,$DIFF(y,1))).
187   EQ(ADD(Coeff(x,y),Coeff(INV(x),y)),E).
188   $AND($INT(y),$AND($INT(z),$GT(y,z))) ->
189      EQ(ADD(Coeff(x,y),Coeff(INV(x),z)),Coeff(x,$DIFF(y,z))).
190   $AND($INT(y),$AND($INT(z),$GT(z,y))) ->
191      EQ(ADD(Coeff(x,y),Coeff(INV(x),z)),Coeff(INV(x),$DIFF(z,y))).
192
193   $INT(y) -> EQ(ADD(x,ADD(Coeff(INV(x),y),zzz)),ADD(Coeff(INV(x),$DIFF(y,1)),zzz)).
194   $INT(y) -> EQ(ADD(INV(x),ADD(Coeff(x,y),zzz)),ADD(Coeff(x,$DIFF(y,1)),zzz)).
195   EQ(ADD(Coeff(x,y),ADD(Coeff(INV(x),y),zzz)),zzz).
196   $AND($INT(y),$AND($INT(z),$GT(y,z))) ->
197      EQ(ADD(Coeff(x,y),ADD(Coeff(INV(x),z),zzz)),ADD(Coeff(x,$DIFF(y,z)),zzz)).
198   $AND($INT(y),$AND($INT(z),$GT(z,y))) ->
199      EQ(ADD(Coeff(x,y),ADD(Coeff(INV(x),z),zzz)),ADD(Coeff(INV(x),$DIFF(z,y)),zzz)).
200
201   % ********************
202   % Literal Demodulators
203   % ********************
204
205   % subtraction by demodulation (complex terms)
206   EQ(EQ(ADD(x,y),ADD(u,v)),EQ(ADD(INV(ADD(u,v)),ADD(x,y)),E)).
207   EQ(EQ(ADD(x,y),MULT(u,v)),EQ(ADD(INV(MULT(u,v)),ADD(x,y)),E)).
208   EQ(EQ(ADD(x,y),INV(u)),EQ(ADD(u,ADD(x,y)),E)).
209   EQ(EQ(ADD(x,y),Coeff(u,v)),EQ(ADD(INV(Coeff(u,v)),ADD(x,y)),E)).
210
211   % prefer non inverse form
212   EQ(EQ(INV(x),E),EQ(x,E)).
213
214   % normalize so leftmost term non INV
215   EQ(EQ(ADD(INV(x),y),E),EQ(ADD(x,INV(y)),E)).
216   EQ(EQ(ADD(Coeff(INV(x),y),z),E),EQ(ADD(Coeff(x,y),INV(z)),E)).
217
218   % literal demodulation takes place before equality ordering
219
220   EQ(EQ(MULT(u,v),ADD(x,y)),EQ(ADD(INV(MULT(u,v)),ADD(x,y)),E)).
221   EQ(EQ(INV(u),ADD(x,y)),EQ(ADD(u,ADD(x,y)),E)).
222   EQ(EQ(Coeff(u,v),ADD(x,y)),EQ(ADD(INV(Coeff(u,v)),ADD(x,y)),E)).
223
224   EQ(EQ(E,INV(x)),EQ(x,E)).
225
226   EQ(EQ(E,ADD(INV(x),y)),EQ(ADD(x,INV(y)),E)).
227   EQ(EQ(E,ADD(Coeff(INV(x),y),z)),EQ(ADD(Coeff(x,y),INV(z)),E)).
228
229end_of_list.
230
231weight_list(pick_given).
232
233   weight(EQ(Coeff($(1),$(1)),E), -100).
234
235end_of_list.
236
237weight_list(purge_gen).
238
239   weight(MULT($(1),MULT($(1),MULT($(1),MULT($(1),$(1))))), 9999).
240   weight(ADD($(1),ADD($(1),ADD($(1),ADD($(1),ADD($(1),ADD($(1),$(1))))))), 9999).
241
242   weight(Coeff(Coeff($(1),$(1)),$(1)),9999).
243   weight(TID($(1),$(1),$(1)),9999).
244
245end_of_list.
246
247weight_list(terms).
248
249    % for equality ordering, want polynomial = term
250    weight(ADD($(1),$(1)),+10).
251
252end_of_list.
253