Преобразование логической головоломки в исчисление предикатов и пролог /dlv

Question

Вопрос в том, что соль была украдена! Что ж, выяснилось, что виновником был либо Гусеница, Билл Ящерица, либо Чеширский Кот. Трое были судимы и сделали следующие заявления в суде:

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

Как это случилось, по крайней мере, один из них солгал, и, по крайней мере, один сказал правду. Кто ел соль?

Я точно знаю, что если Билл верен, то все утверждения верны, а если Чешир верен, то все ложны, поэтому это должна быть гусеница.

Глядя в исчисление предикатов и программируя его, это будет примерно так:

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

В этой загадке есть одна приятная вещь: вам даже не нужна логика предикатов первого порядка для ее моделирования: достаточно использовать пропозициональную логику, потому что, может ли подозреваемый лгать или говорить правду, можно указать с помощью булевой переменной, а сами утверждения также являются только заявлениями над булевыми переменными.

Таким образом, рассмотрите возможность использования решателя ограничений над булевыми переменными при решении этой задачи с помощью Пролога. Смотрите 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].