%------------------------------------------------------------------------------
% File     : PUZ087~2 : TPTP v9.0.0. Released v9.0.0.
% Domain   : Puzzles
% Problem  : Wise men
% Version  : Especial.
% English  : Once upon a time, a king wanted to find the wisest out of his
%            three wisest men. He arranged them in a circle and told them that
%            he would put a white or a black spot on their foreheads and that
%            one of the three spots would certainly be white. The three wise
%            men could see and hear each other but, of course, they could not
%            see their faces reflected anywhere. The king, then, asked to each
%            of them to find out the colour of his own spot. After a while, the
%            wisest correctly answered that his spot was white.

% Refs     : [Gol92] Goldblatt (1992), Logics of Time and Computation
%          : [Bal98] Baldoni (1998), Normal Multimodal Logics: Automatic De
% Source   : [TPTP]
% Names    : 

% Status   : Theorem
% Rating   : ? v9.0.0
% Syntax   : TBA
% SPC      : TFN_THM_NEQ

% Comments : Long connectives
%------------------------------------------------------------------------------
tff(simple_s5,logic,(
    $epistemic_modal ==
        [ $constants == $rigid,
          $quantification == $varying,
          $modalities == $modal_system_S5 ] )).

%----Type for the wise men
tff(agent_type,type,wiseman: $tType).

%----Three wise men
tff(man_a_type,type,a: wiseman).

tff(man_b_type,type,b: wiseman).

tff(man_c_type,type,c: wiseman).

tff(fool_type,type,fool: wiseman).

%---Property of a wiseman's hat: white_spot
tff(white_spot_type,type,white_spot: wiseman > $o).

%----At least one wiseman has a white spot
tff(at_least_one_white_spot,axiom,(
    {$knows(#index_fool)}((white_spot(a)) | (white_spot(b)) | (white_spot(c))) )).

%----If one agent has a white spot all other agents can see this
tff(b_knows_a,axiom,(
    {$knows(#index_fool)}(
      ( white_spot(a)
     => {$knows(#index_b)}(white_spot(a)) ) ) )).

tff(c_knows_a,axiom,(
    {$knows(#index_fool)}(
      ( white_spot(a)
     => {$knows(#index_c)}(white_spot(a)) ) ) )).

tff(a_knows_a,axiom,(
    {$knows(#index_fool)}(
      ( white_spot(b) 
     => {$knows(#index_a)}(white_spot(b)) ) ) )).

tff(c_knows_b,axiom,(
    {$knows(#index_fool)}(
      ( white_spot(b) 
     => {$knows(#index_c)}(white_spot(b)) ) ) )).

tff(a_knows_c,axiom,(
    {$knows(#index_fool)}(
      ( white_spot(c) 
     => {$knows(#index_a)}(white_spot(c)) ) ) )).

tff(b_knows_c,axiom,(
    {$knows(#index_fool)}(
      ( white_spot(c) 
     => {$knows(#index_b)}(white_spot(c)) ) ) )).

%----Black spots are visible
tff(b_knows_not_a,axiom,(
    {$knows(#index_fool)}(
      ( ~ white_spot(a) 
     => {$knows(#index_b)}(~ white_spot(a)) ) ) )).

tff(c_knows_not_a,axiom,(
    {$knows(#index_fool)}( 
      ( ~ white_spot(a) 
     => {$knows(#index_c)}(~ white_spot(a)) ) ) )).

tff(a_knows_not_b,axiom,(
    {$knows(#index_fool)}( 
      ( ~ white_spot(b) 
     => {$knows(#index_a)}(~ white_spot(b)) ) ) )).

tff(c_knows_not_b,axiom,(
    {$knows(#index_fool)}( 
      ( ~ white_spot(b) 
     => {$knows(#index_c)}(~ white_spot(b)) ) ) )).

tff(a_knows_not_c,axiom,(
    {$knows(#index_fool)}( 
      ( ~ white_spot(c) 
     => {$knows(#index_a)}(~ white_spot(c)) ) ) )).

tff(b_knows_not_c,axiom,(
    {$knows(#index_fool)}( 
      ( ~ white_spot(c) 
     => {$knows(#index_b)}(~ white_spot(c)) ) ) )).

%----a and b don't know their situation
tff(a_not_know,axiom,(
    {$knows(#index_fool)}(~ {$knows(#index_a)}(white_spot(a))) )).

tff(b_not_know,axiom,(
    {$knows(#index_fool)}(~ {$knows(#index_b)}(white_spot(b))) )).

%----Prove c knows white spot
tff(c_knows,conjecture,(
    {$knows(#index_c)}(white_spot(c)) )).

%------------------------------------------------------------------------------