\documentclass{article}

\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{../lib/tex/naproche-puzzle}

\title{Dwarfs and Hats}
\author{\Naproche{} Formalization: Steffen Frerix and Peter Koepke}
\date{2018 and 2021}

\begin{document}
\pagenumbering{gobble}

\maketitle

\section{Introduction}

We present a formalized solution in \Naproche of a simple ``hat problem'':

\begin{quotation}
The two dwarfs Sigbert and Tormund are on an expedition and get captured
by an indigenous tribe. In order to be released they are given the following
challenge: Both of them will be placed in a room and will be given a hat. They
can only see the hat the other dwarf is wearing. The hats are either white or black.
Without further communication, one of the dwarfs must be able to name the color of
his hat.
The two may agree on a strategy before they are placed in the room. How can they manage
to be released?
\end{quotation}

We use some \LaTeX{} techniques described in the "agatha" files.


\section{Dwarf Ontology}

\begin{forthel}

[synonym dwarf/dwarfs]

\begin{signature}
A dwarf is a notion.
\end{signature}

\begin{signature}
Sigbert is a dwarf.
\end{signature}

\begin{signature}
Tormund is a dwarf.
\end{signature}

Let aDwarf, ADwarf denote dwarfs.

\begin{signature}
A hat is a notion.
\end{signature}

Let aHat denote a hat.

\begin{signature}
The hat of aDwarf is a hat.
\end{signature}

\begin{signature}
A color is a notion.
\end{signature}

\begin{signature}
White is a color.
\end{signature}

\begin{signature}
Black is a color.
\end{signature}

Let aColor denote a color.

\begin{signature}
The opposite color of aColor is a color.
\end{signature}

\begin{axiom}
The opposite color of White is Black.
\end{axiom}

\begin{axiom}
The opposite color of Black is White.
\end{axiom}

\begin{signature}
The color of aHat is a color.
\end{signature}

\begin{axiom}
The color of the hat of aDwarf is White or
the color of the hat of aDwarf is Black.
\end{axiom}

\begin{signature}
aDwarf names aColor is an atom.
\end{signature}

\begin{definition}
ADwarf names theColor of his hat iff ADwarf names the color
of the hat of ADwarf.
\end{definition}

\end{forthel}


\section{The Challenge}

\begin{forthel}

\begin{definition}
Both dwarfs get released iff some Dwarf names theColor of his hat.
\end{definition}

\end{forthel}


\section{The Strategy of the Dwarfs}

\begin{forthel}

\begin{axiom}
Sigbert names the opposite color of the color of the hat of Tormund.
\end{axiom}

\begin{axiom}
Tormund names the color of the hat of Sigbert.
\end{axiom}

\end{forthel}


\section{Release!}

\begin{forthel}

\begin{theorem}
Both dwarfs get released.
\end{theorem}

\end{forthel}

\end{document}
