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

【问题标题】：Converting logical puzzle into predicate calculus and prolog/dlv将逻辑难题转换为谓词演算和 prolog/dlv
【发布时间】：2015-11-05 20:33:27
【问题描述】：

问题是：盐被偷了！嗯，发现罪魁祸首要么是毛毛虫，要么比尔蜥蜴或柴郡猫。这三个都试过了，做了以下法庭陈述：

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

但是，然后在谓词逻辑中进一步描述这一点，我不会如何描述他们所做的描述或请求。如果一个陈述是真的，那又如何暗示其他陈述可能是假的。

【问题讨论】：

标签： prolog logic predicate answer-set-programming

【解决方案1】：

关于这个谜题的一个好处是，您甚至不需要一阶 谓词逻辑 来对其建模：使用命题逻辑就足够了，因为无论是嫌疑人说谎或说真话可以用布尔变量表示，语句本身也只是对布尔变量的语句。

因此，在使用 Prolog 解决此任务时，请考虑在 Boolean 变量上使用约束求解器。有关这方面的更多信息，请参阅 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].

【讨论】：