Équivalence

let equivalentes f g =
  let n =
    let a = var_max f and b = var_max g in (if a >= b then a else b) + 1
  in
  let v = Array.make n false in
  let rec verifie i =
    if i = n then evalue v f = evalue v g
    else begin
      v.(i) <- false;
      verifie (i + 1) && (v.(i) <- true; verifie (i + 1))
    end
  in
  verifie 0

On prend le nombre de variables couvrant les deux formules, puis on vérifie l'égalité evalue v f = evalue v g sur chaque valuation. C'est une tautologie déguisée (celle de f <-> g).