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