lmc.ml

用ocaml编写的逻辑程序

(*La fonction compose nous permet de calculer la substitution par composition de 2 substitutions*)
let rec test terme sub=match sub with
                       []->true
                       |s::s1->if (fst(s)=fst(terme)) && (snd(s)<>snd(terme)) then false else test terme s1
;;
test sub r;;
(*bool = false*)
let sub=(1,x2);;
test sub r;;
(*bool = false*)

let rec testsub sub1 sub2=match sub1,sub2 with
                          [],[]->true
                          |t::s1,[]->true
                          |[],t::s1->true
                          |t1::s1,t2::s2->let x=test t1 sub2 in
                                          if x then testsub s1 sub2 else failwith"Erreur pour les 2 listes de substitutions"
 ;;
 let sub1=[(0,x2);(1,x3);(4,Fun(0,[x1]))];;
 let sub2=[(1,x2);(2,x4)];;
 (*Failure "Erreur pour les 2 listes de substitutions".*)
 let sub1=[(0,x2);(1,x3);(4,Fun(0,[x1]))];;
 let sub2=[(0,x2);(2,x4)];;
 (*bool = true*) 
 
 
 testsub suba subb;;(* bool = true*)
 
 let rec comp sub1 sub2=match sub1,sub2 with
                       [],[]->[]
                       |[],t::s1->[]
                       |t::s1,[]->[]
                       |t1::s1,t2::s2->let a=fst(t1) in 
                                       let b=snd(t1) in 
                                       let x=substitue sub2 b in 
                                       if b=x then (a,b)::comp s1 sub2
                                       else let y=substitue sub1 x in (a,y)::comp s2 sub2
 ;;
 comp suba subb;;
 (* (int * term) list = [(0, Fun (0, [Var 4])); (3, Fun (0, [Var 4]))]*)
 
 
 let rec compose sub1 sub2=match sub1,sub2 with 
                           [],[]->[]
                           |[],t::s1->sub2
                           |t::s1,[]->sub1
                           |t1::s1,t2::s2->let z=testsub 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"
;;

compose suba subb;;
(*(int * term) list =
[(0, Fun (0, [Var 4])); (2, Fun (0, [Var 4])); (1, Fun (0, [Var 4]));
 (3, Fun (0, [Var 4]))]*)

let rec subliste (sub:subst) terme =match terme with
                           []->[]
                           |t::q->(substitue sub t)::(subliste sub q)
;;
subliste suba p;;
(*term list = [Var 1; Fun (0, [Var 1]); Fun (1, [Var 1])]*)

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,subliste [sub] e))::(subone sub q)
;;
let a=(0,x1);;
let b=[(1,x2);(0,Fun(0,[x1]))];;
subone a b;;
(* (int * term) list = [(1, Var 2); (0, Fun (0, [Var 1])); (0, Var 1)]*)


let compose (sub1:subst) (sub2:subst)=match sub1,sub2 with
                     [],[]->[]
                     |[],t::s1->sub2
                     |t::s1,[]->sub1
                     |t1::s1,t2::s2->compose s1 (subone t1 s2)
;;


compose suba subb;;
compose [] subb;;

(retourne le pgu d'un systeme d'equation)

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



let rec testoccurence num liste =match liste with
                                 []->false
                                 |x::xs->match x with
                                     Var a ->if num =a then true else
                                              testoccurence num xs
                                     |Fun(a,b)->let y=testoccurence num b in 
                                                if y then true else testoccurence num xs
;;

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

let rec occheck listsub =match listsub with
                         []->[]
                         |t::s->(testoccu  (fst t) (elimi [t] s))::(occheck s)
;;
                         
let rec result list=match list with
                    []->false
                    |t::s->t||result s;;
                    
let occucheckfinial list=result (occheck list);;
                         
let rec recherche e l=match l with
                      []->false
                      |x::xs->if ((fst x)=(fst e))&&((snd x)=(snd e)) then true
                              else recherche e xs
 ;;

let rec suppression e l=match l with
                        []->[]
                        |x::xs->if x=e then xs else x::(suppression e xs);;

let rec nettoyage listsub=match listsub 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;;

exception Erreur_Unification;;

let rec unifun f1 f2 =match f1,f2 with
                      [],[]->[]
                      |t::s,[]->raise Erreur_Unification
                      |[],t::s->raise Erreur_Unification
                      |t1::s1,t2::s2->if ((List.length f1)<>(List.length f2)) then raise Erreur_Unification
                                      else match t1,t2 with
                                           Var a,Var b->if a<>b then (a,t2)::unifun s1 s2 else []
                                           |Var a,Fun(b,c)->(a,t2)::unifun s1 s2
                                           |Fun(a,b),Var c->(c,t1)::unifun s1 s2
                                           |Fun(a,b),Fun(c,d)->if ((List.length b)<>(List.length d)) 
                                            then raise Erreur_Unification
                                            else if a=c then let x=unifun b d in
                                                   x@unifun s1 s2 else raise Erreur_Unification
 ;;
                      
                                  
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=testoccurence a c in if x then raise Erreur_Unification
                                                   else (a,Fun(b,c))::[]
                             |Fun(a,b),Var c->let y=testoccurence c b in if y then raise Erreur_Unification
                                                    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 raise Erreur_Unification
;;
                                  

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;;(*(int * term) list = [(1, Var 4); (2, Var 5); (2, Var 5); (3, Var 6)]*)


let rec unifies terme1 terme2=match terme1,terme2 with
                               [],[]->[]
                               |[],t::s->raise Erreur_Unification
                               |t::s,[]->raise Erreur_Unification
                               |t1::s1,t2::s2->let x=unifie t1 t2 in x@unifies s1 s2;;
                               
                               
                              
let rec unifie_sys terme1 terme2 sub=let x=unifie terme1 terme2 in
                                     let y=nettoyage x in let z=
                                     occucheckfinial (compose y sub) in 
                                     if z then [] else compose y sub
;;
                               
let rec unifie_sys terme1 terme2 = unifies terme1 terme2 ;;


unifie_sys [x;a;z] [w;b;b];;
(*(int * term) list =
[(5, Fun (0, [Var 0; Fun (3, [Var 1]); Var 3])); (1, Var 4); (2, Var 5);
 (2, Var 5); (3, Var 6);
 (2, Fun (2, [Fun (0, [Var 4; Var 5]); Var 5; Var 6]))]*)

let rec unifie_sys terme1 terme2 = let x = unifies terme1 terme2 in nettoyage x ;;
unifie_sys [x;a;z][w;b;b];;
(*(int * term) list =
[(5, Fun (0, [Var 0; Fun (3, [Var 1]); Var 3])); (1, Var 4); (3, Var 6);
 (2, Fun (2, [Fun (0, [Var 4; Var 5]); Var 5; Var 6])); (2, Var 5)]*)


(*resolution*)


(*la fonction retourn true si on peut obtenir la clause vide sinon false*)
let rec resoud clause=match clause with
                [[At(i,l)]] ->false
                |[[No(At(i,l))]]->false
                |[[At(i,l);At(j,m)]]->false
                |[[No(At(i,l));No(At(j,m))]]->false
                |[[At(i,l);No(At(j,m))]]->if (i=j)&&((List.length (unifie_sys l m))=0) then true else false
                |[[No(At(i,l));At(j,m)]]->if (i=j)&&((List.length (unifie_sys l m))=0) then true else false
                |[At(i,l);No(At(j,m))]::[clau]->if (i=j)&&((List.length (unifie_sys l m))=0) then (resoud [clau])
                                                else false
                |[No(At(i,l));At(j,m)]::[clau]->if (i=j)&&((List.length (unifie_sys l m))=0) then (resoud [clau])
                                                else false
                |_->failwith"Impossible de resolution"
;;
                
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(p,q);;
let t=Imp(p1,q);;
let u=gen_clauses s;;
let v=gen_clauses t;;
resoud u;;
(*bool = true*)
resoud v;;
(* bool = false*)

(*la fonction affiche le processus de demonstration*)


let rec clause_sub f sub=match f with
                         [[At(i,l)]]->unifie_sys l sub
                         |[[No(At(i,l))]]->unifie_sys l sub
                         |_->failwith"il n'y a pas de sub"
 ;;

let trace_resoud f sub=
       let clauses= gen_clauses f in
      
       resoud clauses
;;