let find_vars formula=
let rec find formula =
match formula with
Var alpha -> [alpha]
| Not alpha -> find alpha
| And (alpha,beta) -> (find alpha) @ (find beta)
| Or (alpha,beta) -> (find alpha) @ (find beta)
| Implicates (alpha,beta) -> (find alpha) @ (find beta)
| Equals (alpha,beta) -> (find alpha) @ (find beta)
| True -> []
| False -> []
in
let vars = find formula in
let rec eliminate vars =
match vars with
var :: vars ->
if List.exists (fun a -> a=var) vars then
eliminate vars
else
var :: (eliminate vars)
| [] -> []
in
eliminate vars