isTaut 2
抜けている条件があったので補ったら先程の論理式も正しく判定するようになった．やりましたね!
*Main> isTaut (Not (And (And (Or (Var 'x') (Var 'y')) (Or (Not (Var 'x')) (Var 'y'))) (And (Or (Var 'x') (Not (Var 'y'))) (Or (Not (Var 'x')) (Not (Var 'y')))))) Const True
data Prop = Const Bool | Var Char | Not Prop | Or Prop Prop | And Prop Prop | Imply Prop Prop deriving (Eq, Ord, Show) isTaut :: Prop -> Prop isTaut (Const b) = (Const b) isTaut (Var x) = (Var x) isTaut (Not p) = rule (Not (isTaut p)) isTaut (Or p1 p2) = rule (Or (isTaut p1) (isTaut p2)) isTaut (And p1 p2) = rule (And (isTaut p1) (isTaut p2)) isTaut (Imply p1 p2) = rule (Or (isTaut (Not p1)) (isTaut p2)) rule :: Prop -> Prop rule (Const b) = (Const b) rule (Not (Const b)) = (Const (not b)) rule (Or (Const b1) (Const b2)) = (Const (b1 || b2)) rule (And (Const b1) (Const b2)) = (Const (b1 && b2)) rule (Imply (Const b1) (Const b2)) = (Const (not b1 && b2)) rule (Var x) = (Var x) rule (Not (Not p)) = rule p rule (Not (Or p1 p2)) = rule (And (rule (Not (rule p1))) (rule (Not (rule p2)))) rule (Not (And p1 p2)) = rule (Or (rule (Not (rule p1))) (rule (Not (rule p2)))) rule (Or (Const True) p) = (Const True) rule (Or p (Const True)) = (Const True) rule (Or (Const False) p) = p rule (Or p (Const False)) = p rule (Or (Not p1) p2) | (rule p1) == (rule p2) = (Const True) rule (Or p1 (Not p2)) | p1 == p2 = (Const True) rule (Or p1 p2) | p1 == p2 = p1 rule (Or (Or p1 p2) p3) | p1 == p3 = rule (Or p2 p3) | p2 == p3 = rule (Or p1 p3) rule (Or (Or p1 p2) p3) | (p1 == (Not p3) || p2 == (Not p3)) = (Const True) rule (Or (Or p1 p2) p3) | ((Not p1) == p3 || (Not p2) == p3) = (Const True) rule (Or p1 (Or p2 p3)) | p1 == p2 = rule (Or p1 p3) | p1 == p3 = rule (Or p1 p2) rule (Or p1 (Or p2 p3)) | ((Not p1) == p2 || (Not p1) == p3) = (Const True) rule (Or p1 (Or p2 p3)) | (p1 == (Not p2) || p1 == (Not p3)) = (Const True) rule (Or (And p1 p2) p3) | (p1 == p3 || p2 == p3) = p3 rule (Or (And p1 p2) p3) | p1 == (Not p3) = rule (And p2 p3) | p2 == (Not p3) = rule (And p1 p3) rule (Or p1 (And p2 p3)) | (p1 == p2 || p1 == p3) = p1 rule (Or p1 (And p2 p3)) | (Not p1) == p3 = rule (And p1 p2) | (Not p2) == p3 = rule (And p1 p3) rule (Or (Or p1 p2) (Or p3 p4)) | (p1 == p3 || p2 == p3) = rule (Or (Or p1 p2) p4) | (p1 == p4 || p2 == p4) = rule (Or (Or p1 p2) p3) | ((Not p1) == p3 || (Not p2) == p3 || p1 == (Not p3) || p2 == (Not p3)) = (Const True) | ((Not p1) == p4 || (Not p2) == p4 || p1 == (Not p4) || p2 == (Not p4)) = (Const True) rule (Or (And p1 p2) (And p3 p4)) | p1 == p3 = rule (And p1 (Or p2 p4)) | p1 == p4 = rule (And p1 (Or p2 p3)) | p2 == p3 = rule (And p2 (Or p1 p4)) | p2 == p4 = rule (And p2 (Or p1 p3)) rule (Or (And p1 p2) (Or p3 p4)) | p1 == p3 = rule (Or p1 p4) | p1 == p4 = rule (Or p1 p3) | p2 == p3 = rule (Or p2 p4) | p2 == p4 = rule (Or p2 p3) | ((Not p1) == p3 || (Not p1) == p4) = rule (Or (Or p3 p2) p4) | ((Not p2) == p3 || (Not p2) == p4) = rule (Or (Or p3 p1) p4) | (p1 == (Not p3) || p1 == (Not p4)) = rule (Or (Or p3 p2) p4) | (p2 == (Not p3) || p2 == (Not p4)) = rule (Or (Or p3 p1) p4) rule (Or (Or p3 p4) (And p1 p2)) | p1 == p3 = rule (Or p1 p4) | p1 == p4 = rule (Or p1 p3) | p2 == p3 = rule (Or p2 p4) | p2 == p4 = rule (Or p2 p3) | ((Not p1) == p3 || (Not p1) == p4) = rule (Or (Or p3 p2) p4) | ((Not p2) == p3 || (Not p2) == p4) = rule (Or (Or p3 p1) p4) | (p1 == (Not p3) || p1 == (Not p4)) = rule (Or (Or p3 p2) p4) | (p2 == (Not p3) || p2 == (Not p4)) = rule (Or (Or p3 p1) p4) rule (And (Const False) p) = (Const False) rule (And p (Const False)) = (Const False) rule (And (Const True) p) = p rule (And p (Const True)) = p rule (And (Not p1) p2) | p1 == p2 = (Const False) rule (And p1 (Not p2)) | p1 == p2 = (Const False) rule (And p1 p2) | p1 == p2 = p1 rule (And (And p1 p2) p3) | p1 == p3 = rule (And p2 p3) | p2 == p3 = rule (And p1 p3) rule (And (And p1 p2) p3) | (p1 == (Not p3) || p2 == (Not p3)) = (Const False) rule (And (And p1 p2) p3) | ((Not p1) == p3 || (Not p2) == p3) = (Const False) rule (And p1 (And p2 p3)) | p1 == p2 = rule (And p1 p3) | p1 == p3 = rule (And p1 p2) rule (And p1 (And p2 p3)) | ((Not p1) == p2 || (Not p1) == p3) = (Const False) rule (And p1 (And p2 p3)) | (p1 == (Not p2) || p1 == (Not p3)) = (Const False) rule (And (Or p1 p2) p3) | (p1 == p3 || p2 == p3) = p3 rule (And (Or p1 p2) p3) | p1 == (Not p3) = rule (Or p2 p3) | p2 == (Not p3) = rule (Or p1 p3) rule (And p1 (Or p2 p3)) | (p1 == p3 || p1 == p2) = p1 rule (And p1 (Or p2 p3)) | (Not p1) == p3 = rule (Or p1 p2) | (Not p2) == p3 = rule (Or p1 p3) rule (And (And p1 p2) (And p3 p4)) | (p1 == p3 || p2 == p3) = rule (And (And p1 p2) p4) | (p1 == p4 || p2 == p4) = rule (And (And p1 p2) p3) | ((Not p1) == p3 || (Not p2) == p3 || p1 == (Not p3) || p2 == (Not p3)) = (Const False) | ((Not p1) == p4 || (Not p2) == p4 || p1 == (Not p4) || p2 == (Not p4)) = (Const False) rule (And (Or p1 p2) (Or p3 p4)) | p1 == p3 = rule (Or p1 (And p2 p4)) | p1 == p4 = rule (Or p1 (And p2 p4)) | p2 == p3 = rule (Or p2 (And p1 p4)) | p2 == p4 = rule (Or p2 (And p1 p3)) rule (And (Or p1 p2) (And p3 p4)) | p1 == p3 = rule (And p1 p4) | p1 == p4 = rule (And p1 p3) | p2 == p3 = rule (And p2 p4) | p2 == p4 = rule (And p2 p3) | ((Not p1) == p3 || (Not p1) == p4) = rule (And (And p2 p4) p3) | ((Not p2) == p3 || (Not p2) == p4) = rule (And (And p1 p4) p3) | (p1 == (Not p3) || p1 == (Not p4)) = rule (And (And p3 p2) p4) | (p2 == (Not p3) || p2 == (Not p4)) = rule (And (And p3 p1) p4) rule (And (And p3 p4) (Or p1 p2)) | p1 == p3 = rule (And p1 p4) | p1 == p4 = rule (And p1 p3) | p2 == p3 = rule (And p2 p4) | p2 == p4 = rule (And p2 p3) | ((Not p1) == p4 || (Not p1) == p3) = rule (And (And p2 p4) p3) | ((Not p2) == p4 || (Not p2) == p3) = rule (And (And p1 p4) p3) | (p1 == (Not p3) || p1 == (Not p4)) = rule (And (And p3 p2) p4) | (p2 == (Not p3) || p2 == (Not p4)) = rule (And (And p3 p1) p4) rule p = p
