- vừa được xem lúc

MÔ PHỎNG THUẬT TOÁN VƯƠNG HẠO TRONG PROLOG

0 0 76

Người đăng: Nguyễn Trung Hậu

Theo Viblo Asia

1. Các luật suy diễn trong thuật toán Vương Hạo

Luật 1: Chuyển vế các giả thuyết và kết luận ở dạng phủ định

Ví dụ: p v q, !(r ^ s), !q, p v r -> s, !p <=> p v q, p v r, p -> s, r ^ s, q

Luật 2: Thay dấu ^ thành dấu phẩy của giả thuyết

Ví dụ: p ^ q, r ^ (!p v s) -> !q v !r <=> p, q, r, !p v s -> !q v !r

Luật 3: Thay dấu v thành dấu phẩy của kết luận

Ví dụ: p ^ q, r ^ (!p v s) -> !q v !r <=> p ^ q, r ^ (!p v s) -> !q, !r

Luật 4: Tách thành hai danh sách riêng của giả thuyết nếu chứa dấu v

Ví dụ: p, !p v q -> q <=> p, !p -> q và p, q -> q

Luật 5: Tách thành hai danh sách riêng của kết luận nếu chứa dấu ^

Luật 6: Thay đổi dấu -> ở các vế giả thuyết và kết luận về dạng chuẩn CNF và DNF

Ví dụ về chuyển đổi dạng chuẩn CNF: ¬(p→q) ∨ (r→p)

1. Loại bỏ các liên kết →, ↔

¬(¬p ∨ q) ∨ (¬r ∨ p)

2. Sử dụng các phép biến đổi tương đương (vd: luật DeMorgan và phép phủ định 2 lần)

(p ∧ ¬q) ∨ (¬r ∨ p)

3. Sử dụng các luật kết hợp (associative rules) và phân bố (distributive rules)

(p ∨ ¬r ∨ p) ∧ (¬q ∨ ¬r ∨ p) <=> (p ∨ ¬r) ∧ (¬q ∨ ¬r ∨ p)

Luật 7: Thay đổi dấu ⬄ ở các vế giả thuyết và kết luận về dạng chuẩn CNF và DNF

2. Cài đặt thuật toán Vương Hạo

% Automated Theorem Proving
% Wang's Algorithm % Define operators.
:-op(700,xfy,<->).
:-op(700,xfy,->).
:-op(600,xfy,v).
:-op(600,xfy,&).
:-op(500,fy,!). % Main call.
prove([],[]).
prove([L|P],[R|A]):- nl, ansi_format([bold],'Statement: ',[]), write(L), write(' |= '), write(R), nl, nl, ansi_format([bold],'Attempting proof!',[]), nl, nl, wang(L,R), prove(P,A). % Procedure of Wang to prove theorem.
wang(L,R):- rules(L,R,[],0), nl, ansi_format([bold,fg(green)], 'Result: The given theorem is true.',[]), nl, nl; ansi_format([bold, fg(red)],'Proof failed for current step!',[]), nl, nl, ansi_format([bold,fg(red)], 'Result: The given theorem is false.',[]), nl, nl. % Move negations from left to right.
rules(L,R,S,T):- member(!X,L), delete(L,!X,Ld), append(S,[[['*Rule 1L '],[Ld,' |= ',[X|R]],T]],Sa), rules(Ld,[X|R],Sa,T). % Move negations from right to left.
rules(L,R,S,T):- member(!X,R), delete(R,!X,Rd), append(S,[[['*Rule 1R '],[[X|L],' |= ',Rd],T]],Sa), rules([X|L],Rd,Sa,T). % Replace conjunction by commas on the left.
rules(L,R,S,T):- member(X & Y,L), delete(L,X & Y,Ld), append(S,[[['*Rule 2 '],[[X,Y|Ld],' |= ',R],T]],Sa), rules([X,Y|Ld],R,Sa,T). % Replace disjunction by commas on the right.
rules(L,R,S,T):- member(X v Y,R), delete(R,X v Y,Rd), append(S,[[['*Rule 3 '],[L,' |= ',[X,Y|Rd]],T]],Sa), rules(L,[X,Y|Rd],Sa,T). % Branch disjunction on the left.
rules(L,R,S,T):- member(X v Y,L), delete(L,X v Y,Ld), Ta is T + 1, append(S,[[['*Rule 4a - Branch Level ',T],[[X|Ld],' |= ',R],T]],Sa), rules([X|Ld],R,Sa,Ta), Tb is T + 1, append([],[[['*Rule 4b - Branch Level ',T],[[Y|Ld],' |= ',R],T]],Sb), rules([Y|Ld],R,Sb,Tb). % Branch conjunction on the right.
rules(L,R,S,T):- member(X & Y,R), delete(R,X & Y, Rd), append(S,[[['*Rule 5a - Branch Level ',T],[L,' |= ',[X|Rd]],T]],Sa), Ta is T + 1, rules(L,[X|Rd],Sa,Ta), Tb is T + 1, append([],[[['*Rule 5b - Branch Level ',T],[L,' |= ',[Y|Rd]],T]],Sb), rules(L,[Y|Rd],Sb,Tb). % Replace implication on the left.
rules(L,R,S,T):- member(X -> Y,L), delete(L,X -> Y,Ld), append(S,[[['*Rule 6L '],[[!X v Y|Ld],' |= ',R],T]],Sa), rules([!X v Y|Ld],R,Sa,T). % Replace implication on the right.
rules(L,R,S,T):- member(X -> Y,R), delete(R,X -> Y,Rd), append(S,[[['*Rule 6R '],[L,' |= ',[!X v Y|Rd]],T]],Sa), rules(L,[!X v Y|Rd],Sa,T). % Replace equivalence on the left.
rules(L,R,S,T):- member(X <-> Y,L), delete(L,X <-> Y,Ld), append(S,[[['*Rule 7L '],[[(X -> Y) & (Y -> X)|Ld],' |= ',R],T]],Sa), rules([(X -> Y) & (Y -> X)|Ld],R,Sa,T). % Replace equivalence on the right.
rules(L,R,S,T):- member(X <-> Y,R), delete(R,X <-> Y,Rd), append(S,[[['*Rule 7R '],[L,' |= ',[(X -> Y) & (Y -> X)|Rd]],T]],Sa), rules(L,[(X -> Y) & (Y -> X)|Rd],Sa,T). % Finally compare both sides.
rules(L,R,S,T):- append(S,[[['*Tautology? '],[L,' |= ',R], T]],Sa), member(X,L), member(X,R), append(Sa,[[['*True. '],[],T]],Sb), printprove(Sb). % If theorem is true then print prove.
printprove([]).
printprove([[P,Q,T]|S]):- tab(T*5), printlist(P), tab(40 - T*5), printlist(Q), nl, printprove(S). % Helper for printing list recursively.
printlist([]).
printlist([H|T]):- write(H), printlist(T).

3. Demo

Bước 1: Chạy chương trình Prolog

Bước 2: Chứng minh các mệnh đề sau đây

(p -> q) & (!r -> !q) -> (p -> r)

Bước 3: Kết quả

Bình luận

Bài viết tương tự

- vừa được xem lúc

Thuật toán quay lui (Backtracking)

Quay lui là một kĩ thuật thiết kế giải thuật dựa trên đệ quy. Ý tưởng của quay lui là tìm lời giải từng bước, mỗi bước chọn một trong số các lựa chọn khả dĩ và đệ quy.

0 0 38

- vừa được xem lúc

Các thuật toán cơ bản trong AI - Phân biệt Best First Search và Uniform Cost Search (UCS)

Nếu bạn từng đọc các thuật toán trong AI (Artificial Intelligence - Trí tuệ nhân tạo), rất có thể bạn từng nghe qua về các thuật toán tìm kiếm cơ bản: UCS (thuộc chiến lược tìm kiếm mù) và Best First Search (thuộc chiến lược tìm kiếm kinh nghiệm). Khác nhau rõ từ khâu phân loại rồi, thế nhưng hai th

0 0 146

- vừa được xem lúc

Sử dụng vector trong lập trình C++ - giải bài toán lập trình muôn thủa

Chào buổi tối mọi người, hôm nay lang thang trên mạng bắt gặp bài toán quen thuộc một thời của quãng đường sinh viên IT. Đấy chính là câu số 1 trong đề thi dưới đây:.

0 0 35

- vừa được xem lúc

A* Search Algorithm

What is A* Search Algorithm. How it works. . Explanation.

0 0 42

- vừa được xem lúc

Python: Jump Search

Search là một từ khóa khá là quen thuộc đối với chúng ta. Hiểu theo đúng nghĩa đen của nó chính là "Tìm kiếm".

0 0 35

- vừa được xem lúc

Thuật toán tính nhanh nghịch đảo căn bậc 2.

Mở đầu. Vào khoảng những năm 2002, 2003, khi mã nguồn của tựa game Quake 3 Arena được chuyển thành mã nguồn mở, người ta đã tìm ra một hàm tính ra được giá trị nghịch đảo của căn bậc 2 một cách nhanh chóng, được biết đến rộng rãi với cái tên Fast inverse square root.

0 0 48