to create a frame with the knowledge of a specific subject in a certain point of time. But in our process, one subject will reason about what another is thinking in a recursive way (in the similar process as the minimax algorithm).As the day follows,\[\begin{matrix}d_i & | & O(\phi) \\ d_{i+1} & | & \phi\end{matrix}\]In a frame of day \(d_i\) of subject \(X\):\[BlueEyed(X) \Rightarrow O(Leave(X))\]But, as the problem was announced no subject leave until \(n^{\text{th}}\) - last day: \[\begin{matrix}\forall X, i < n, d_i \square_X & | & \neg Leave(X)\end{matrix}\]Two vampires exampleLet us assume only two vampires: Anna and Maria. Both vampires know\[\begin{matrix}BlueEyed(Maria) \vee BlueEyed(Anna)\end{matrix}\]Now, let us examine Maria reasoning, \(\square_{\text{Maria}}\)... \[\begin{matrix}\neg BlueEyed(Maria) & \text{(hypothesis)} \\BlueEyed(Anna) & \text{(unit propagation)} \\O(Leave(Anna)) & \text{(prognosis: next day Anna leaves)}\end{matrix}\]However, next day, Anna did not leave (what is a contradiction \(\bot\) - hypothesis is false). Therefore,\[\begin{matrix}\vDash BlueEyed(Maria) & \text{(law of the excluded middle)}\end{matrix}\]Three vampires exampleNow lets do that for 3 vampires: Anna, Maria and John.Global knowledge\[\begin{matrix}BlueEyed(Maria) \vee BlueEyed(Anna) \vee BlueEyed(John) \\BlueEyed(X) \Rightarrow O(Leave(X))\end{matrix}\]At, any time, there are 3 frames...: (frame 1) What Maria is thinking...(frame 2) What Maria thinks what Anna is thinking and (frame 3) What Maria thinks what Anna thinks what John is thiking.Maria hypothesis is \(\neg BlueEyed(Maria)\). But she also KNOWS (\(\Rightarrow\) she is SURE about that) that Anna would be thinking the same way. So, if Maria hypothesis is right, for Anna, Maria would be not BlueEyed. At same time, Anna would be considering herself as not blue eyed by her own hypothesis. And, applying the same reasoning, Anna would consider what John would be thinking. And that third frame would inheritated not blue eyed for Maria and not blue eyed for Anna. Therefore, John would know that he is the only one with blue eyes and for Anna (according with Maria reasoning) the conclusion would be that John leaves next day.However, John would not leave. So, Anna hypothesis was wrong (in frame 2). So, in frame 2, Anna concludes that she has blue eyes. But next day Anna does not leave. So Maria concludes that she must have blue eyes.\[\begin{matrix}& BlueEyed(Maria) BlueEyed(Anna) BlueEyed(John) \\& BlueEyed(X) \Rightarrow O(Leave(X)) \\d_0| & \neg BlueEyed(Maria) & \text{(Maria hypothesis)} \\d_0| & \neg BlueEyed(Anna) & \text{(Anna hypothesis over Maria hypothesis)} \\d_0| & BlueEyed(John) & \text{(unit propagation)} \\d_0| & O(Leave(John)) & \text{(prognosis)}\end{matrix}\]The next day prognosis...\[\begin{matrix}d_1| & Leave(John) & \end{matrix}\]at \(d_1\) ...\[\begin{matrix}d_1| & \neg Leave(John) \bot \\d_1| & BlueEyed(Anna) & \text{(law of the excluded middle)} \\d_1| & O(Leave(Anna)) & \text{(prognosis)}\end{matrix}\]So \[\begin{matrix}d_2 & Leave(Anna) & \text{(prognosis)}\end{matrix}\]at \(d_2\) ...\[\begin{matrix}d_2|& \neg Leave(Anna) \bot \\d_2 & \vDash BlueEyed(Maria)\end{matrix}\]