lmc.ml

用ocaml编写的逻辑程序

(*mise sous form clausale*)

(*type des termes*)
type term=Var of int
          |Fun of int * term list;;

let x0=Var 0 and x1=Var 1;;              
               
let t1=Fun(0,[x0]);; (*f0(x0)*)
let t2=Fun(1,[x0;Fun(0,[x1])]);;(*f1(x0,f0(x1))*)

(*strinf_of_list:convertit une liste l en chaine de caracteres en utilisant la fonction string_of_elt pour convertir chaque element*)
 
let string_of_list string_of_elt l=
  let rec sofl=function 
      []->" "
      |x::[]->string_of_elt x
      |x::xs->(string_of_elt x)^","^(sofl xs)
      in sofl l;;
      
(*string_of_term:convertit un term en chaine de caractere*)

let rec string_of_term=function
  Var i->"x"^(string_of_int i)
  |Fun(i,[])->"f"^(string_of_int i)
  |Fun(i,lt)->"f"^(string_of_int i)^"("^(string_of_list string_of_term lt)^")"
;;

let print_term t=print_string(string_of_term t);;

     
(*type des formules du premier ordre*)               
type form=At of int*term list (*formule atomique*)
 |No of form (*negation*)
 |Et of form*form (*conjonction*)
 |Or of form*form (*disjonction*)
 |Imp of form*form (*implication*)
 |Equ of form*form (*equivalence*)
 |All of int*form (*quantification universelle*)
 |Ex of int*form(*quantification existentielle*)
;;


(*string_of_form:convertit une formule en chaine de caracteres*)


let rec string_of_form=function
						 At(i,l)->"P"^(string_of_int i)^"("^(string_of_list string_of_term l)^ ")"
						 |No(p)->"!"^(string_of_form p)
						 |Et(p,q)->(string_of_form p)^"&"^(string_of_form q)
						 |Or(p,q)->(string_of_form p)^"v"^(string_of_form q)
						 |Imp(p,q)->(string_of_form p)^"->"^(string_of_form q)
						 |Equ(p,q)->(string_of_form p)^"<->"^(string_of_form q)
						 |All(n,p)->"Ax"^(string_of_int n)^"["^(string_of_form p)^"]"
						 |Ex(n,p)->"Ex"^(string_of_int n)^"["^(string_of_form p)^"]"
;;

let print_form p=print_string(string_of_form p);;


(*il existe x0 pout tout x1 p0(f0(x1),f1(x0))*)
let p=Ex(0,(All(1,At(0,[Fun(0,[Var 1]);Fun(1,[Var 0])]))));;
let p1=Ex(0,(All(1,Or(At(0,[Fun(0,[Var 1]);Fun(1,[Var 0])]),At(1,[Fun(0,[Var 0]);Fun(1,[Var 1])])))));;
(*pour tout x0 il existe x1 p0(f0(x1),f1(x0))*)
let q=All(0,(Ex(1,At(0,[Fun(0,[Var 1]);Fun(1,[Var 0])]))));;
let s=Imp(p1,q);;
(*p->q*)
let p_imp_q=Imp(p,q);;
let s=Imp(p,q);;


(*declarer les litteraux positifs et negatifs*)
type lp=P of int;;
type ln=N of int;;


let p=P 1;;
let n=N 2;;
let p1=[P 1;P 2;P 3];;
let n1=[N 1;N 2;N 3];;



(*string_of_lp:convertit un litteraux positifs en chaine de caracteres*)
let string_of_lp1=function
         P i->"P"^(string_of_int i);;
let string_of_lp=function
         []->""
         |(P i)::lp1->"P"^(string_of_int i)^","^(string_of_list string_of_lp1 lp1 );;


(*string_of_ln:convertit un litteraux négatifs en chaine de caracteres*)
let string_of_ln1=function
           N i->"N"^(string_of_int i);;
let string_of_ln=function
         []->""
         |(N i)::ln1->"N"^(string_of_int i)^","^(string_of_list string_of_ln1 ln1);;



(*definition du type clause*)
type clause=Clause of int * lp list * ln list;;


let s=Clause(2,[P 1],[N 1]);;
let t=Clause(1,[P 1;P 2;P 3],[N 1;N 2;N 3]);;  
let r=Clause(3,[P 3;P 4;P 5;P 6],[N 2;N 4;N 6]);;          
       
(*string_of_clause:convertit une clause en chaine de caracteres*)
(*un petit problèle quand string_of_clause s ,obtenir string = "(2,[P1, ],[N1, ])"mais quand string_of_clause t ou r il marchent*)
let rec string_of_clause=function
     Clause(i,l1,l2)->"("^(string_of_int i)^","^"["^ (string_of_lp l1)^"]"^","^"["^(string_of_ln l2)^"]"^")"
;;

exception FormuleException;;
(*la fonction pour l'élimination des implications et déplacer les négation vers l'intérieur*)
let rec  elimi_depl s=match s with 
              At(i,l)->At(i,l)
              |Or(p,q)->Or(elimi_depl p,elimi_depl q)
              |Et(p,q)->Et(elimi_depl p,elimi_depl q)
              |Imp(p,q)->Or(elimi_depl (No p),elimi_depl q)
              |Equ(p,q)->Et(Or(elimi_depl (No p),elimi_depl q),Or(elimi_depl p,elimi_depl (No q)))
              |All(n,p)->All(n,elimi_depl p)
              |Ex(n,p)->Ex(n,elimi_depl p)
              |No(Imp(p,q))->Et(elimi_depl p,elimi_depl (No q))
              |No(No(p))->elimi_depl p
              |No(At(i,l))->No(At(i,l))
              |No(Et(p,q))->Or((elimi_depl (No p)),(elimi_depl (No q)))
              |No(Or(p,q))->Et((elimi_depl (No p)),(elimi_depl (No q)))
              |No(Ex(n,p))->All(n,(elimi_depl (No p)))
              |No(All(n,p))->Ex(n,(elimi_depl (No p)))
              |No(Equ(p,q))->Or(Et(elimi_depl (No p),elimi_depl q),Et(elimi_depl p,elimi_depl (No q)))
;;


 
(*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 "Or" de deux listes de clauses *)
let rec computeOr lc1 lc2 = match (lc1,lc2) with
                       |([],_) -> [] 
                       |(_,[]) -> []
                       |([]::_,_) -> lc2
                       |(_,[]::_) -> lc1
                       |(c1::reste1,_) ->(addHeadListe c1 lc2)@(computeOr reste1 lc2)
;;
(* mise sous forme clausale d'une form f *)
(* [] pas de clauses, implique f tautologie *)
(* [[]] clause vide, implique f antilogie *)
exception FormuleException;;
let rec clauses f = match f with
               At(i,l)->[[f]]
               |Et(p,q)-> (clauses p)@(clauses q)
               |Ex(n,p)->(clauses p)
               |All(n,p)->(clauses p)
               |Or(p,q) -> computeOr (clauses p) (clauses q)
               |Imp(p,q) ->computeOr (clauses p) (clauses q)
               |Equ(p,q)->(computeOr (clauses p) (clauses q))@(computeOr (clauses q) (clauses p))
               |No(At(i,l)) -> [[f]]
               |_-> raise FormuleException
(* f a des negations non elimi_depl*) 
;;

let gen_clauses f = clauses (elimi_depl f);;



(*unification*)

(*representation des substitutions*)

(*type des substitutions:liste de couple(i,t)
 Hypotheses:
 1-les variables sont triees par ordre croissant de leur indice
 2-un indice de variable n'apparait qu'une seule fois dans la liste*)
 
(*la definition de subst*)
type subst=(int*term) list;; 
let s=[(0,Var 1);(1,Fun(0,[Var 2]))];;


(*string_of_subst:convertit une substitution sigma en chaine de caracteres*)

let string_of_subst sigma=
 let string_of_redex(n,t)=
 string_of_term(Var n)^ "|->"^string_of_term t
 in "["^(string_of_list string_of_redex sigma)^"]"
;;


let print_subst sigma=print_string(string_of_subst sigma);;

(*reduct:donne le term associe a la variable n par la substitution sigma 
si la variable d'indice n appartient au domaine de sigma.sinon ,l'exception Not_Found est levee*)


(*retourn le sigma d'un terme de Var*)
let reduct n sigma=
   let rec reduct_rec=function
        []->raise Not_found
        |(n',t)::l->if n'=n then t else if n'<n then reduct_rec l else raise Not_found
        in reduct_rec sigma
;;


(*la fonction pour faire le sub dans la liste*)
let rec subs liste sub =match liste with
                 []->[]
                 |t::s1->match t with
                        Var c->if c=(fst sub) then (snd sub)::(subs s1 sub) else t::subs s1 sub
                        |Fun(e,d)->(Fun(e,subs d sub))::(subs s1 sub)
 ;;
let p=[x0;Fun(0,[x1]);Fun(1,[x0])];;
let sub=(0,x1);;
subs p sub;;
(*term list = [Var 1; Fun (0, [Var 1]); Fun (1, [Var 1])]*)


(*la fonction pour obtenir une substitution dans une liste de term *)
let rec substitut sub terme=match sub with
                  []->terme(*if sub est vide on obtient le terme*)
                  |(a,b)::s1->match terme with(*sub n'est pas vide,on parcour le terme*)
                             (*si le terme est Var et indice egal celui de sub*)
                              Var c->if a=c then substitut s1 b else substitut s1 terme
                              |Fun(e,d)->match d with
                                         []->substitut s1 terme
                                         |h::t->let x=Fun(e,subs d (a,b)) in substitut s1 x
 ;;
 let x2=Var 2;;
 let x3=Var 3;;
 let x4=Var 4;;
 let r=[(0,x2);(1,x3);(4,Fun(0,[x1]))];;
 
 substitut r  x4;;
 (*term = Fun (0, [Var 1])*)
 
let rec substitue sub terme=
                          let x=terme in 
                          let y=substitut sub terme
                          in if x=y then y else substitue sub y
 ;;
 substitue r x4;;
 (*term = Fun (0, [Var 3])*)
 
let x0=Var 0 and x1=Var 1;;   
let x2=Var 2;;           
               
let t1=Fun(0,[x0]);; (*f0(x0)*)
let t2=Fun(1,[x0;Fun(0,[x1])]);;(*f1(x0,f0(x1))*)

let suba = [(0,Var 1);(2,Fun (0,[Var 4]))];;
let subb = [(1,Var 2);(3,Fun (0,[Var 4]))];;
let subc = [(0,Var 1);(3,Var 4);(1,Var 3)];;
substitue subc x0;;(* term = Var 4*)
substitue suba x0;;(* term = Var 1*)
substitue suba x1;;(* term = Var 1*)
substitue suba t1;;(* term = Fun (0, [Var 1])*)
substitue suba t2;;(* term = Fun (1, [Var 1; Fun (0, [Var 1])])*)

let u = Fun (0,[Var 0 ;Fun (0,[Var 0;Var 1;Var 3]);Var 3]);;
let subtest = [(0,Var 1);(1,Fun(1,[Var 2]));(3,Var 5)];;
substitue subtest u;;