# 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.