5.Thuật toán Vương Hạo

*Thuật toán vương hạo là thuật toán dùng để cm tự động các định lí đc biểu diễn trong logic mệnh đề

   Input  :gt1,gt1,..,gtm

               kl1,kl2,..,kln

   Output chung minh gt-->kl

 Nếu chứng minh dc thông báo thành công cong ko thất bại

(gt kt #)

*phương pháp chứng minh

B1:chuẩn hóa các mệnh đề gti với (i=1,m) và đưa nó vào tập vt

B2: chuẩn hóa các mệnh đề kết luận với (i=1,n) và đưa nó vào tập vế phải

 Ta có cặp (vt,vp)->p

B3: chưng minh p# còn thực hiện

+p=>(vt,vp)(p lấy ra cặp vế trái,vế phải)

+nếu vtvp= thì

 Chuyển vế (vt,vp)

-if(vtvp=) thì

 Neu(not tach (vt,vp) thi

+that bai

Nguoc lai

 (vt,vp) n =>p

Nguoc lai

 Thanh cong

Nguoc lai

Thanh cong =>chuan hoa

+xet

 -Nếu tất cả các cặp (vt,vp)trong p đều chứng minh dc=>định lí dc chứng minh

-tách :thay dấu

 +Nếu vt có dấ ^ ta có thể thay bằng dấu (,),còn vp có dấu thì thay bằng dấu (,)

*thuật toán theo ngôn ngữ tựa

Procedure vuonghao;

Begin

For i=1 to m do

Begin

Chuanhoa(gti);

vt=vt{gti};

end;

For i:=1 to n do

Chuanhoa(kli);

(vp=vp{kli };

End;

(vt,vp)=>p;

While (p# rong) do

 Begin

If(vtvp=rỗng) then

Chuyenve(vt,vp);

Thaydau(vt,vp);

If(vtvp=rong) then

If  not tach(vt,vp) then

Begin

 Thatbai;

  Exit;

End

Else

Dua cap vt,vp moi tach vao p;

Else

Thanhcong;

end

Else

Thanhcong;

End;

6.Thuật toán Robinson (Hợp giải)

*Ý Tưởng

 Thực chất của phương pháp hợp giải do Robinson đề xuất là chứng minh bằng phản chứng để chỉ ra gt1,gt2,..,gtn có thể suy ra kl1,kl2,..,kln ta sẽ lấy phủ định của kết luận đem hợp cùng gt nếu bằng cách biến đổi nào đó ta suy ra dc mâu thuẫn thì quá trình chứng minh thành công

*Thuật toán

Input gt1,gt2,..gtm va kl1, ...kln

Output dinh li dc chung minh neu gt=>kl

*Thuật toán bằng ngôn ngữ tựa

Procedure robinson;

Begin

 P=;

For i:=1 to m do

Begin

Chuanhoa(gti);

P=p{gti};end;

For i:=1 to n do

Chuanhoa(kli);

(P=p{kli };

End;

If mauthuan(p) then

Begin

Thanhcong;

Exit; end;

P1=; while (p1#p) and(7 mauthuan(p)) do

Begin

P1=p;hopgiai(p);

End;

If mauthuan (p) then

Thanhcong

Else thatbai;

End;