1/* Tests on logic */ 2 3/* Small theorem prover for propositional logic, based on the 4 * resolution principle. 5 * Written by Ayal Pinkus, based on the simple theorem prover from "Prolog, Ivan Bratko, chapter 20" 6 * Version 0.1 initial implementation. 7 * 8 * 9 * Examples: 10CanProve(( (a=>b) And (b=>c)=>(a=>c) )) <-- True 11CanProve(a Or Not a) <-- True 12CanProve(True Or a) <-- True 13CanProve(False Or a) <-- a 14CanProve(a And Not a) <-- False 15CanProve(a Or b Or (a And b)) <-- a Or b 16 */ 17 18RuleBase("=>",{a,b}); 19 20 21/* 22 Simplify a boolean expression. CNF is responsible 23 for converting an expression to the following form: 24 (p1 Or p2 Or ...) And (q1 Or q2 Or ...) And ... 25 That is, a conjunction of disjunctions. 26*/ 27 28 29// Trivial simplifications 3010 # CNF( Not True) <-- False; 3111 # CNF( Not False) <-- True; 3212 # CNF(True And (_x)) <-- CNF(x); 3313 # CNF(False And (_x)) <-- False; 3414 # CNF(_x And True) <-- CNF(x); 3515 # CNF(_x And False) <-- False; 3616 # CNF(True Or (_x)) <-- True; 3717 # CNF(False Or (_x)) <-- CNF(x); 3818 # CNF((_x) Or True ) <-- True; 3919 # CNF((_x) Or False) <-- CNF(x); 40 41// A bit more complext 4221 # CNF(_x Or _x) <-- CNF(x); 4322 # CNF(_x And _x) <-- CNF(x); 4423 # CNF(_x Or Not (_x)) <-- True; 4514 # CNF(Not (_x) Or _x) <-- True; 4625 # CNF(_x And Not (_x)) <-- False; 4726 # CNF(Not (_x) And _x) <-- False; 48 49// Simplifications that deal with (in)equalities 5025 # CNF(((_x) == (_y)) Or ((_x) !== (_y))) <-- True; 5125 # CNF(((_x) !== (_y)) Or ((_x) == (_y))) <-- True; 5226 # CNF(((_x) == (_y)) And ((_x) !== (_y))) <-- False; 5326 # CNF(((_x) !== (_y)) And ((_x) == (_y))) <-- False; 54 5527 # CNF(((_x) >= (_y)) And ((_x) < (_y))) <-- False; 5627 # CNF(((_x) < (_y)) And ((_x) >= (_y))) <-- False; 5728 # CNF(((_x) >= (_y)) Or ((_x) < (_y))) <-- True; 5828 # CNF(((_x) < (_y)) Or ((_x) >= (_y))) <-- True; 59 60// some things that are more complex 61120 # CNF((_x) Or (_y)) <-- LogOr(x, y, CNF(x), CNF(y)); 6210 # LogOr(_x,_y,_x,_y) <-- x Or y; 6320 # LogOr(_x,_y,_u,_v) <-- CNF(u Or v); 64 65130 # CNF( Not (_x)) <-- LogNot(x, CNF(x)); 6610 # LogNot(_x, _x) <-- Not (x); 6720 # LogNot(_x, _y) <-- CNF(Not (y)); 68 6940 # CNF( Not ( Not (_x))) <-- CNF(x); // eliminate double negation 7045 # CNF((_x)=>(_y)) <-- CNF((Not (x)) Or (y)); // eliminate implication 71 7250 # CNF( Not ((_x) And (_y))) <-- CNF((Not x) Or (Not y)); // De Morgan's law 7360 # CNF( Not ((_x) Or (_y))) <-- CNF(Not (x)) And CNF(Not (y)); // De Morgan's law 74 75/* 7670 # CNF((_x) And ((_y) Or (_z))) <-- CNF(x And y) Or CNF(x And z); 7770 # CNF(((_x) Or (_y)) And (_z)) <-- CNF(x And z) Or CNF(y And z); 78 7980 # CNF((_x) Or ((_y) And (_z))) <-- CNF(x Or y) And CNF(x Or z); 8080 # CNF(((_x) And (_y)) Or (_z)) <-- CNF(x Or z) And CNF(y Or z); 81*/ 82 8370 # CNF(((_x) And (_y)) Or (_z)) <-- CNF(x Or z) And CNF(y Or z); // Distributing Or over And 8480 # CNF((_x) Or ((_y) And (_z))) <-- CNF(x Or y) And CNF(x Or z); 85 8690 # CNF((_x) And (_y)) <-- CNF(x) And CNF(y); // Transform subexpression 87 88101 # CNF( (_x) < (_y) ) <-- Not CNFInEq(x >= y); 89102 # CNF( (_x) > (_y) ) <-- CNFInEq(x > y); 90103 # CNF( (_x) >= (_y) ) <-- CNFInEq(x >= y); 91104 # CNF( (_x) <= (_y) ) <-- Not CNFInEq(x > y); 92105 # CNF( (_x) == (_y) ) <-- CNFInEq(x == y); 93106 # CNF( (_x) !== (_y) ) <-- Not CNFInEq(x == y); 94 95111 # CNF( Not((_x) < (_y)) ) <-- CNFInEq( x >= y ); 96113 # CNF( Not((_x) <= (_y)) ) <-- CNFInEq( x > y ); 97116 # CNF( Not((_x) !== (_y)) ) <-- CNFInEq( x == y ); 98 99/* Accept as fully simplified, fallthrough case */ 100200 # CNF(_x) <-- x; 101 10220 # CNFInEq((_xex) == (_yex)) <-- (CNFInEqSimplify(xex-yex) == 0); 10320 # CNFInEq((_xex) > (_yex)) <-- (CNFInEqSimplify(xex-yex) > 0); 10420 # CNFInEq((_xex) >= (_yex)) <-- (CNFInEqSimplify(xex-yex) >= 0); 10530 # CNFInEq(_exp) <-- (CNFInEqSimplify(exp)); 106 10710 # CNFInEqSimplify((_x) - (_x)) <-- 0; // strictly speaking, this is not always valid, i.e. 1/0 - 1/0 != 0... 108100# CNFInEqSimplify(_x) <-- [/*Echo({"Hit the bottom of CNFInEqSimplify with ", x, Nl()});*/ x;]; 109 // former "Simplify"; 110 111// Some shortcuts to match prev interface 112CanProveAux(_proposition) <-- LogicSimplify(proposition, 3); 11310 # LogicSimplify(_proposition, _level)_(level<2) <-- CNF(proposition); 114 11520 # LogicSimplify(_proposition, _level) <-- 116[ 117 Local(cnf, list, clauses); 118 Check(level > 1, "Wrong level"); 119 // First get the CNF version of the proposition 120 Set(cnf, CNF(proposition)); 121 122 If(level <= 1, cnf, [ 123 Set(list, Flatten(cnf, "And")); 124 Set(clauses, {}); 125 ForEach(clause, list) 126 [ 127 Local(newclause); 128 //newclause := BubbleSort(LogicRemoveTautologies(Flatten(clause, "Or")), LessThan); 129 Set(newclause, LogicRemoveTautologies(Flatten(clause, "Or"))); 130 If(newclause != {True}, DestructiveAppend(clauses, newclause)); 131 ]; 132 133 /* 134 Note that we sort each of the clauses so that they look the same, 135 i.e. if we have (A And B) And ( B And A), only the first one will 136 persist. 137 */ 138 Set(clauses, RemoveDuplicates(clauses)); 139 140 If(Equals(level, 3) And (Length(clauses) != 0), [ 141 Set(clauses, DoUnitSubsumptionAndResolution(clauses)); 142 Set(clauses, LogicCombine(clauses)); 143 ]); 144 145 Set(clauses, RemoveDuplicates(clauses)); 146 147 If(Equals(Length(clauses), 0), True, [ 148 /* assemble the result back into a boolean expression */ 149 Local(result); 150 Set(result, True); 151 ForEach(item,clauses) 152 [ 153 Set(result, result And UnFlatten(item, "Or", False)); 154 ]; 155 156 result; 157 ]); 158 ]); 159]; 160 161/* CanProve tries to prove that the negation of the negation of 162 the proposition is true. Negating twice is just a trick to 163 allow all the simplification rules a la De Morgan to operate 164 */ 165/*CanProve(_proposition) <-- CanProveAux( Not CanProveAux( Not proposition));*/ 166 167CanProve(_proposition) <-- CanProveAux( proposition ); 168 1691 # SimpleNegate(Not (_x)) <-- x; 1702 # SimpleNegate(_x) <-- Not(x); 171 172/* LogicRemoveTautologies scans a list representing e1 Or e2 Or ... to find 173 if there are elements p and Not p in the list. This signifies p Or Not p, 174 which is always True. These pairs are removed. Another function that is used 175 is RemoveDuplicates, which converts p Or p into p. 176*/ 177 178/* this can be optimized to walk through the lists a bit more efficiently and also take 179care of duplicates in one pass */ 180LocalCmp(_e1, _e2) <-- LessThan(ToString() Write(e1), ToString() Write(e2)); 181 182// we may want to add other expression simplifers for new expression types 183100 # SimplifyExpression(_x) <-- x; 184 185// Return values: 186// {True} means True 187// {} means False 188LogicRemoveTautologies(_e) <-- 189[ 190 Local(i, len, negationfound); Set(len, Length(e)); 191 Set(negationfound, False); 192 193 //Echo(e); 194 e := BubbleSort(e, "LocalCmp"); 195 196 For(Set(i, 1), (i <= len) And (Not negationfound), i++) 197 [ 198 Local(x, n, j); 199 // we can register other simplification rules for expressions 200 //e[i] := MathNth(e,i) /:: {gamma(_y) <- SimplifyExpression(gamma(y))}; 201 Set(x, MathNth(e,i)); 202 Set(n, SimpleNegate(x)); /* this is all we have to do because of 203 the kind of expressions we can have coming in */ 204 205 For(Set(j, i+1), (j <= len) And (Not negationfound), j++) [ 206 Local(y); 207 Set(y, MathNth(e,j)); 208 209 If(Equals(y, n), 210 [ 211 //Echo({"Deleting from ", e, " i=", i, ", j=", j, Nl()}); 212 213 Set(negationfound, True); 214 //Echo({"Removing clause ", i, Nl()}); 215 ], 216 If(Equals(y, x), 217 [ 218 //Echo({"Deleting from ", e, " j=", j, Nl()}); 219 DestructiveDelete(e, j); 220 Set(len,MathSubtract(len,1)); 221 ]) 222 ); 223 ]; 224 Check(len = Length(e), "The length computation is incorrect"); 225 ]; 226 227 If(negationfound, {True}, e); /* note that a list is returned */ 228]; 229 23010 # Contradict((_x) - (_y) == 0, (_x) - (_z) == 0)_(y != z) <-- True; 23112 # Contradict((_x) == (_y), (_x) == (_z))_(y != z) <-- True; 23213 # Contradict((_x) - (_y) == 0, (_x) - (_z) >= 0)_(z > y) <-- True; 23314 # Contradict((_x) - (_y) == 0, (_x) - (_z) > 0)_(z > y) <-- True; 23414 # Contradict(Not (_x) - (_y) >= 0, (_x) - (_z) > 0)_(z > y) <-- True; 23515 # Contradict(_a, _b) <-- Equals(SimpleNegate(a), b); 236 237/* find the number of the list that contains n in it, a pointer to a list of lists in passed */ 238LogicFindWith(_list, _i, _n) <-- 239[ 240 Local(result, index, j); 241 Set(result, -1); Set(index, -1); 242 243 For(j := i+1, (result<0) And (j <= Length(list)), j++) 244 [ 245 Local(k, len); Set(len, Length(list[j])); 246 For(k := 1, (result<0) And (k<=len), k++) 247 [ 248 Local(el); Set(el, list[j][k]); 249 250 If(Contradict(n, el), 251 [Set(result, j); Set(index, k);]); 252 ]; 253 ]; 254 {result, index}; 255]; 256 257/* LogicCombine is responsible for scanning a list of lists, which represent 258 a form (p1 Or p2 Or ...) And (q1 Or q2 Or ...) And ... by scanning the lists 259 for combinations x Or Y And Not x Or Z <-- Y Or Z . If Y Or Z is empty then this clause 260 is false, and thus the entire proposition is false. 261*/ 262LogicCombine(_list) <-- 263[ 264 Local(i, j); 265 For(Set(i,1), i<=Length(list), Set(i,MathAdd(i,1))) 266 [ 267 //Echo({"list[", i, "/", Length(list), "]: ", list[i], Nl()}); 268 269 For(j := 1, (j<=Length(list[i])), j++) 270 [ 271 Local(tocombine, n, k); 272 Set(n, list[i][j]); 273 274 {tocombine, k} := LogicFindWith(list, i, n);// search forward for n, tocombine is the list we 275 // will combine the current one with 276 If(tocombine != -1, 277 [ 278 Local(combination); 279 Check(k != -1, "k is -1"); 280 281 Set(combination, LogicRemoveTautologies(Concat(list[i], list[tocombine]))); 282 If(combination = {}, // the combined clause is false, so the whole thing is false 283 [Set(list, {{}}); Set(i, Length(list)+1);], [/*Set(i, 0);*/]); 284 ]); 285 ]; 286 ]; 287 list; 288]; 289 29010 # Subsumes((_x) - (_y) == 0, Not ((_x) - (_z)==0))_(y!=z) <-- True; 291// suif_tmp0_127_1-72==0 And 78-suif_tmp0_127_1>=0 29220 # Subsumes((_x) - (_y) == 0, (_z) - (_x) >= 0)_(z>=y) <-- True; 29320 # Subsumes((_x) - (_y) == 0, (_z) - (_x) > 0)_(z>y) <-- True; 294// suif_tmp0_127_1-72==0 And suif_tmp0_127_1-63>=0 29530 # Subsumes((_x) - (_y) == 0, (_x) - (_z) >= 0)_(y>=z) <-- True; 29630 # Subsumes((_x) - (_y) == 0, (_x) - (_z) > 0)_(y>z) <-- True; 297 29890 # Subsumes((_x), (_x)) <-- True; 299 300100# Subsumes((_x), (_y)) <-- False; 301 302 303// perform unit subsumption and resolutiuon for a unit clause # i 304// a boolean indicated whether there was a change is returned 305DoUnitSubsumptionAndResolution(_list) <-- 306[ 307 Local(i, j, k, isFalse, isTrue, changed); 308 Set(isFalse, False); 309 Set(isTrue, False); 310 Set(changed, True); 311 312 //Echo({"In DoUnitSubsumptionAndResolution", Nl()}); 313 314 While(changed) [ 315 Set(changed, False); 316 317 For(i:=1, (Not isFalse And Not isTrue) And i <= Length(list), i++) 318 [ 319 If(Length(list[i]) = 1, [ 320 Local(x); Set(x, list[i][1]); //n := SimpleNegate(x); 321 //Echo({"Unit clause ", x, Nl()}); 322 323 // found a unit clause, {x}, not use it to modify other clauses 324 For(j:=1, (Not isFalse And Not isTrue) And j <= Length(list), j++) 325 [ 326 If(i !=j, [ 327 Local(deletedClause); Set(deletedClause, False); 328 For(k:=1, (Not isFalse And Not isTrue And Not deletedClause) And k <= Length(list[j]), k++) 329 [ 330 // In both of these, if a clause becomes empty, the whole thing is False 331 332 //Echo({" ", x, " subsumes ", list[j][k], i,j, Subsumes(x, list[j][k]), Nl()}); 333 334 // unit subsumption -- this kills clause j 335 If(Subsumes(x, list[j][k]), [ 336 // delete this clause 337 DestructiveDelete(list, j); 338 j--; 339 If(i>j, i--); // i also needs to be decremented 340 Set(deletedClause, True); 341 Set(changed, True); 342 If(Length(list) = 0, [Set(isTrue, True);]); 343 ], 344 // else, try unit resolution 345 If(Contradict(x, list[j][k]), [ 346 //Echo({x, " contradicts", list[j][k], Nl()}); 347 DestructiveDelete(list[j], k); 348 k--; 349 Set(changed, True); 350 If(Length(list[j]) = 0, [Set(isFalse, True);]); 351 ]) 352 ); 353 ]; 354 ]); 355 ]; 356 ]); 357 ]; 358 ]; 359 360 list; 361];