Tautologie

let tautologie f =
  let n = nb_variables f in
  let v = Array.make n false in
  let rec essaie i =
    if i = n then evalue v f
    else begin
      v.(i) <- false;
      essaie (i + 1) && (v.(i) <- true; essaie (i + 1))
    end
  in
  essaie 0

Toute valuation doit rendre la formule vraie : le && exige les deux branches (x_i faux et vrai) et s'arrête au premier échec. tautologie (Ou (Var 0, Non (Var 0))) vaut true. On a aussi tautologie f = not (satisfiable (Non f)).