% nacteni:
/* ['8.2_20.pl']. */

% pomocne funkce - jen "zaslepky"
% symboly P1, P2, P3
proposition_symbols([p1,p2,p3],_).
% priklad: KB = P2 and P3
%          alpha = P2
%          beta = P1
pl_true(kb,   [p3-true, p2-true, p1-true]):-!.
pl_true(kb,   [p3-true, p2-true, p1-false]):-!.
pl_true(alpha,[p3-true, p2-true, p1-true]):-!.
pl_true(alpha,[p3-false,p2-true, p1-true]):-!.
pl_true(alpha,[p3-true, p2-true, p1-false]):-!.
pl_true(alpha,[p3-false,p2-true, p1-false]):-!.
pl_true(beta, [p3-true, p2-true, p1-true]):-!.
pl_true(beta, [p3-true, p2-false,p1-true]):-!.
pl_true(beta, [p3-false,p2-true, p1-true]):-!.
pl_true(beta, [p3-false,p2-false,p1-true]):-!.

% tt_entails(+KB,+Alpha)
tt_entails(KB,Alpha):-proposition_symbols(Symbols,[KB,Alpha]),
    tt_check_all(KB,Alpha,Symbols,[]).
% tt_check_all(+KB,+Alpha,+Symbols,+Model)
tt_check_all(KB,Alpha,[],Model):-pl_true(KB,Model),!,pl_true(Alpha,Model).
tt_check_all(_KB,_Alpha,[],_Model):-!.
tt_check_all(KB,Alpha,[P|Symbols],Model):-
    tt_check_all(KB,Alpha,Symbols,[P-true|Model]),
    tt_check_all(KB,Alpha,Symbols,[P-false|Model]).

show_bool(Text,P):-write(Text),call(P),!,write('yes'),nl.
show_bool(_,_):-write('no'),nl.

%:- trace,tt_entails(kb,alpha).
:- show_bool('KB entails Alpha: ', tt_entails(kb,alpha)), % true
   show_bool('KB entails Beta: ', tt_entails(kb,beta)).  % false