Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
119
Issues
119
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
606d9ad0
Commit
606d9ad0
authored
Dec 16, 2010
by
Jean-Christophe Filliâtre
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
doc: Einstein Logic Problem
parent
1b919e57
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
48 additions
and
7 deletions
+48
-7
doc/manual.tex
doc/manual.tex
+3
-3
doc/syntax.tex
doc/syntax.tex
+45
-4
No files found.
doc/manual.tex
View file @
606d9ad0
...
...
@@ -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
}
...
...
doc/syntax.tex
View file @
606d9ad0
...
...
@@ -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
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment