type boolean = 
  | True 
  | False
  | Var of int
  | Not of boolean
  | And of (boolean*boolean)
  | Or of (boolean*boolean)
  | Impl of (boolean*boolean)
  | Equiv of (boolean*boolean)

let rec string_of_boolean f = 
  let comp v f1 f2 = (string_of_boolean f1)^v^(string_of_boolean f2) in
  let par f1 = "("^f1^")" in match f with 
    True -> "True"
  | False-> "False"
  | Var i -> "x"^(string_of_int i)
  | Not f1 -> "~"^(par (string_of_boolean f1))
  | And (f1,f2) -> par (comp "/\\" f1 f2)
  | Or (f1,f2) -> par (comp "\\/" f1 f2)
  | Impl (f1,f2) -> par (comp "->" f1 f2)
  | Equiv (f1,f2) -> par (comp "<->" f1 f2)

let rec eval e f = match f with
  True -> true
| False -> false
| Var i -> List.nth e i
| Not f1 -> not (eval e f1)
| And (f1,f2) -> (eval e f1) && (eval e f2)
| Or (f1,f2) ->  (eval e f1) || (eval e f2)
| Impl (f1,f2) -> (eval e f2) || (not (eval e f1))
| Equiv (f1,f2) -> (eval e f1)=(eval e f2) 

eval [true;false;true] 
         (Impl (Or (And (Var 0,Var 1), Var 2), 
                Impl (Var 2,And (Var 0, Var 1))))

Per produrre la tabella, prima bisogna sapere il numero delle variabili:

let rec maxI f = match f with
     True -> 0
   | False -> 0
   | Var i -> i
   | Not f1 -> (maxI f1)
   | And (f1,f2) -> max (maxI f1) (maxI f2)
   | Or (f1,f2) -> max (maxI f1) (maxI f2)
   | Impl (f1,f2) -> max (maxI f1) (maxI f2)
   | Equiv (f1,f2) -> max (maxI f1) (maxI f2)

let table f = 
  let n = maxI f in
  (* Calcola il numero delle cifre di  k *)
  let rec digit k = if k < 10 then 1 else 1+digit (k/10) in
  (* Lunghezza di una casella *)
  let size = max 5 ((digit n)+1)  in
  (* Un bool come una stringa *)
  let string_of_bool b = if b then " true" else "false" in
  (* Indentazione per valori booleani *)
  let indent = (String.make (size-5) ' ')^"|" in
  (* Generazione della tabella *)
  let rec gen e k = match k with
    0 ->
      begin
        List.iter (fun x -> print_string (string_of_bool x); print_string indent) e;
        print_string (string_of_bool (eval e f)); print_newline();
      end
  | _ -> gen (false::e) (k-1);gen (true::e) (k-1) in
  (* Separatore *)
  let sep = String.make ((n+2)*(size+1)) '-' in
  (* Sep *)
  print_string sep; print_newline();
  (* Prima riga *)
  for i=0 to n do
    print_string (String.make (max 0 (size-((digit i)+1))) ' ');
    print_string "x"; print_int i; print_string "|";
  done;
  print_string (string_of_boolean f); print_newline();
  (* Sep *)
  print_string sep; print_newline();
  (* Tabella *)
  gen [] (n+1);
  (* Sep *)
  print_string sep; print_newline()

------------------
   x0|   x1|(x0/\x1)
------------------
false|false|false
 true|false|false
false| true|false
 true| true| true
------------------

let sat f = 
  let n = maxI f in
  let rec satn e k = match k with
    0 -> eval e f
  | _ -> if (satn (false::e) (k-1)) then true else satn (true::e) (k-1) 
  in
  satn [] (n+1)

let taut f = 
  let n = maxI f in
  let rec tautn e k = match k with
    0 -> eval e f
  | _ -> if (tautn (false::e) (k-1)) then (tautn (true::e) (k-1)) else false 
  in
  tautn [] (n+1)

ogni valutazione va bene, la formula è una tautologia.

*A8

non c'è tale valutazione, la formula è una tautologia.

*A9

la formula è equivalente a y, dunque y=false la rende vera.

*A10

la formula è equivalente a y, dunque y=false la rende falsa.

*A11

ogni valutazione va bene, la formula è una tautologia.

*A12

non c'è tale valutazione, la formula è una tautologia.

*A13

x	y	x∨¬y	x∧y	(x∨ ¬y) ⇒ (x ∧ y)
falso	falso	vero	vero	vero
falso	vero	vero	falso	falso
vero	falso	falso	falso	vero
vero	vero	vero	falso	falso

Problema delle N regine

let exactly_one i j n = 
  let rec  f k n1 = 
    if (n1=1) then (Not (Var k))
    else And (Not (Var k), f (k+j) (n1-1))
  in 
  let rec  g k n2 = 
    if (n2=1) then (Var k)
    else And (Impl (Var k, f (k+j) (n2-1)),
              Impl (Not (Var k), g (k+j) (n2-1)))
  in  g i n

let at_most_one i j n = 
  let rec  f k n1 = 
    if (n1=1) then (Not (Var k))
    else And (Not (Var k), f (k+j) (n1-1))
  in 
  let rec  g k n2 = 
    if (n2=2) then  Impl (Var k, f (k+j) (n2-1))
    else And (Impl (Var k, f (k+j) (n2-1)),Impl (Not (Var k), g (k+j) (n2-1)))
  in  if (n=1) then True else g i n

let gen_rows n = 
  let rec f k n1 = 
    if (n1=1) then exactly_one k 1 n
    else And(exactly_one k 1 n, f (k+n) (n1-1))
  in f 0 n

let gen_cols n = 
  let rec f k n1 =
    if (n1=1) then exactly_one k n n
    else And(exactly_one k n n, f (k+1) (n1-1))
  in f 0 n

let gen_diags n =
  let rec  f k n1 = 
      if (n1=1) then  at_most_one k (n-1) n
      else  And (And (And (at_most_one k (n+1) n1,
                          at_most_one k (n-1) (n-n1+1)),
                     And (at_most_one (n*n-k-1) (-(n+1)) n1,
                          at_most_one (n*n-k-1) (-(n-1)) (n-n1+1))),
                f (k+1) (n1-1))
  in 
    if (n=1) then True
    else And (at_most_one 0 (n+1) n, f 1 (n-1))

let chessboard n =
  if (n<2) then True
  else And (And (gen_rows n, gen_cols n), gen_diags n)

let rec expand f = match f with
  Var _ | True | False   -> f
| And(a,b) -> And(expand a, expand b)
| Or(a,b) -> Or(expand a, expand b)
| Not a -> Not (expand a)
| Impl(a,b) -> Or(Not (expand a),expand b)
| Equiv(a,b) -> And (Or(expand a,Not (expand b)),Or(Not (expand a),expand b))

let check_cnf f = 
  let rec only_neg f = match f with
    True | False | Var _ -> true
  | Not a -> only_neg a
  | _ -> false in
  let rec only_or f = match f with
    Or(a,b) -> (only_or a) && (only_or b)
  | _ -> only_neg f in
  let rec only_and f = match f with
    And(a,b) -> (only_and a) && (only_and b)
  | _ -> only_or f in
  only_and f

let rec push_neg f = match f with
  Or (a,b) -> Or (push_neg a, push_neg b)
| And (a,b) -> And (push_neg a, push_neg b)
| Not a -> rpush_neg a
| _ -> f
and
rpush_neg f = match f with
  Or (a,b) -> And (rpush_neg a, rpush_neg b)
| And (a,b) -> Or (rpush_neg a, rpush_neg b)
| Not a -> push_neg a
| True -> False
| False -> True
| _ -> Not f

let push_or f =
  let rec push_rules a b = match (a,b) with
    And (a1,a2), _ -> And (push_rules a1 b, push_rules a2 b)
  | _, And (b1,b2) -> And (push_rules a b1, push_rules a b2)
  |  _ -> Or (a,b) in
  let rec push f = match f with
    And (a,b) -> And (push a, push b)
  | Or (a,b) -> push_rules (push a) (push b)
  | _ -> f in
  push f

let cnf f = push_or (push_neg (expand f))

(* Il tipo dei valori: vero, falso, o sconosciuto *)
type value = 
    TRUE 
  | FALSE
  | NONE

(* Trovare il valore di una variable dentro la lista *)
let rec get_env e i = match (e,i) with
  (v::e1), 0 -> v
| (v::e1), _ -> get_env e1 (i-1)
| [], _ -> NONE

(* Il tipo del risultato della valutazione *)
type eval = 
  Satisfied 
| Contradiction 
| Vars of boolean list

let rec eval_disj e f = match f with 
  Var i ->
    begin
     match get_env e i with
       TRUE -> Satisfied
     | FALSE -> Contradiction
     | NONE -> Vars [Var i]
    end
| Not (Var i) ->
    begin
     match get_env e i with
       TRUE ->  Contradiction
     | FALSE -> Satisfied
     | NONE ->  Vars  [Not (Var i)]
    end
| Or (f1,f2) -> 
     begin 
       match eval_disj e f1 with
         Satisfied -> Satisfied 
       | Vars l1 ->
           begin 
             match eval_disj e f2 with
               Satisfied -> Satisfied
             | Contradiction -> Vars l1
             | Vars l2 -> Vars (List.append l1 l2)
           end
       | Contradiction -> eval_disj e f2
      end
| False -> Contradiction
| _ -> Satisfied

let rec eval_conj e f = match f with 
  And (f1, f2) ->
    begin
     match eval_conj e f1 with
       Contradiction -> Contradiction
     | Satisfied -> eval_conj e f2 
     | Vars l1 ->
         begin
           match eval_conj e f2 with 
             Satisfied -> Vars l1
           | Contradiction -> Contradiction
           | Vars l2 -> Vars (List.append l1 l2)
         end
    end
|  _ ->
         begin
           match eval_disj e f with
             Satisfied -> Satisfied
           | Contradiction -> Contradiction
           | Vars [v1] -> Vars [v1]
           | Vars _ -> Vars []
         end

(* Update della lista e all'indice i con il valore v
  Usa il tipo option per dire se questo update e' possible *)
let rec set_env e i v = match (e,i) with
  (NONE::e1), 0 -> Some (v::e1)
| (v1::e1), 0 -> if (v1=v) then (Some e) else None
| (v1::e1), _ -> 
    begin 
      match (set_env e1 (i-1) v) with
        None -> None
      | Some e2 -> Some (v1::e2)
    end
| [], _ -> set_env [NONE] i v

(* Da una lista costruisce due liste dove il primo NONE della
   lista iniziale e' stato rimpiazzato con TRUE e FALSE rispettivamente *)
let rec split_env e  = match e with
  []  -> [TRUE],[FALSE]
| NONE::e1 -> TRUE::e1, FALSE::e1
| v::e1 -> let l1,l2 = split_env e1 in
            v::l1,v::l2 

(* Assegna dentro e a v il valore TRUE *)
let set_var e v = match v with
  (Var i) -> set_env e i TRUE
| (Not (Var i)) -> set_env e i FALSE
| _ -> Some e

(* Assegna a tutte le variabili dentro l il valore TRUE *)
let rec set_vars e l = match l with
  [] -> Some e
| v::l1 ->
   begin 
     match set_var e v with
       None -> None
     | Some e1 -> set_vars e1 l1
   end


let rec davis f = 
  let rec  davisn e = match eval_conj e f with
    Satisfied -> true
  | Contradiction -> false
  | Vars [] -> 
      let e1,e2 = split_env e in
        if (davisn e1) then true else (davisn e2)
  | Vars l -> 
      begin
        match set_vars e l with
          None -> false
        | Some e1 -> davisn e1
      end
  in davisn []

(¬x ∨ z) ∧ (y ∨ z).

Algoritmo di Stålmarck

let rec transform f = match f with
  Var _ | True | False   -> f
| And(a,b) -> And (transform a, transform b)
| Or(a,b) -> Not (And (transform (Not a), transform (Not b)))
| Not a -> Not (transform a)
| Impl(a,b) -> Not (And (transform a, Not (transform b)))
| Equiv(a,b) -> Equiv (transform a, transform b)

(* Una tripla e' composta da 3 numeri relativi:
     True -> 1
     False-> -1
     (Var i)-> i+2
     (Not (Var i)) -> -(i+2) *)
type triplet = Andt of int*int*int | Equivt of int*int*int

(* Ritorna la variabile di testa e la lista di triplet *)
let make_triplets f = 
  (* la prima variabile disponibile *)
  let nvar = (maxI f)+3 in
  (* Espande implicazione e disgiunzione *)
  let f1= transform f in
  let rec iter f n l = match f with
    True -> 1,l,n
  | False -> -1,l,n
  | Var i -> i+2,l,n
  | Not f1 -> let i1,l1,n1 = iter f1 n l in -i1,l1,n1
  | And(f1,f2) ->
      let i1,l1,n1 = iter f1 n l in 
      let i2,l2,n2 = iter f2 n1 l1 in 
        n2,(Andt (n2,i1,i2))::l2,n2+1
  | Equiv(f1,f2) ->
      let i1,l1,n1 = iter f1 n l in 
      let i2,l2,n2 = iter f2 n1 l1 in 
        n2,(Equivt (n2,i1,i2))::l2,n2+1
  (* Impossibile *)
  | _ -> 1,l,n 
  in let i1,l1,n1=iter f1 nvar [] 
  in i1,l1

• get_min che, data una variabile segnata, restituisce la variabile di indice più piccolo uguale alla variabile data.
• get_class che, data una variabile segnata, restituisce la lista delle variabili uguali alla variabile data.
• add_eq che permette di aggiungere una equazione.
• is_contradictory che verifica che c'è una contraddizione nell'ambiente.

(* {v1=true,v2=-v3, v2=v5, v4=v6}
   come numeri interi (true->1, vi-> i+2)
   {2=1,3=-4,3=6,5=7} e' rappresentato come:
     [(1, Class [1,2]);
      (2, Ref 1);
      (3, Class [3,-4;6]);
      (4, Ref (-3));
      (5, Class [5,7]);
      (6, Ref (3));
      (7, Ref (5))]

*)

type tvalue = Ref of int | Class of int list
type env = (int*tvalue) list


(* Trovare il valore di una variabile dentro l'ambiente
   il valore di default e' Class[i] *)
let rec get_env e i = match e with
  ((j,v)::e1) -> if (i<j) then Class[i] else
                 if (j<i) then get_env e1 i else v
| [] -> Class [i]

(* Update dell'ambiente *)
let rec set_env e i v = match e with
  ((j,v1)::e1) -> if (i<j) then (i,v)::e else
                  if (j<i) then (j,v1)::set_env e1 i v else (i,v)::e1
| [] -> [(i,v)]

(* Ritorna il numero piu` piccolo (in valore assoluto) che e' uguale a v *)
let get_min e v = 
  if v>=0 then
    (match get_env e v with
       Ref i -> i
     | Class l -> v)
  else
    (match get_env e (-v) with
       Ref i -> -i
     | Class l -> v)

(* Ritorna la classe d'equivalenze *)
let rec get_class e v = 
  if 0<v then
    (match get_env e v with
       Ref i -> get_class e i
     | Class l -> l)
  else
    List.map (fun x -> -x)
    (match get_env e (-v) with
       Ref i -> get_class e i
     | Class l -> l)

(* Da' il segno di n: 1 se n>=0 altrimenti -1 *)
let sign n = if 0 <= n then 1 else -1

(* Fa un append di due liste ordinate *)
let rec merge_list l1 l2 = match (l1,l2) with
  _,[] -> l1
| [],_ -> l2
|(a::l1'),(b::l2') -> let res = (abs a)-(abs b) in
                      if res<0
                      then a::merge_list l1' l2
                      else if res=0
                      then a::merge_list l1' l2'
                      else b::merge_list l1 l2'


(* Usa l'indice 0 per dire se un ambiente e' una contraddizione *)
let make_contradictory e = set_env e 0 (Ref (-1))
let is_contradictory e = 
  match get_min e 0 with
    -1 -> true
  | _ -> false


(* Aggiunge una equazione all'ambiente. 
   Usa il tipo option per dire se e' possibile o no *)
let add_eq e v1 v2 = 
  let v1'= get_min e v1 in
  let v2'= get_min e v2 in
  if v1'=v2' then e else 
  if v1'= -v2' then make_contradictory e else 
  let v1'',v2'' =  if (abs v1') <= (abs v2')
                   then abs v1',(sign v1')*v2'
                   else abs v2',(sign v2')*v1'  in
  let l1 = get_class e v1'' in
  let l2 = get_class e v2'' in
  (* Tutti gli elementi di l2 devono puntare su v1''*)
  let e1 = List.fold_left (fun e1 v -> 
                   if 0<v then set_env e1 v (Ref v1'')
                   else set_env e1 (-v) (Ref (-v1''))) e l2 in
  (* La classe d'equivalenze di v1'' e' l'unione di l1 e l2 *)
  set_env e1 v1'' (Class (merge_list l1 l2)) 

let ttrue = 1
let tfalse = -1

let rec apply_rule tl e t = match t with
  Andt (v1,v2,v3) -> 
    let v1'=(get_min e v1) in
    let v2'=(get_min e v2) in
    let v3'=(get_min e v3) in
      if v1'=ttrue then propagate tl (propagate tl e v2' v3') v3' ttrue
      else if v2'=ttrue then propagate tl e v1' v3'
      else if v2'=tfalse then propagate tl e v1' tfalse
      else if v3'=ttrue then propagate tl e v1' v2'
      else if v3'=tfalse then propagate tl e v1' tfalse
      else if v1'= -v2' then propagate tl (propagate tl e  v1' v3') v3' tfalse
      else if v1'= -v3' then propagate tl (propagate tl e v1' v2') v2' tfalse
      else if v2'=v3' then propagate tl e v1' v2'
      else if v2'= -v3' then propagate tl e v1' tfalse
      else e
| Equivt (v1,v2,v3) -> 
    let v1'=(get_min e v1) in
    let v2'=(get_min e v2) in
    let v3'=(get_min e v3) in
      if v1'=ttrue then propagate tl e v2' v3'
      else if v1'=tfalse then propagate tl e v2' (-v3')
      else if v2'=ttrue then propagate tl e v1' v3'
      else if v2'=tfalse then propagate tl e v1' (-v3')
      else if v3'=ttrue then propagate tl e v1' v2'
      else if v3'=tfalse then propagate tl e v1' (-v2')
      else if v1'=v2' then propagate tl e v3' ttrue
      else if v1'= -v2' then propagate tl e v3' tfalse
      else if v1'=v3' then propagate tl e v2' ttrue
      else if v1'= -v3' then propagate tl e v2' tfalse
      else if v2'=v3' then propagate tl e v1' ttrue
      else if v2'= -v3' then propagate tl e v1' tfalse
      else e
and propagate tl e v1 v2 =
    let e1 = add_eq e v1 v2 in
    if is_contradictory e1 then e1 else
    if (e=e1) then e else 
    propagate_list tl e1 tl

and propagate_list tl e l = match l with
  [] -> e
| t::l1 -> let e1 = apply_rule tl e t in
             if is_contradictory e1 then e1
             else propagate_list tl e1 l1

(* Aggiunge ad e tutte le equazioni che sono vere per e1 ed e2  *)
let get_intersect e1 e2 e =
 let rec min_elt l1 l2 = match (l1,l2) with
   [],_ -> 0
 | _,[] -> 0 
 | (a1::l1'),(a2::l2') ->
     let res = (abs a1)-(abs a2) in
       if res<0
       then min_elt l1' l2
       else if 0<res
       then min_elt l1 l2'
       else if a1<>a2
       then min_elt l1' l2'
       else a1 in
 let rec inter e l1 l2 = match (l1,l2) with
   [],_ -> e
 | _,[] -> e
 | (i1,v1)::l1',(i2,v2)::l2' ->
     if (i1<i2) then inter e l1' l2
     else if (i2<i1) then inter e l1 l2' 
     else
        inter (add_eq e i1
                 (min_elt (get_class e1 i1) (get_class e2 i2)))
               l1' l2'  in

 if is_contradictory e1 then e2
 else if is_contradictory e2 then e1 
 else inter e e1 e2

let stal n f =
 let i,l = make_triplets f in
 let ai = abs i in
 let rec find_var e  m = 
   if ai<m then None
   else if m=(get_min e m) then Some m
   else find_var e (m+1) in
 (* Prova tutte le variabili *)
 let rec try_all e n m =
   match find_var e m with
     None -> e
  |  Some i ->
      let e1 = stalN n e i ttrue in
      let e2 = stalN n e i tfalse in
      let e3 = get_intersect e1 e2 e in
      if is_contradictory e3 then e3 
      else try_all e3 n (m+1) 
 and
  (* Itera fino a quando c'è una contraddizione o l'ambiente non cambia *)
  repeat_try_all e n = 
    let e1 = try_all e n 2 in
    if (is_contradictory e1) ||  e=e1 then e1
    else repeat_try_all e1 n
 and
  stalN n e v1 v2 = 
   let e1 = propagate l e v1 v2 in
   if (is_contradictory e1) || (n=0) then e1
   else repeat_try_all e1 (n-1) in
 if is_contradictory (stalN n [] i tfalse)
 then "Tautologia" else "Nessuna conclusione"