% -*-Prolog-*- :- op(1050,xfx,('==>')). (P ==> Q) => (P => Q), (not(Q) => not(P)). or(P,Q) => (not(P) => Q), (not(Q) => P). prove_by_contradiction(P) :- P. prove_by_contradiction(P) :- \+ (not(P) ; P), add(not(P)), P -> rem(not(P)) ; (rem(not(P)),fail). => or(p,q). => (p ==> x). => (q ==> x). % try :- prove_by_contradiction(x).