Truth Table

A truth table shows how the truth of a formula in propositional logic is dependent upon its constituent variables.

Example

The following is the truth table for the conjunction of two variables.

`A`	`B`	`A ∧ B`
`f`	`f`	`f`
`f`	`t`	`f`
`t`	`f`	`f`
`t`	`t`	`t`

Implementation

The following code can be found in the examples directory of the Barry's Prolog distribution.

The following Prolog code will display a truth table for a given formula in proposition logic. First we fix a set of operators which we will need to represent the formulas of propositional logic.

:-op(200, fy, ~).                   % Negation
:-op(0, yfx, (/\)).
:-op(400, xfy, (/\)).               % Conjunction (not ISO associativity which is yfx)
:-op(0, yfx, (\/)).
:-op(500, xfy, (\/)).               % Disjunction (not ISO associativity which is yfx)
:-op(600, xfy, =>).                 % Implication
:-op(700, xfy, <=>).                % Equivalence

The procedure pl_atoms/2 collects the set of atoms (propositional variables) in a given formula. Here we use ord_union/2 which comes from a library which implements sets as ordered lists. A Prolog atom is a singleton set (list of one element).


	  pl_atoms(Atom, [Atom]) :- 
	atom(Atom), 
	!.
pl_atoms(~Phi, Atoms) :- 
	pl_atoms(Phi, Atoms).
pl_atoms(Phi /\ Psi, Atoms) :- 
	pl_atoms(Phi, A1), 
	pl_atoms(Psi, A2), 
	ord_union(A1, A2, Atoms).
pl_atoms(Phi \/ Psi, Atoms) :- 
	pl_atoms(Phi, A1), 
	pl_atoms(Psi, A2), 
	ord_union(A1, A2, Atoms).
pl_atoms(Phi => Psi, Atoms) :- 
	pl_atoms(Phi, A1), 
	pl_atoms(Psi, A2), 
	ord_union(A1, A2, Atoms).
pl_atoms(Phi <=> Psi, Atoms) :- 
	pl_atoms(Phi, A1), 
	pl_atoms(Psi, A2), 
	ord_union(A1, A2, Atoms).

The procedure pl_eval/2 is the definition of the semantics of propositional logic. Using the valuation (truth assignment) V we evaluate the formula. An association list is used to implement the valuation — get_assoc/3 is from the association list library.


	  pl_eval(Atom, V) :- 
	atom(Atom),  
	(get_assoc(Atom, V, Answer); throw(no_such_proposition_variable(Atom))),
	!,
	Answer = true.
pl_eval(~Phi, V) :- 
	\+ pl_eval(Phi, V).
pl_eval(Phi /\ Psi, V) :- 
	pl_eval(Phi, V), 
	pl_eval(Psi, V).
pl_eval(Phi \/ Psi, V) :- 
	pl_eval(Phi, V)
    ; 
	pl_eval(Psi, V).
pl_eval(Phi => Psi, V) :- 
	pl_eval(~Phi \/ Psi, V).
pl_eval(Phi <=> Psi, V) :-
	pl_eval((~Phi \/ Psi) /\ (Phi \/ ~Psi), V).

The procedure pl_valuation/2 builds a valuation from a given set of variables. This can be used in a failure driven loop to generate all possible valuations. The procedure put_assoc/4 is from the same library as get_assoc/3.


	  pl_valuation([], t).                      % The empty association is denoted by the symbol t. 
pl_valuation([H|T], V) :-
	member(Truth, [false, true]),     % Do this first so we create a choice point for the first element before the last element.
	pl_valuation(T, Vtemp),
	put_assoc(H, Vtemp, Truth, V).

pl_print_truth_table_row prints one row of a truth table. The first argument is a set of atom-truth pairs, one for each variable of the table. The second argument is either true or false depending on the evaluation of the original formula w.r.t. the valuation represented by the values in first argument.


	  pl_print_truth_table_row([], Truth) :- 
	print(Truth), 
	nl.
pl_print_truth_table_row([(_-X)|T], Truth) :- 
	print(X), 
	put_code(9),   % ASCII 9 is a horizontal TAB.
	pl_print_truth_table_row(T, Truth).

In pl_print_truth_table_head/1 we print the head row of the truth table. There is one element in the list argument for each variable.


	  pl_print_truth_table_head([]) :- 
	print(formula),
	nl.
pl_print_truth_table_head([H|T]) :- 
	print(H), 
	put_code(9),   % ASCII 9 is a horizontal TAB.
	pl_print_truth_table_head(T).

The procedure pl_print_truth_table/1 drives the whole process. There is one call to pl_print_truth_table/2 for each possible valuation for the formula. The procedure assoc_to_list/2 is from the association list library.


	  pl_print_truth_table(Phi) :-
	print('Truth table for '), 
	print(Phi),
	nl,
	pl_atoms(Phi, Atoms),
	pl_print_truth_table_head(Atoms),
	pl_print_truth_table(Atoms, Phi).

pl_print_truth_table(Atoms, Phi) :-
	pl_valuation(Atoms, V),                % The failure driven loop starts here. Create a valuation V
	(   pl_eval(Phi, V) ->                 % Evaluate the formula given V
	    Truth = true
	;
	    Truth = false
	),
	assoc_to_list(V, Lst),                 % Turn the valuation into a list of true/false elements (a row).
	pl_print_truth_table_row(Lst, Truth),  % Print the row.
	fail.                                  % Force a new round of the failure driven loop, i.e., create a new valuation.
pl_print_truth_table(_, _).                    % Finished.

The following transcript shows an example where we print the truth table for (p /\ q => q /\ r)


	  | ?- pl_print_truth_table((p /\ q => q /\ r)).
Truth table for p/\ q=>q/\ r
p	q	r	formula
false	false	false	true
false	false	true	true
false	true	false	true
false	true	true	true
true	false	false	true
true	false	true	true
true	true	false	false
true	true	true	true
% yes

References

Doets, Kees. From Logic to Logic Programming. MIT Press, 1994.