DEV Community

Full Stack Hacker
Full Stack Hacker

Posted on • Edited on

3 2

Simulating Wang algorithm in Prolog

Rules of inference in Wang algorithm

Rule 1: Transform hypotheses and conclusions in the negative form

Example:

p v q, !(r ^ s), !q, p v r -> s, !p <=> p v q, p v r, p -> s, r ^ s, q

Rule 2: Replace the ^ sign with the comma of the hypothesis

Example:

p ^ q, r ^ (!p v s) -> !q v !r <=> p, q, r, !p v s -> !q v !r

Rule 3: Replace the v with the comma of the conclusion

Example:

p ^ q, r ^ (!p v s) -> !q v !r <=> p ^ q, r ^ (!p v s) -> !q, !r

Rule 4: Split into two separate lists of the hypothesis if it contains v sign

Example: p, !p v q -> q <=> p, !p -> q and p, q -> q

Rule 5: Split into two separate lists of the conclusion if it contains the ^ sign

Rule 6: Change the sign -> in the hypothesis and conclusion sides of the normal form CNF and DNF

Example of CNF normal form conversion: ¬(p→q) v (r→p)

Remove links →,↔

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

Use equivalent transformations (e.g. DeMorgan's law and double negation)

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

Use association rules and distribution rules

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

Rule 7: Change the sign ⬄ in the hypothesis and conclusion sides of the normal form CNF and DNF

Implementation of Wang algorithm

% 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).

Demo

Step 1: Run the program Prolog

Step 2: Prove the following statements

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

Step 3: Result

Top comments (0)

Retry later