<div class="notebook"> <div class="nb-cell program" name="p1"> /* prolog tutorial 2.13 Truth table maker https://www.cpp.edu/~jrfisher/www/prolog_tutorial/2_13.html */ /* Vidal-Rosset : Adding of the usual connectives and change of the order of truth values: first truth, i.e. 1. See below. */ :- op( 500, fy, ~). % negation :- op(1000, xfy, &). % conjunction :- op(1100, xfy, v). % disjunction :- op(1110, xfy, =>). % implication :- op(1120, xfy, <=>). % implication :- use_rendering(table, [header(['Vars','V'])]). find_vars(N,V,V) :- member(N,[0,1]),!. /* Boolean constants in expression */ find_vars(X,Vin,Vout) :- atom(X), (member(X,Vin) -> Vout = Vin ; /* already have */ Vout = [X|Vin]). /* include */ find_vars(X <=> Y,Vin,Vout) :- find_vars(X,Vin,Vtemp), find_vars(Y,Vtemp,Vout). find_vars(X => Y,Vin,Vout) :- find_vars(X,Vin,Vtemp), find_vars(Y,Vtemp,Vout). find_vars(X & Y,Vin,Vout) :- find_vars(X,Vin,Vtemp), find_vars(Y,Vtemp,Vout). find_vars(X v Y,Vin,Vout) :- find_vars(X,Vin,Vtemp), find_vars(Y,Vtemp,Vout). find_vars(~ X,Vin,Vout) :- find_vars(X,Vin,Vout). % next([0|R],[1|R]). % next([1|R],[0|S]) :- next(R,S). inversion of the order: next([1|R],[0|R]). next([0|R],[1|S]) :- next(R,S). initial_assign([],[]). initial_assign([_|R],[1|S]) :- initial_assign(R,S). % initial_assign 1 and not 0. predecessor(A,S) :- reverse(A,R), % predecessor instead of successor. next(R,N), reverse(N,S). % biconditional truth table biconditional(1,1,1). biconditional(1,0,0). biconditional(0,1,0). biconditional(0,0,1). % conditional truth table conditional(1,1,1). conditional(1,0,0). conditional(0,1,1). conditional(0,0,1). % biconditional truth table conjunction(1,1,1). conjunction(1,0,0). conjunction(0,1,0). conjunction(0,0,0). % disjunction truth table disjunction(1,1,1). disjunction(1,0,1). disjunction(0,1,1). disjunction(0,0,0). % negation truth table negation(1,0). negation(0,1). truth_value(N,_,_,N) :- member(N,[0,1]). truth_value(X,Vars,A,Val) :- atom(X), lookup(X,Vars,A,Val). truth_value(X <=> Y,Vars,A,Val) :- truth_value(X,Vars,A,VX), truth_value(Y,Vars,A,VY), biconditional(VX,VY,Val). truth_value(X => Y,Vars,A,Val) :- truth_value(X,Vars,A,VX), truth_value(Y,Vars,A,VY), conditional(VX,VY,Val). truth_value(X & Y,Vars,A,Val) :- truth_value(X,Vars,A,VX), truth_value(Y,Vars,A,VY), conjunction(VX,VY,Val). truth_value(X v Y,Vars,A,Val) :- truth_value(X,Vars,A,VX), truth_value(Y,Vars,A,VY), disjunction(VX,VY,Val). truth_value(~X,Vars,A,Val) :- truth_value(X,Vars,A,VX), negation(VX,Val). lookup(X,[X|_],[V|_],V). lookup(X,[_|Vars],[_|A],V) :- lookup(X,Vars,A,V). tt(E) :- find_vars(E,[],V), reverse(V,Vars), initial_assign(Vars,A), format(' '), write(Vars),format(' '),write(E), nl, format('-----------------------------------------'), nl, write_row(E,Vars,A), format('-----------------------------------------'), nl. write_row(E,Vars,A) :- format(' '), write(A),format(' '), truth_value(E,Vars,A,V),write(V),nl, (predecessor(A,N) -> write_row(E,Vars,N) ; true). </div> <div class="nb-cell query" name="q1"> tt(((a v b) => c) <=> ((a => c) & (b => c))) </div> <div class="nb-cell query" data-tabled="true" name="q2"> tt(a) % <- insert your formula inside the round brackets. </div> </div>