type atom = int;; type formule = |Faux |Atomic of atom |Non of formule |Et of (formule * formule) |Ou of (formule * formule) |Implique of (formule * formule) |Equiv of (formule * formule);; exception Mauvais_numero;; let rec nieme k liste = match liste with |[] -> raise Mauvais_numero |t::q -> if k=0 then t else nieme (k-1) q;; let rec eval formule env = match formule with |Faux -> false |Atomic a -> nieme a env |Non p -> if (eval p env) then false else true |Et (p,q) -> if (eval p env) then if (eval q env) then true else false else false |Ou (p,q) -> if (eval p env) then true else if (eval q env) then true else false |Implique (p,q) -> eval (Ou(Non p,q)) env |Equiv (p,q) -> eval (Et(Implique(p,q),Implique(q,p))) env;; (* |Equiv(p,q) -> max2 (borne_var p) (borne_var q)*) let rec concat l1 l2 = match l1 with |[] -> l2 |t::q -> t::(concat q l2);; let rec ajoute_el el liste_de_listes = match liste_de_listes with |[] -> [] |t::q -> (el::t)::(ajoute_el el q);; let rec tous_environnements n = match n with |0 -> [[]] |n -> concat (ajoute_el true (tous_environnements (n-1))) (ajoute_el false (tous_environnements (n-1)) );; let est_tautologie formule n = let liste = tous_environnements n in let rec test f = match f with |[] -> true |t::q -> (eval formule t) & (test q) in test liste;; let dm = Equiv(Non(Et(Atomic 0,Atomic 1)) , Ou(Non(Atomic 0),Non(Atomic 1)));; est_tautologie dm;; let rec dit_formule formule = match formule with |Faux -> "Faux" |Non Faux -> "Vrai" |Atomic a -> string_of_int a |Non p -> "non " ^ dit_formule p |Et(p,q) -> "( " ^ dit_formule p ^ " et " ^ dit_formule q ^ " )" |Ou(p,q) -> "( " ^ dit_formule p ^ " ou " ^ dit_formule q ^ " )" |Implique(p,q) -> "( " ^ dit_formule p ^ " implique " ^ dit_formule q ^ " )" |Equiv(p,q) -> "( " ^ dit_formule p ^ " equivalent a " ^ dit_formule q ^ " )";;