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