projet.txt

用ocaml编写的逻辑程序

(*type des termes*)

type term=Var of int
          |Fun of int * term list;;


(*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 substitutions:liste de couple(i,t)(cf sujet) 
 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*)
 

 type subst=(int * term) list;;

(*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*)

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 esle raise Not_found
        in reduct_rec sigma
;;




(*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)
 |Al(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);;