From 606d9ad08ad1f0e1a37fa60d88fa0ab9e066dd64 Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Thu, 16 Dec 2010 21:53:51 +0100 Subject: [PATCH] doc: Einstein Logic Problem --- doc/manual.tex | 6 +++--- doc/syntax.tex | 49 +++++++++++++++++++++++++++++++++++++++++++++---- 2 files changed, 48 insertions(+), 7 deletions(-) diff --git a/doc/manual.tex b/doc/manual.tex index d0c8036ec..7282da487 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -146,10 +146,10 @@ Johannes Kanig, St\'ephane Lescuyer, Sim\~ao Melo de Sousa. \input{manpages.tex} -\chapter{Complete API documentation} -\label{chap:apidoc} +% \chapter{Complete API documentation} *) +% \label{chap:apidoc} *) -\input{./apidoc.tex} +% \input{./apidoc.tex} *) \bibliographystyle{abbrv} \bibliography{manual} diff --git a/doc/syntax.tex b/doc/syntax.tex index bbd92d08d..93e451027 100644 --- a/doc/syntax.tex +++ b/doc/syntax.tex @@ -104,9 +104,42 @@ the length of a list is non-negative. We now consider another, slightly more complex example: to use \why\ to solve a little puzzle known as Einstein's logic problem''\footnote{This was contributed by St\'ephane Lescuyer.}. -The problem is stated as follows. +The problem is stated as follows. Five persons, of five +different nationalities, live in five houses in a row, all +painted with different colors. +These five persones own different pets, drink different beverages and +smoke different brands of cigars. +We are given the following information: \begin{itemize} -\item TODO +\item The Englishman lives in a red house; + +\item The Swede has dogs; + +\item The Dane drinks tea; + +\item The green house is on the left of the white one; + +\item The green house's owner drinks coffee; + +\item The person who smokes Pall Mall has birds; + +\item The yellow house's owner smokes Dunhill; + +\item In the house in the center lives someone who drinks milk; + +\item The Norwegian lives in the first house; + +\item The man who smokes Blends lives next to the one who has cats; + +\item The man who owns a horse lives next to the one who smokes Dunhills; + +\item The man who smokes Blue Masters drinks beer; + +\item The German smokes Prince; + +\item The Norwegian lives next to the blue house; + +\item The man who smokes Blends has a neighbour who drinks water. \end{itemize} The question is: what is the nationality of the fish's owner? @@ -206,9 +239,17 @@ this theory. neighbour (Owner.to (Cigar.to Blend)) (Owner.to (Drink.to Water)) end \end{verbatim} +Finally, we declare the goal in a fourth theory +\begin{verbatim} +theory Problem "Goal of Einstein's problem" + use import Einstein + use import EinsteinHints -TODO - + goal G: Pet.to Fish = German +end +\end{verbatim} +and we are ready to use \why\ to discharge this goal with any prover +of our choice. %%% Local Variables: %%% mode: latex -- GitLab