Commit 316362be authored by Manuel Eberl's avatar Manuel Eberl
Browse files

sitegen for Blue_Eyes

parent 17c110a297d8
......@@ -10066,3 +10066,17 @@ abstract =
work is partially described in Mansky and Gunter's paper at CPP
2019 and Mansky's doctoral thesis (UIUC, 2020).
 
[Blue_Eyes]
title = Solution to the xkcd Blue Eyes puzzle
author = Jakub Kądziołka <mailto:kuba@kadziolka.net>
topic = Mathematics/Misc
date = 2021-01-30
notify = kuba@kadziolka.net
abstract =
In a <a href="https://xkcd.com/blue_eyes.html">puzzle published by
Randall Munroe</a>, perfect logicians forbidden
from communicating are stranded on an island, and may only leave once
they have figured out their own eye color. We present a method of
modeling the behavior of perfect logicians and formalize a solution of
the puzzle.
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>Solution to the xkcd Blue Eyes puzzle - Archive of Formal Proofs
</title>
<link rel="stylesheet" type="text/css" href="../front.css">
<link rel="icon" href="../images/favicon.ico" type="image/icon">
<link rel="alternate" type="application/rss+xml" title="RSS" href="../rss.xml">
<!-- MathJax for LaTeX support in abstracts -->
<script>
MathJax = {
tex: {
inlineMath: [['$', '$'], ['\\(', '\\)']]
},
processEscapes: true,
svg: {
fontCache: 'global'
}
};
</script>
<script id="MathJax-script" async src="../components/mathjax/es5/tex-mml-chtml.js"></script>
</head>
<body class="mathjax_ignore">
<table width="100%">
<tbody>
<tr>
<!-- Navigation -->
<td width="20%" align="center" valign="top">
<p>&nbsp;</p>
<a href="https://www.isa-afp.org/">
<img src="../images/isabelle.png" width="100" height="88" border=0>
</a>
<p>&nbsp;</p>
<p>&nbsp;</p>
<table class="nav" width="80%">
<tr>
<td class="nav" width="100%"><a href="../index.html">Home</a></td>
</tr>
<tr>
<td class="nav"><a href="../about.html">About</a></td>
</tr>
<tr>
<td class="nav"><a href="../submitting.html">Submission</a></td>
</tr>
<tr>
<td class="nav"><a href="../updating.html">Updating Entries</a></td>
</tr>
<tr>
<td class="nav"><a href="../using.html">Using Entries</a></td>
</tr>
<tr>
<td class="nav"><a href="../search.html">Search</a></td>
</tr>
<tr>
<td class="nav"><a href="../statistics.html">Statistics</a></td>
</tr>
<tr>
<td class="nav"><a href="../topics.html">Index</a></td>
</tr>
<tr>
<td class="nav"><a href="../download.html">Download</a></td>
</tr>
</table>
<p>&nbsp;</p>
<p>&nbsp;</p>
</td>
<!-- Content -->
<td width="80%" valign="top">
<div align="center">
<p>&nbsp;</p>
<h1> <font class="first">S</font>olution
to
the
xkcd
<font class="first">B</font>lue
<font class="first">E</font>yes
puzzle
</h1>
<p>&nbsp;</p>
<table width="80%" class="data">
<tbody>
<tr>
<td class="datahead" width="20%">Title:</td>
<td class="data" width="80%">Solution to the xkcd Blue Eyes puzzle</td>
</tr>
<tr>
<td class="datahead">
Author:
</td>
<td class="data">
Jakub Kądziołka (kuba /at/ kadziolka /dot/ net)
</td>
</tr>
<tr>
<td class="datahead">Submission date:</td>
<td class="data">2021-01-30</td>
</tr>
<tr>
<td class="datahead" valign="top">Abstract:</td>
<td class="abstract mathjax_process">
In a <a href="https://xkcd.com/blue_eyes.html">puzzle published by
Randall Munroe</a>, perfect logicians forbidden
from communicating are stranded on an island, and may only leave once
they have figured out their own eye color. We present a method of
modeling the behavior of perfect logicians and formalize a solution of
the puzzle.</td>
</tr>
<tr>
<td class="datahead" valign="top">BibTeX:</td>
<td class="formatted">
<pre>@article{Blue_Eyes-AFP,
author = {Jakub Kądziołka},
title = {Solution to the xkcd Blue Eyes puzzle},
journal = {Archive of Formal Proofs},
month = jan,
year = 2021,
note = {\url{https://isa-afp.org/entries/Blue_Eyes.html},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td>
</tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
</tbody>
</table>
<p></p>
<table class="links">
<tbody>
<tr>
<td class="links">
<a href="../browser_info/current/AFP/Blue_Eyes/outline.pdf">Proof outline</a><br>
<a href="../browser_info/current/AFP/Blue_Eyes/document.pdf">Proof document</a>
</td>
</tr>
<tr>
<td class="links">
<a href="../browser_info/current/AFP/Blue_Eyes/index.html">Browse theories</a>
</td></tr>
<tr>
<td class="links">
<a href="../release/afp-Blue_Eyes-current.tar.gz">Download this entry</a>
</td>
</tr>
<tr><td class="links">Older releases:
None
</td></tr>
</tbody>
</table>
</div>
</td>
</tr>
</tbody>
</table>
<script src="../jquery.min.js"></script>
<script src="../script.js"></script>
</body>
</html>
\ No newline at end of file
......@@ -95,6 +95,14 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
Author:
Roland Coghetto
</td>
</tr>
<tr>
<td class="entry">
2021-01-30: <a href="entries/Blue_Eyes.html">Solution to the xkcd Blue Eyes puzzle</a>
<br>
Author:
Jakub Kądziołka
</td>
</tr>
<tr>
<td class="entry">
......
......@@ -41,6 +41,20 @@ postulate of Euclid and Euclid&#39;s original parallel postulate. These
proofs, which are not constructive, are directly inspired by Pierre
Boutry, Charly Gries, Julien Narboux and Pascal Schreck.
&lt;/p&gt;</description>
</item>
<item>
<title>Solution to the xkcd Blue Eyes puzzle</title>
<link>https://www.isa-afp.org/entries/Blue_Eyes.html</link>
<guid>https://www.isa-afp.org/entries/Blue_Eyes.html</guid>
<dc:creator> Jakub Kądziołka </dc:creator>
<pubDate>30 Jan 2021 00:00:00 +0000</pubDate>
<description>
In a &lt;a href=&#34;https://xkcd.com/blue_eyes.html&#34;&gt;puzzle published by
Randall Munroe&lt;/a&gt;, perfect logicians forbidden
from communicating are stranded on an island, and may only leave once
they have figured out their own eye color. We present a method of
modeling the behavior of perfect logicians and formalize a solution of
the puzzle.</description>
</item>
<item>
<title>JinjaDCI: a Java semantics with dynamic class initialization</title>
......@@ -588,26 +602,5 @@ Computer Systems, 3, 63-75, 1985]. Our main result is a formal
termination and correctness proof of the Chandy--Lamport algorithm and
its use in stable property detection.</description>
</item>
<item>
<title>Relational Characterisations of Paths</title>
<link>https://www.isa-afp.org/entries/Relational_Paths.html</link>
<guid>https://www.isa-afp.org/entries/Relational_Paths.html</guid>
<dc:creator> Walter Guttmann, Peter Höfner </dc:creator>
<pubDate>13 Jul 2020 00:00:00 +0000</pubDate>
<description>
Binary relations are one of the standard ways to encode, characterise
and reason about graphs. Relation algebras provide equational axioms
for a large fragment of the calculus of binary relations. Although
relations are standard tools in many areas of mathematics and
computing, researchers usually fall back to point-wise reasoning when
it comes to arguments about paths in a graph. We present a purely
algebraic way to specify different kinds of paths in Kleene relation
algebras, which are relation algebras equipped with an operation for
reflexive transitive closure. We study the relationship between paths
with a designated root vertex and paths without such a vertex. Since
we stay in first-order logic this development helps with mechanising
proofs. To demonstrate the applicability of the algebraic framework we
verify the correctness of three basic graph algorithms.</description>
</item>
</channel>
</rss>
This diff is collapsed.
......@@ -897,6 +897,7 @@
<a href="entries/FunWithFunctions.html">FunWithFunctions</a> &nbsp;
<a href="entries/FunWithTilings.html">FunWithTilings</a> &nbsp;
<a href="entries/IMO2019.html">IMO2019</a> &nbsp;
<a href="entries/Blue_Eyes.html">Blue_Eyes</a> &nbsp;
</div>
<h2>Tools</h2>
<div class="list">
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment