projetlmc.ml

用ocaml编写的逻辑程序

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

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

type form = At of int * term list (*formule atomique*)
	| No of form (* negation *)
	| And 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*) ;;

(*il exite x pour tout x p0(f0(x1),f1(x0))*)
let p = Ex(0,(All(1,At(0,[Fun (0,[Var 1]); Fun (1,[Var 0])])))) ;;
(*pour tout x il existe x1p0(f0(x1),f1(x0)) *)
let q = All(0,(Ex(1,At(0,[Fun (0,[Var 1]); Fun (1,[Var 0])])))) ;;
(*p->q*)
let p-imp-q = Imp(p,q);;

type subst = (int * term) list;;
(*{x0|x1,x1|f0(x2)}*)

let rec substitue sub terme = 
                let x = terme in 
                let y = substit sub terme
			    in if(x = y) then y else substitue sub y;;

let rec substit sub terme = match sub with
		[] -> terme
		|(a,b)::xs -> match terme with 
				Var (c) -> if(a = c) then substit xs b else substit xs terme
				|Fun (e,d) -> match d with
						[] -> substit xs terme   
						|h::t -> let x = Fun(e, subs d (a,b)) in substit
 xs x;;
 			      
                                                 Fun(e, subs(d, ab)


let rec subs liste sub = match liste with 
			[] -> []
			|t::xs -> match t with
					|Var (c) -> if(c = (fst sub)) then (snd sub)::(subs xs sub) else t::subs xs sub
					|Fun (e,d) -> (Fun(e,subs d sub))::(subs xs sub);;

let x0 = Var 0;;
let x1 = Var 1;;
let x2 = Var 2;;
let t1 = Fun (0,[x0]);;
let t2 = Fun (1,[x0; Fun (0,[x2])]);;
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;;
substitue suba x0;;
substitue suba x1;;
substitue suba t1;;
substitue suba t2;;

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;;

(*La fonction compose nous permet de calculer la substitution par composition de 2 substitutions*) 
let rec teste terme sub = match sub with
			  [] -> true
			  |x::xs -> if(fst(x) = fst(terme)) && (snd(x) <> snd(terme)) then 
						false else
						teste terme xs ;;

let rec testeSub sub1 sub2 = match sub1,sub2 with
			[],[] -> true
			|t::xs,[] -> true
			|[],t::xs -> true
			|q1::xs1,q2::xs2 -> let x = teste q1 sub2 in if (x) then testeSub xs1 sub2 							else failwith "Erreur pour les 2 listes de 							substitutions";; 
(*testeSub suba subb;; pour tester la fonction testeSub*)
		
let rec comp sub1 sub2 = match sub1,sub2 with
				[],[] -> []
				|[],t::xs -> []
				|t::xs,[] -> []
				|q1::xs1,q2::xs2 ->let a = fst(q1) in let b = snd(q1) in 
				let x =substitue sub2 b in if(b = x) then (a,b)::comp xs1 	sub2 
				else let y = substitue sub1 x in (a,y)::comp 	xs1 sub2;;

let rec compose sub1 sub2 = match sub1,sub2 with
				[],[] -> []
				|[],t::xs -> sub2
				|t::xs,[] -> sub1
				|q1::xs1,q2::xs2 ->let z = testeSub sub1 sub2 in if (z) then 
				let x = comp sub1 sub2 in let y = comp sub2 sub1 in x@y 
				else 	failwith "Impossible de composer deux substitutions";;


let rec subone sub listsub = match listsub with
				[] -> sub::[]
				|t::q -> (match t with
					 (a,b) -> (match b with
						 	Var (c) -> if(c = (fst sub)) then (a,snd sub)::(subone sub q) else t::(subone sub q)
							|Fun (d,e) ->(a,Fun(d,substitueliste sub e))::(subone sub q)));; 

let rec substitueliste sub lterme = match lterme with 
					[] -> []
					|t::q -> (substitue [sub] t)::(substitueliste sub q);;



let rec compose (sub1:subst) (sub2:subst) = match sub1,sub2 with
				[],[] -> []
				|[],t::xs -> sub2
				|t::xs,[] -> sub1
                |q1::xs1,q2::xs2 -> compose xs1 (subone q1 sub2) ;; 



let suba = [(0,Var 1);(2,Fun (0,[Var 4]))];;
let subb = [(1,Var 2);(3,Fun (0,[Var 4]))];;						  
(*compose suba subb;;
compose [] subb;; tester pour la fonction de compose*)

(*Retourne le pgu d'un systeme d'équations (liste de paires de termes) en parametre deux listes de termes*)

let rec elimination (sub:subst) lterme = match lterme,sub with
 				[],[]-> []
				|[],t::q -> []
				|t::q,[] -> []
				|t::q,t1::q1 -> (match t,t1 with 
					(a,b),(c,d)-> if d = (Var a) then (c,b)::(elimination sub q) else (a,b)::(elimination sub q));;

let rec testeOcc num sub = match sub with
			[] -> false
			|t::q -> if (fst t) = num then let x = testOccurrence (fst t) [snd t] in
			x||testeOcc num q else testeOcc num q;;  


let rec occurcheck listesub = match listesub with
			[] -> []
			|t::xs -> (testeOcc (fst t) (elimination [t] xs))::(occurcheck xs);;

let rec result list = match list with
			[] -> false
			|t :: xs -> t||result xs;;

let occurcheckfinal liste = result (occurcheck liste);;
					
let rec unifie_sys lterme1 lterme2 sub = 
                                    let x = 
                                    unifie_s lterme1 lterme2 in let y = 							
                                    nettoyage x in let z = 
                                    occurcheckfinal (compose y sub) in if(z) then [] else (compose y sub);;
 
(*La fonction Nettoyage nous permet de Nettoyer la liste par exemple [(0,Var 1),(0,Var 1)],on supprime un element (0,Var 1)*)
let rec nettoyage listesub = match listesub with 
			[] -> []
			|x::xs -> let y = recherche x xs in if (y) then (let z = suppression x xs 				
			                                     	in nettoyage z@[x]) else x::nettoyage xs;;

(*La fonction suppression nous permet de supprimer un element dans une liste*) 
let rec suppression e l = match l with
			[] -> []
			|x::xs -> if(x = e) then xs else x::(suppression e xs);;

(*La fonction recherche nous permet de rechercher un element dans une liste *)
let rec recherche e l = match l with
			[] -> false
			|x::xs -> if (((fst e) = (fst x)) && ((snd e) = (snd x))) then true else 						
			recherche e xs;;

let rec unifie_s lterme1 lterme2 = match lterme1,lterme2 with
					[],[] -> [] 
					|[],t::xs -> failwith "Impossible dans le cas l2 est different que l1"
					|t::xs,[] -> failwith "Impossible dans le cas l1 est different que l2"
					|p1::xs1,p2::xs2 -> let x = unifie p1 p2 in x@unifie_s xs1 xs2 ;;

let u = [Var 0;Fun(0,[Var 2]);Var 3];;
let v = [Var 1;Fun(0,[Var 3]);Var 4];;
(*Retourne le pgu de deux termes t et t'*)
let rec unifie terme1 terme2 = match terme1,terme2 with
				Var (a),Var (b) -> if (a <> b) then (a,Var b)::[] else []
				|Var (a),Fun (b,c) -> let x = testOccurrence a c in if(x) then 					(*changer*)failwith "Erreur de teste d'occurrence" else (a,Fun (b,c))::[]
				|Fun (a,b),Var (c) -> let y = testOccurrence c b in if(y) then 					failwith "Erreur de teste d'occurrence" else (c,Fun (a,b))::[]
				|Fun (a,b),Fun (c,d) -> if ((a = c) && ((List.length b) = (List.length d))) then uniFun b d else failwith "Les deux fonctions ne sont pas unifiables"(*changer*);;
 
let rec testOccurrence num listeF = match listeF with
					[] -> false
					|x::xs -> match x with
						Var (a) -> if(num = a) then true else 							
						testOccurrence num xs
						|Fun (a,b) -> let y = testOccurrence num b in
						if(y) then true else testOccurrence num xs;;

let rec uniFun l1 l2 = match l1,l2 with
			[],[] -> []
			|[],x::xs1 -> failwith "Impossible dans le cas l2 est different que l1"
			|x::xs1,[] -> failwith "Impossible dans le cas l1 est different que l2"
			|p1::xs1,p2::xs2 -> if ((List.length l1) <> (List.length l2)) then 
						failwith "Les arguments de 2 fonctions sont pas les meme"(*changer*) else
						match p1,p2 with 
						Var (a),Var (b) -> if (a <> b) then (a,p2)::uniFun xs1 xs2 else []
						|Var (a),Fun (b,c) -> (a,p2)::uniFun xs1 xs2
						|Fun (a,b),Var (c) -> (c,p1)::uniFun xs1 xs2
						|Fun (a,b),Fun (c,d) -> if ((List.length b) <> (List.length d)) then failwith "Les arguments de 2 fonctions sont pas les meme" else if (a = c) 
						then let x = uniFun b d in x@uniFun xs1 xs2 else failwith "Les deux fonctions sont différentes";;


(*test la fonction unifie*)
let x = Fun(0,[Var 0;Fun (3,[Var 1]);Var 3]);;
let y = Fun (0,[Var 1;Fun (3,[Var 2]);Var 4]);;
let z = Var 2;;
let w = Var 5;;
let a = Fun(2,[Fun (0,[Var 1;Var 2]);Var 2;Var 3]);; 
let b = Fun(2,[Fun (0,[Var 4;Var 5]);Var 5;Var 6]);;
unifie a b;;
unifie_sys [x;a;z] [w;b;b];;
let rec unifie_sys lterme1 lterme2 = unifie_s lterme1 lterme2 ;;
let rec unifie_sys lterme1 lterme2 = let x = unifie_s lterme1 lterme2 in nettoyage x ;;