Is ⇒⇒ associative? In other words, is a⇒(b⇒c) a b c always equivalent to a⇒b⇒c a b c ? What is a methodical way of answering questions of this type? We can make a truth table with two output columns, one for each formula in question, and then just check whether those two columns are the same.

Thus we see that truth tables are a method for answering questions of the form “Is formula φφ equivalent to formula ψψ?” We make a truth table, with a column for each of φφ and ψψ, and just inspect whether the two columns always agree. A bit of a brute-force solution, but certainly correct.

What about the related question, “Is formula θθ a tautology?”. Well, obviously truth tables can handle this as well: make a truth table for the formula, and inspect whether all entries are true. For example, in the above problem, we could have made a truth table for the single formula a⇒ b⇒c ⇔ a⇒b ⇒c⇔ a b c a b c . The original question of equivalence becomes, is this new formula a tautology?

The first approach is probably a tad easier to do by hand, though clearly the two approaches are equivalent. Another handy trick is to have three output columns you're computing: one for φ=a⇒ b⇒c φ a b c , one for ψ= a⇒b ⇒c ψ a b c , and one for φ⇔ψ⇔ φ ψ; filling out the first two helper columns makes it easier to fill out the last column.

int do_something(int value1, int value2)
{
   bool a = …;
   bool b = …;

   if (a && b)
      return value1;
   else if (a || b)
      return value2;
   else
      return value1;
}
    

int do_something(int value1, int value2)
{
   bool a = …;
   bool b = …;

   if ((a && !b) || (!a && b))
      return value2;
   else
      return value1;
}
    

So, how would do we use truth tables to reason about WaterWorld? Suppose you wanted to show that G-safeG-safe was true on some particular board. Clearly a truth table with the single column G-safeG-safe alone isn't enough (it would have only two rows — false and true — and just sit there and stare at you). We need some way to incorporate both the rules of WaterWorld and the parts of the board that we could see.

We can do that by starting with a huge formula that was the conjunction of all the WaterWorld domain axioms; call it ρρ. We would encode the board's observed state with another formula, ψψ. Using these, we can create the (rather unwieldy) formula that we're interested in: ρ∧ψ⇒G-safe ρ ψ G-safe . (Notice how this formula effectively ignores all the rows of the the truth-table that don't satisfy the rules ρρ, and the rows that don't correspond to the board we see ψψ: because of the semantics of ⇒⇒, whenever ρ∧ψρ ψ is false, the overall formula ρ∧ψ⇒G-safe ρ ψ G-safe is true.)