Conversion de puzzle logique en calcul de prédicat et prolog/dlv

Question

La question est: Le sel a été volé! Eh bien, il a été constaté que le coupable était soit le Caterpillar, Bill le lézard ou le chat du Cheshire. Les trois ont été jugés et ont fait les déclarations suivantes au tribunal:

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

Comme il est arrivé, au moins un d'entre eux mentaient et au moins un dit la vérité. Qui a mangé le sel ?

Je sais avec certitude si la facture est vraie, que toutes les déclarations sont vraies, et si le cheshire est vrai, alors tous sont faux, donc ce doit être la chenille.

regardant dans le calcul des prédicats et la programmation, ce serait quelque chose comme ce droit:

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 

Mais qui décrit plus loin cette logique sous-jacente, je ne sais pas comment je qualifierais de descriptions ou un plaidoyer qu'ils ont fabriqué. Et comment cela si une déclaration est vraie peut impliquer que d'autres peuvent être des faux.

Answer 1

Une bonne chose au sujet de ce casse-tête est que vous ne devez même pas de premier ordre logique sous-jacente pour modéliser: Il suffit d'utiliser logique propositionnelle, parce que si un suspect est ou dit peut être indiquée la vérité une variable booléenne, et les instructions elles-mêmes ne sont que des instructions sur des variables booléennes.

Ainsi, pensez à utiliser un solveur de contraintes sur Boolean variables lors de la résolution de cette tâche avec Prolog. Voir clpb pour plus d'informations à ce sujet.

Voici une solution d'échantillon, en utilisant SICStus Prolog ou 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])). 

Et de cette solution unique est facilement déterminée sans recherche:

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