Converting logical puzzle into predicate calculus and prolog/dlv

Question

The question is : The salt has been stolen! Well, it was found that the culprit was either the Caterpillar, Bill the Lizard or the Cheshire Cat. The three were tried and made the following statements in court:

CATERPILLAR: Bill the Lizard ate the salt.
BILL THE LIZARD: That is true!
CHESHIRE CAT: I never ate the salt.

As it happened, at least one of them lied and at least one told the truth. Who ate the salt?

I know for sure if bill is true, than all statements are true, and if cheshire is true, then all are false, so it must be the caterpillar.

Looking at in predicate calculus and programming it, it would be something like this right:

suspect(caterpillar).
suspect(lizard).
suspect(cat).

:- suspect(cat), suspect(lizard).
:- suspect(cat), suspect(caterpillar).
:- suspect(lizard), suspect(caterpillar).

%where these imply not more than one of these can be true or returned in our set

But then further describing this in predicate logic I don't how I would describe the descriptions or plea's they have made. And how that if one statement is true can imply that others may be falses.

Answer 1

One nice thing about this puzzle is that you do not even need first-order predicate logic to model it: It suffices to use propositional logic, because whether a suspect lies or tells the truth can be indicated with a Boolean variable, and the statements themselves are also only statements over Boolean variables.

Thus, consider using a constraint solver over Boolean variables when solving this task with Prolog. See clpb for more information about this.

Here is a sample solution, using SICStus Prolog or SWI:

:- use_module(library(clpb)).

solution(Pairs) :-
        Suspects = [_Caterpillar,Lizard,Cat],
        pairs_keys_values(Pairs, [caterpillar,lizard,cat], Suspects),
        Truths = [CaterpillarTrue,LizardTrue,CatTrue],
        % exactly one of them ate the salt
        sat(card([1], Suspects)),
        % the statements
        sat(CaterpillarTrue =:= Lizard),
        sat(LizardTrue =:= Lizard),
        sat(CatTrue =:= ~Cat),
        % at least one of them tells the truth:
        sat(card([1,2,3], Truths)),
        % at least one of them lies:
        sat(card([1,2,3], [~CaterpillarTrue,~LizardTrue,~CatTrue])).

And from this the unique solution is readily determined without search:

?- solution(Pairs).
Pairs = [caterpillar-1, lizard-0, cat-0].