type binop = Et | Ou | Oubien | Impl | Equiv;; type formule = | Vrai | Faux | Var of string | Non of formule | Bin of binop * formule * formule;; (* Question 1 *) let rec affiche par f = match | Vrai -> print_string "1" | Faux -> print_string "0" | Var(x) -> print_string "x" | Non(g) -> print_string "Non("; affiche false g; print_string ")" | Bin(op,g,h) -> if par then print_string "("; affiche true g; print_string ( match op with | Et -> " . " | Ou -> " + " | Oubien -> " ++ " | Impl -> " => " | Equiv -> " <=> " ); affiche true h; if par then print_string ")" ;; (* par est vrai ssi f doit être entouré de parenthèses *) let print_formule f = affiche false f; print_newline ();; (* Question 2 *) let rec evalue f = match f with | Vrai -> true | Faux -> false | Var(x) -> failwith "la formule contient une variable" | Non(g) -> not(evalue g) | Bin(op,g,h) -> let a = evalue g and b = evalue h in match op with | Et -> a && b | Ou -> a || b | Oubien -> a <> b | Impl -> (not a) or b | Equiv -> a = b ;; (* Question 3 *) let rec subs x y f = match f with | Var(v) -> if v = x then y else f | Non(g) -> Non(subs x y g) | Bin(op,g,h) -> Bin(op, subs x y g, subs x y h) | _ -> f ;; (* Question 4 *) let rec simplifie f = match f with | Non(g) -> begin match (simplifie g) with | Vrai -> Faux | Faux -> Vrai | Non(h) -> h | h -> Non(h) end | Bin(op,g,h) -> begin match op, simplifie (g), simplifie (h) with | Et, Vrai, b -> b | Et, Faux, b -> Faux | Et, a, Vrai -> a | Et, a, Faux -> Faux | Ou, Vrai, b -> Vrai | Ou, Faux, b -> b | Ou, a, Vrai -> Vrai | Ou, a, Faux -> a | Oubien, Vrai, b-> b | Oubien, Faux, b-> Non(b) | Oubien, a, Vrai-> a | Oubien, a, Faux-> Non(a) | Impl, Vrai, b -> Vrai | Impl, Faux, b -> b | Impl, a, Vrai -> Non(a) | Impl, a, Faux -> Vrai | Equiv, Vrai, b -> b | Equiv, Faux, b -> Non(b) | Equiv, a, Vrai -> a | Equiv, a, Faux -> Non(a) | _,g,h -> Bin(op,g,h) end | _ -> f ;; (* Question 5 *) let rec tautologie f vars = match vars with | [] -> evalue(f) | x::suite -> tautologie (simplifie (subs x Vrai f)) suite & tautologie (simplifie (subs x Faux f)) suite ;; (* Question 6 *) let rec tautologieBis f vars = match vars with | [] -> (evalue f, []) | x::suite -> match tautologieBis (subs x Vrai f) suite with | (false,l) -> (false,(x^"=Vrai")::l) | (true,_) -> match tautologieBis (subs x Faux f) suite with | (false,l) -> (false,(x^"=Vrai")::l) | (true,_) -> (true,[]) ;; (* Question 7: Une conjonction de clauses est une tautologie ssi chacune des clauses est une tautologie. Une clause est une tautologie ssi il existe une variable x telle que Var(x) et Non(Var(x)) apparaissent dans la clause. La nouvelle fonction de tautologie réalisera ces tests. *)