将逻辑难题转换为谓词演算和 prolog/dlv

Question

问题是：盐被偷了！好吧，我们发现罪魁祸首要么是毛毛虫， 蜥蜴比尔或柴郡猫。三者经过尝试，做出如下 法庭陈述：

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

碰巧的是，他们中至少有一个说谎，至少一个说真话。谁吃了 盐？

我确定如果 bill 是真的，那么所有的陈述都是真的，如果 cheshire 是真的，那么所有的都是假的，所以它一定是毛毛虫。

查看谓词演算并对其进行编程，它应该是这样的：

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

但是在谓词逻辑中进一步描述这一点，我不知道如何描述他们所做的描述或请求。以及如果一个陈述为真如何暗示其他陈述可能为假。

Answer 1

这个谜题的一个好处是你甚至不需要一阶谓词逻辑来建模：使用命题[=24就足够了=] 逻辑，因为嫌疑人是说谎还是说真话可以用一个布尔变量来表示，而陈述本身也只是对布尔变量的陈述。

因此，在使用 Prolog 解决此任务时，请考虑在 布尔值 变量上使用约束求解器。有关详细信息，请参阅 clpb。

这是一个示例解决方案，使用 SICStus Prolog 或 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])).

由此无需搜索即可轻松确定唯一解：

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