honest_and_liar.why

theory Situation
  type person = A | B | C 
  type status = Honest | Liar

  function status (person) : status

  axiom Honest_is_the_only_one:
    (status A = Honest /\ status B = Liar   /\ status C = Liar) \/
    (status A = Liar   /\ status B = Honest /\ status C = Liar) \/
    (status A = Liar   /\ status B = Liar   /\ status C = Honest)

  (* aが「bはsだ」と言った *)
  predicate evidence (a b : person) (s : status) =
    if status a = Honest then status b = s else status b <> s

  (* A「私は正直者です。」 *)
  axiom evidence_A: evidence A A Honest
  (* B「Aはうそつきです。私が正直者です。」 *)
  axiom evidence_B: evidence B A Liar /\ evidence B B Honest
  (* C「Bはうそつきです。本当の正直者は私です。」 *)
  axiom evidence_C: evidence C B Liar /\ evidence C C Honest
end

theory Goals
  use import Situation

  (* goal A_is_Honest: status A = Honest *)
  goal B_is_Honest: status B = Honest
  (* goal C_is_Honest: status C = Honest *)
end