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ả