[Part 10] A Propositional Logic approach to Raymond Smullyan's Knights and Knaves puzzles Automating puzzle proofs with Mace4

Earlier in this series, we solved the following Knights and Knaves puzzle in a variety of ways:

A makes the following statement, "At least one of us is a knave."  

What are A and B?

First, we solved it informally.

Second, we solved it using a rather linear, direct formal proof. 

Third, we solved it using a hierarchical, natural deduction-style proof.

Fourth, we solved it using a truth table.

Fifth, we solved it using a proof by contradiction.

Sixth, in the previous post, we solved it using automated theorem proving in Prover9.

The way we used Prover9 in the previous post was to input both the statement of the puzzle and its solution. This use case would correspond to a scenario where:

1. we are able to solve the puzzle informally, but 
2. we want to check our solution formally without having to write a formal proof ourselves.

In other words, we were able to automate step 2.

But can we automate step 1 as well?

In other words, could we simply feed the puzzle statement, but not its solution, to an automated theorem prover that would then discover a provably correct solution?

The answer is yes; but Prover9 will not do for this.

Recall, from the previous post, that the app I used, namely Prover9-Mace4, is described as a "front end to the programs Prover9 (which searches for proofs) and Mace4 (which searches for finite models and counterexamples)." 

It turns out that Mace4 will allow us to automate step 2 above.

Mace4 takes, as input, a set of formulas and returns one or more models for it.

In the context of propositional logic, a model for a given set of formulas is an interpretation that makes all formulas in the set true, where an interpretation is an assignment of truth values (i.e., True or False) to all propositions in the set of formulas. 

When solving Knights and Knaves puzzles, the input to Mace4 is a set of one or more formulas that encode the puzzle statement. Mace4 will then return the truth values that all propositions in the formulas must take on to make the puzzle statement true, that is, to solve the puzzle.

And since the propositions, for us, will be \(A\), \(B\), etc., that is, the propositions that represent, "A is a knight, "B is a knight", etc., the output of Mace4 will be a solution to the puzzle!

Let's then use Mace4 to solve the puzzle above.

Here again is what the GUI for the Prover9-Mace4 app looks like:

It is the same GUI as before; but we will use it differently:

1. We will use the top-left input box (as before) to specify the input to Mace4 
2. but this time, we will leave the bottom left input box empty: note that, under our current use case, we do not yet know the solution to the puzzle; and we do not need it since we are not looking for a proof by contradiction
3. we will use the Mace4 panel in the bottom-right corner instead of the Prover9 panel in the top-right corner.

Here is the same GUI with the input formula typed in:

Before we run Mace4, we want to override one of its default options. To do this, we click on the "Mace4 Options" tab toward the top of the window...

... and set the maximum number of models to 4 (circled in red above). 

Since our puzzle statement involves exactly two propositions (\(A\) and \(B\)) and each one of them can be either True or False, the total number of distinct interpretations is equal to 4.

We are using Mace4 to find out which one(s) of these four interpretations is a (are) solution(s) to the puzzle. 

Now, if we set this option to 1, Mace4 would return the first solution it finds. But then we may miss alternative solutions (for puzzles that have more than one solution). 

If we set this option to a number larger than 4, we may make Mace4 work harder than it needs to, since there cannot possibly be more than 4 distinct solutions.

Having set this option to a reasonable value (and left the other options to their default values), we click on the "Formulas" tab to return to the main window and we launch Mace4 by clicking on the "Start" button in the bottom-right pane.

Mace4 returns an answer almost instantaneously (given the tiny size of our problem), namely:

This output lists four models, that is, four interpretations (numbered 1 through 4) that make the puzzle statement true.

Each interpretation associates (i.e., establishes a relation between) a truth value
(1 for True and 0 for False) to the propositions \(A\) and \(B\).

In the first model, we see that \(A\) is True and \(B\) is False, which is the expected solution to this puzzle. In other words, A must be a knight and B must be a knave.

Surprisingly, the last three interpretations are identical to the first one. This simply means that there is only one solution to this puzzle.

The reason for the duplication is that internally, these interpretations are represented in such a way that Mace4 cannot immediately tell that they are actually identical to each other.

In fact, they are identical to us (technically, they are isomorphic to each other). What we really want is only one such solution, called a canonical form.

To ask Mace4 to remove all isomorphic solutions and only display what we consider to be distinct solutions, we can:

1. click on the "Isofilter..." button at the top of the output window,
2. select the "Canonical Forms" algorithm in the pop-up window, and
3. click the "Start" button in this same pop-up window.

Mace4 will then output:

which is the unique solution to this puzzle.