clausal.ml

用ocaml编写的逻辑程序

(* Mise sous forme clausale d'une formule *)

type binconn = Et | Ou | Impl | Equiv;;(*FORM*)
type formule =
| Const of bool (* valeur constante *)
| Var of string (* variable *)
| Bin of binconn * formule * formule (* con. binaire *)
| Non of formule (* con. unaire *)

;;
exception FormuleException;;
(* fait descendre les negations *)
let rec descente f = match f with
Const _ -> f
| Var _ -> f

| Bin(Ou,f1,f2)->Bin(Ou,descente f1,descente f2)
| Bin(Et,f1,f2)->Bin(Et,descente f1,descente f2)
| Bin(Impl,f1,f2)->Bin(Ou,descente(Non f1),descente f2)
| Bin(Equiv,f1,f2)->Bin(Et,(Bin(Ou,descente(Non f1),descente f2)),(Bin(Ou,descente (Non f2),descente f1)))
| Non (Non f1) -> descente (f1)
| Non (Var _) -> f
| Non (Bin(Et,f1,f2)) ->Bin(Ou,descente (Non f1), descente (Non f2))
| Non (Bin(Ou,f1,f2)) ->Bin(Et,descente (Non f1), descente (Non f2))
| Non (Bin(Impl,f1,f2)) ->Bin(Et,descente ( f1), descente (Non f2))
| Non (Bin(Equiv,f1,f2))->Bin(Ou,Bin(Et,descente( f1),descente(Non f2)),Bin(Et,descente(f2),descente(Non f1)))
|Non _ -> raise FormuleException
;;
(* ajoute une liste en tete de chaque liste *)
(* d'une liste de listes *)
let addHeadListe l ll =
List.map (function l1 -> l@l1) ll;;
(* calcule le ``ou'' de deux listes de clauses *)
let rec computeOr lc1 lc2 = match (lc1,lc2) with
| ([],_) -> [] (* [] <-> liste vide, tautologie *)
| (_,[]) -> []
(* simplification ici, *)
(* [[],...] <-> préesence de la clause vide *)
| ([]::_,_) -> lc2
| (_,[]::_) -> lc1
| (c1::reste1,_) ->
(addHeadListe c1 lc2)@(computeOr reste1 lc2)
;;
(* on peut l'améliorer en testant les receptitions *)
(* exception si la formule comporte des negations *)
(* non descendues *)
exception FormuleException;;
(* mise sous forme clausale d'une formule f *)
(* [] pas de clauses, implique f tautologie *)
(* [[]] clause vide, implique f antilogie *)
let rec clauses f = match f with
Const b -> if (b) then [] else [[]]
| Var _ -> [[f]]
| Bin(Et,f1,f2) -> (clauses f1)@(clauses f2)
| Bin(Ou,f1,f2) -> computeOr (clauses f1) (clauses f2)
| Bin(Impl,f1,f2) ->computeOr (clauses f1) (clauses f2)
| Bin(Equiv,f1,f2)->(computeOr (clauses f1) (clauses f2))@(computeOr (clauses f2) (clauses f1))
| Non (Var _) -> [[f]]
| Non _ -> raise FormuleException
(* f a des negations non descendues *)
;;
let make_clauses f = clauses (descente f);;
(* test sur un exemple *)
let f = Non ( Bin(Et, Bin(Ou, Var "p", Var "q"), Var "r"));;
make_clauses f;;
let d= Bin(Impl,Var"x",Var"y");;
make_clauses d;;
let r=Bin(Equiv,Var"x",Var"y");;
make_clauses r;;
let w= Bin(Impl,Bin(Ou, Var"x",Var"y"),Bin(Et,Var"u",Var"v"));;
make_clauses w;;
let c=Bin(Impl,Bin(Impl,Bin(Et,Var"m",Var "n"),Bin(Ou, Var"x",Var"y")),Bin(Et,Var"u",Var"v"));;
make_clauses c;;
(* [[Non (Var "p"); Non (Var "r")]; *)
(* [Non (Var "q"); Non (Var "r")]] *)

(* entree-sortie a l'aide de Genlex *)
open Genlex;;
let mon_lexer s =
make_lexer ["non";"et";"ou";"(";")"](Stream.of_string s);;
(* entree des formules sous formes de chaines
de caracteres, avec une forme preefixe *)