Contradiction in Prolog

Question

I'm testing Prolog ability to test contradiction. To test this, I came up with the following scenario:

There are three suspects: a, b, and c, who are on trial, and one of the suspect is guilty and the rest are innocent.

The facts of the case are,

(Fact 1) if a is innocent then c must be guilty, and

(Fact 2) if a is innocent then c must be innocent.

The answer to who is guilty is suspect 'a' because suspect 'c' cannot be both guilty and innocent. The following code is my implementation:

who_guilty(Suspects) :-
% Knowledge Base
Suspects=[[Name1,Sentence1],
            [Name2, Sentence2],
            [Name3,Sentence3]],

% Suspects
Names=[a,b,c],
Names=[Name1,Name2,Name3],

% One Is Guilty
Sentences=[innocent,innocent,guilty],
permutation(Sentences,[Sentence1,Sentence2,Sentence3]),

% If A Innocent Then C Is Guilty
(member([a,innocent],Suspects) -> member([c,guilty], Suspects) ; true),

% If A Innocent Then C Is Innocent
(member([a,innocent],Suspects) -> member([c,innocent], Suspects) ; true).

To get Prolog's answer, the query that needs to be run is who_guilty(S). Prolog will then output two identical answers:

S = [[a, guilty], [b, innocent], [c, innocent]] ?

S = [[a, guilty], [b, innocent], [c, innocent]]

My central question is how can I get only one answer instead of two?

Answer 1

Using clpb :

:- use_module(library(clpb)).

% 0 means guilty
% 1 means innocent
guilty(A,B,C) :-
    % only one is guilty
    sat(~A * B * C + A * ~B * C + A * B * ~C),
    % Fact 1
    sat(A =< ~C),
    % Fact 2
    sat(A =< C).

?- guilty(A,B,C).
A = 0,
B = C, C = 1.

Answer 2

A compact solution, that follows your intuition about expressing the facts.

who_guilty(L) :-
    select(guilty,L,[innocent,innocent]),
    ( L = [innocent,_,_] -> L = [_,_,guilty] ; true ),
    ( L = [innocent,_,_] -> L = [_,_,innocent] ; true ).

yields:

?- who_guilty(L).
L = [guilty, innocent, innocent] ;
false.

thanks to joel76 (+1), here is a more synthetic solution based on library(clpb)

?- sat(card([1],[A,B,C])*(~A =< ~C)*(~A =< C)).
A = 1,
B = C, C = 0.

1 means guilty...

Answer 3

Using clpfd library, you can solve this problem easily:

solve(L):-
    L = [A,B,C], %0 innocent, 1 guilty
    L ins 0..1,
    A + B + C #= 1, %one is guilty
    A #= 0 #==> C #= 1, %if a is innocent then c must be guilty
    A #= 0 #==> C #= 0, %if a is innocent then c must be innocent
    label(L).

?- solve(L).
L = [1, 0, 0]

Answer 4

You should add a new predicate which checks whether someone is both innocent and guilty, which then answers yes to whether there are contradictory outcomes. You are giving Prolog two facts, meaning two correct conclusions to the query. Your real question is "do I have facts contradicting each other?", which means A and NOT A are both true at the same time. contradiction(A, not(A)).

All truths are universal and you are giving two truths that are contradictory to Prolog, so both are true to Prolog.