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

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

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, in the previous post, we solved it using a proof by contradiction.

In this post, we'll describe how a software program can solve this type of puzzle using automated theorem proving.

When searching for relevant tools, I came across the Prover9-Mace4 app that, according to its documentation, is a "front end to the programs Prover9 (which searches for proofs) and Mace4 (which searches for finite models and counterexamples)." 

I played a little bit with Prover9 for this post and will give a brief demo of it here. In the next post, I will turn to Mace4.

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

For this demo, I'll use Prover9 to complete a proof by contradiction of the puzzle's solution.

For this use case, I first entered the logical formula that makes up the puzzle into the top (larger) input box labeled "Assumptions:".

As discussed in previous posts, the statement of this puzzle translates to a single formula, namely:

\( A \leftrightarrow (-A\ |\ {-B})\)

which, in Prover9, can be typed up as:

A <-> (-A | -B).

Note the period that must end each formula in Prover9.

Then, I entered the logical formula that makes up the puzzle's solution into the bottom (smaller) input box labeled "Goals:".

As discussed in previous posts, the statement of this solution translates to a single formula, namely:

\( A\ \&\ {-B}\)

which, in Prover9, can be typed up as:

A & -B.

Again, note the period at the end of the formula.

Before running the theorem prover, I clicked on the "Show Current Input" button in the top-right corner of the GUI. This popped up a window containing the input that is put together into a text file made up of what I typed into the GUI and that will be fed to the command-line tool that this app is a front end for.

This window looks like this:

This automatically generated input file contains Prover9 options (e.g., limits on the running time; many other options are available) followed by the two groups of input formulas: assumptions and goals.

Everything looked good to me. So I closed this window. Then, back in the main window, I clicked on the "Start" button in the Prover9 section (the top one, above the Mace4 section).

For such a simple example, Prover9 finds a proof almost instantaneously.

Here is its output:

The numbered lines at the bottom of the output window show the proof's steps.

Since the proof is abbreviated (when compared to the level of detail that was used in the proofs of previous posts), I will go through it step by step.

The first two lines show the two input formulas, that is, the assumption and the goal.

The "non_clause" annotation on each one of these lines means that these two formulas are not in the format that Prover9 expects: they are not clauses.

A clause is a formula that has a special form: it must be a disjunction of literals, where a literal is a single proposition, optionally negated. Here is an example of a clause:

\(A\ |\ {-B}\ |\ {-C}\)

with three literals, two of which are negated.

As a pre-processing step, Prover9 first converts all input formulas, including assumptions and goals (the latter is first negated, as we discuss below), to clauses. This algorithm is called "clausify".

This is a general yet simple algorithm that converts any input formula \(\varphi\) in propositional logic into a conjunction of clauses that is logically equivalent to \(\varphi\).

Here is a (reconstructed) trace of this algorithm when applied to \(\varphi = A \leftrightarrow (-A\ |\ {-B})\). It simply uses a series of logical equivalences to rewrite \(\varphi\) as follows:

1.  \(A \leftrightarrow (-A\ |\ {-B})\)  [initial formula]
2.  \((A \rightarrow (-A\ |\ {-B}))\ \&\ ((-A\ |\ {-B})\ \rightarrow A)\) [a. + equivalence of a bi-conditional to a conjunction of conditionals]
3. \(A \rightarrow (-A\ |\ {-B})\) [first half of conjunction elimination on b.]
4. \((-A\ |\ {-B}) \rightarrow A\) [second half of conjunction elimination on b.]

At this point, \(\varphi\) is equivalent to the conjunction of the two formulas above (c. and d.), each one of which must be "clausified".

5. \(-A\ |\ (-A\ |\ {-B})\) [c.+ conditional to disjunction equivalence] 
6. \(-A\ |\ {-B}\) [e.+ idempotence of disjunction]

This last step works because \(-A\ |\ {-A}\) is logically equivalent to \(-A\). 

This is how Prover9 infers the clause on line 3 in the output image above, that is, as (partial) output of the clausify algorithm applied to the formula on line 1.

Now, continuing the trace of the clausify algorithm, we get:

7. \(-(-A\ |\ {-B})\ |\ A\) [d.+ conditional to disjunction equivalence] 
8. \((A\ \&\ B)\ |\ A\) [g.+ De Morgan's law + double negation elimination] 
9. \((A\ |\ A)\ \&\ (B\ |\ A)\) [h.+ distributivity of disjunction over conjunction] 
10. \(A\ |\ A\) [first half of conjunction elimination on i.] 
11. \(A\) [j.+ idempotence of disjunction]

And this is how Prover9 infers the clause on line 4 in the output image above, that is, as (partial) output of the clausify algorithm applied to the formula on line 1.

This step also marks the completion of the clausify algorithm.

Now, recall that Prover9 is searching for a proof by contradiction, which requires negating the goal formula.

So, line 5 of Prover9's output is simply the negation of the conjunction of the two clauses on line 2.  Note that the negation of the goal formula is already a clause, and therefore does not need to be clausified in this sample proof.

As the next-to-last step, Prover9 infers, on line 6,  the clause \(B\) by applying the resolution inference rule to the clauses on lines 4 and 5.

Note that Prover9 uses the phrase unit deletion here (instead of resolution) because one of the premises, namely the clause \(A\) on line 4, is a unit clause (that is, a clause made up of a single literal). This clause is combined with the premise \(-A\ |\ B\) on line 5 to cancel its literal \(-A\), yielding \(B\) on line 6.

Finally, Prover9 infers \(\$F\) on line 7, which is its symbol for \(\perp\).

Note that Prover9 uses the phrase back unit deletion here because the newly inferred formula \(B\) on line 6 is used to cancel out the \(-B\) (hence the unit deletion) in the previously inferred formula on line 3 (that is, an inference step that goes back and modifies a previously inferred formula).

This back unit deletion step yields the clause \(-A\) which, in this same step (i.e., on line 7) is cancelled out with the clause \(A\) on line 4 (another unit deletion operation) to yield the contradiction.

This last step concludes the proof, since a contradiction was inferred. 

The (non-negated) goal formula is therefore a logical consequence of the assumption. 

In other words, Prover9 has formally proved our solution to the Knights and Knaves puzzle.

In the next post, we will use Mace4 to solve this same puzzle using another application of automated theorem proving.