Not negation, read as 'not'
( (a=>b) And (b=>c) ) => (a=>c) |
In> CanProve(( (a=>b) And (b=>c) ) => (a=>c)) Out> True; |
Not ( Not x) --> x eliminate double negation x=>y --> Not x Or y eliminate implication Not (x And y) --> Not x Or Not y De Morgan's law Not (x Or y) --> Not x And Not y De Morgan's law (x And y) Or z --> (x Or z) And (y Or z) Distribution x Or (y And z) --> (x Or y) And (x Or z) Distribution |
(p1 Or p2 Or ...) And (q1 Or q2 Or ...) And ... |
(p Or Y) And ( Not p Or Z) --> (Y Or Z) |
As a last step, the algorithm negates the result again. This has the added advantage of simplifying the expression further.
In> CanProve(a Or Not a) Out> True; In> CanProve(True Or a) Out> True; In> CanProve(False Or a) Out> a; In> CanProve(a And Not a) Out> False; In> CanProve(a Or b Or (a And b)) Out> a Or b; |