type variavel = string type formula = Implica of formula*formula Equivale of formula*formula Ou of formula*formula E of formula*formula Nao of formula Var of variavel Verdade Falso (* Função (recursiva estrutural) de conversão de expressões para strings *) let rec string_of_formula form = match form with Var v -> v Verdade -> "TRUE" Falso -> "FALSE" Implica(f, g) -> ("( "^ string_of_formula f ^ " -> " ^ string_of_formula g ^" )") Equivale(f, g) -> ("( "^ string_of_formula f ^ " <-> " ^ string_of_formula g ^" )") E(f, g) -> ("( "^ string_of_formula f ^ " & " ^ string_of_formula g ^" )") Ou(f, g) -> ("( "^ string_of_formula f ^ " | " ^ string_of_formula g ^" )") Nao f -> ("!"^ string_of_formula f ) type literal = Bot Top V of variavel N of variavel type fnc = literal list list (* alínea 3 *) let rec implfree f = match f with Implica (g, h) -> Ou ((Nao (implfree g)),(implfree h)) Equivale (g, h) -> E ((Ou (Nao (implfree g),(implfree h))), (Ou (Nao (implfree h),(implfree g)))) E (g, h) -> E (implfree g, implfree h) Ou (g, h) -> Ou (implfree g, implfree h) Nao g -> Nao (implfree g) _ -> f ;; let rec nnfc f = match f with Nao (Nao g) -> nnfc g Nao (E (g,h)) -> Ou (nnfc (Nao g), nnfc (Nao h)) Nao (Ou (g,h)) -> E (nnfc (Nao g), nnfc (Nao h)) E (g, h) -> E (nnfc g, nnfc h) Ou (g, h) -> Ou (nnfc g, nnfc h) _ -> f ;; let rec distr f g = match (f,g) with (E (h,i), _ ) -> E ((distr h g), (distr i g)) (_ , E (h,i)) -> E ((distr f h), (distr f i)) _ -> Ou (f,g) let rec cnfc f = match f with Ou (g,h) -> distr (cnfc g) (cnfc h) E (g,h) -> E (cnfc g, cnfc h) _ -> f ;; let t f = cnfc (nnfc (implfree f));; let rec to_fnc_aux_ou f = match f with Ou ((Ou (g,h)), (Ou (i,j))) -> to_fnc_aux_ou (Ou (g,h)) @ to_fnc_aux_ou (Ou (i,j)) Ou (Var g, Ou (i,j)) -> V g::to_fnc_aux_ou (Ou (i,j)) Ou ((Ou (g,h)), Var i) -> to_fnc_aux_ou (Ou (g,h)) @ [V i] Ou (Nao (Var g), Ou (i,j)) -> N g::to_fnc_aux_ou (Ou (i,j)) Ou ((Ou (g,h)), Nao (Var i)) -> to_fnc_aux_ou (Ou (g,h)) @ [N i] Ou (g,h) -> (to_fnc_aux_ou g) @ (to_fnc_aux_ou h) Nao (Var x) -> [N x] Var x -> [V x] Verdade -> [Top] Falso -> [Bot] _ -> failwith "to_fnc_aux_ou: Formato invalido" ;; let rec to_fnc_aux f = match f with E (E (g,h),E (i,j)) -> to_fnc_aux (E (g,h)) @ to_fnc_aux (E (i,j)) E (Ou (g,h),E (i,j)) -> to_fnc_aux_ou (Ou (g,h)) :: to_fnc_aux (E (i,j)) E (E (g,h),Ou (i,j)) -> to_fnc_aux (E (g,h)) @ [to_fnc_aux_ou (Ou (i,j))] E (Ou (g,h),Ou (i,j)) -> [to_fnc_aux_ou (Ou (g,h));to_fnc_aux_ou (Ou (i,j))] Ou _ -> [to_fnc_aux_ou f] Nao _ -> [to_fnc_aux_ou f] Var _ -> [to_fnc_aux_ou f] Verdade -> [to_fnc_aux_ou f] Falso -> [to_fnc_aux_ou f] _ -> failwith "to_fnc_aux: Formato invalido" let to_fnc f = to_fnc_aux (t f);; (* (* (A/\ C) -> (~(B-> ~A) \/ (C /\ ~D) *) let exemplo = Implica (E (Var "A",Var "C"), Ou (Nao (Implica (Var "B", Nao (Var "A"))), E(Var "C", Nao (Var "D"))));; let ex = t exemplo;; (string_of_formula exemplo);; (string_of_formula ex);; let res = to_fnc exemplo;; *)
This document was generated using caml2html