[23d763]: / web / entries / Flyspeck-Tame.shtml  Maximize  Restore  History

Download this file

132 lines (110 with data), 5.0 kB

<!DOCTYPE public "-//w3c//dtd html 4.01 transitional//en"
		"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
  <title>Archive of Formal Proofs</title>
  <link rel="stylesheet" type="text/css" href="../front.css">
  <script src="../jquery.min.js"></script>
  <script src="../script.js"></script>
  <link rel="icon" href="../images/favicon.ico" type="image/icon">
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
</head>
<body>

<table width="100%">
  <tbody>
    <tr>
      <td width="20%" align="center" valign="top">
      <!-- navigation -->
      <!--#include file="nav.html"-->
      </td>
      <td width="80%" valign="top">
      <!-- content -->

<div align="center">
<p> </p>

<h1><font class="first">F</font>lyspeck
<font class="first">I</font>:
<font class="first">T</font>ame
<font class="first">G</font>raphs
</h1>
<p></p>
<table width="80%" class="data">
  <tbody>
    <tr><td class="datahead" width="20%">Title:</td>
        <td class="data" width="80%">Flyspeck I: Tame Graphs</td></tr>

    <tr><td class="datahead">Author:</td>
        <td class="data">Gertrud Bauer and <a href="http://www.in.tum.de/~nipkow">Tobias Nipkow</a></td></tr>

    <tr><td class="datahead">Submission date:</td>
        <td class="data">2006-05-22</td></tr>

    <tr><td class="datahead" valign="top">Abstract:</td>
        <td class="abstract">

These theories present the verified enumeration of <i>tame</i> plane graphs as defined by Thomas C. Hales in his <i>revised</i> proof of the Kepler Conjecture. The revison concerns the definition of tameness. The <a href="http://www.in.tum.de/~nipkow/pubs/Flyspeck/">IJCAR 2006 paper by Nipkow, Bauer and Schultz</a> refers to the original version of Hales' proof.
        </td></tr>

    <tr><td class="datahead" valign="top">Change history:</td>
        <td class="abstract">

[2010-11-02]: modified theories to reflect the modified
definition of tameness in Hales' revised proof.
        </td></tr>

    <tr><td class="datahead" valign="top">BibTeX:</td>
        <td class="formatted">
			<pre>@article{Flyspeck-Tame-AFP,
  author  = {Gertrud Bauer and Tobias Nipkow},
  title   = {Flyspeck I: Tame Graphs},
  journal = {Archive of Formal Proofs},
  month   = may,
  year    = 2006,
  note    = {\url{http://afp.sf.net/entries/Flyspeck-Tame.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}</pre>
        </td></tr>

    <tr><td class="datahead">License:</td>
        <td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>


<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
<!---INCLUDE- file="devel-warning.shtml"-->

  </tbody>
</table>

<p></p>

<!--#set var="name" value="Flyspeck-Tame" -->
<!--#set var="binfo" value="../browser_info/current/HOL/HOL-Library/${name}" -->

<!--#set var="doc" value="${binfo}/document.pdf" -->
<!--#set var="outline" value="${binfo}/outline.pdf" -->
<!--#set var="browse" value="${binfo}/index.html" -->
<!--#set var="tar" value="../release/afp-${name}-current.tar.gz" -->

<table class="links">
  <tbody>
    <tr>
  <td class="links">
	<a href="<!--#echo var="outline" -->">Proof outline</a><br>
	<a href="<!--#echo var="doc" -->">Proof document</a>
  </td>
	<!-- link to README.hmtl if no document exists -->	
	</tr>
    <tr>
  <td class="links">
	<a href="<!--#echo var="browse" -->">Browse theories</a>
	</td></tr>
    <tr>
  <td class="links"> 
	<a href="<!--#echo var="tar" -->">Download this entry</a>
	</td>
  </tr>
    <tr><td class="links">Older releases:
<ul>
<li>Isabelle 2012: <a href="../release/afp-<!--#echo var="name" -->-2012-05-25.tar.gz">afp-<!--#echo var="name" -->-2012-05-25.tar.gz</a></li>
<li>Isabelle 2011-1: <a href="../release/afp-<!--#echo var="name" -->-2011-10-11.tar.gz">afp-<!--#echo var="name" -->-2011-10-11.tar.gz</a></li>
<li>Isabelle 2011: <a href="../release/afp-<!--#echo var="name" -->-2011-02-11.tar.gz">afp-<!--#echo var="name" -->-2011-02-11.tar.gz</a></li>
<li>Isabelle 2009-2: <a href="../release/afp-<!--#echo var="name" -->-2010-06-30.tar.gz">afp-<!--#echo var="name" -->-2010-06-30.tar.gz</a></li>
<li>Isabelle 2009-1: <a href="../release/afp-<!--#echo var="name" -->-2009-12-12.tar.gz">afp-<!--#echo var="name" -->-2009-12-12.tar.gz</a></li>
<li>Isabelle 2009: <a href="../release/afp-<!--#echo var="name" -->-2009-04-29.tar.gz">afp-<!--#echo var="name" -->-2009-04-29.tar.gz</a></li>
<li>Isabelle 2008: <a href="../release/afp-<!--#echo var="name" -->-2008-06-10.tar.gz">afp-<!--#echo var="name" -->-2008-06-10.tar.gz</a></li>
<li>Isabelle 2007: <a href="../release/afp-<!--#echo var="name" -->-2008-01-04.tar.gz">afp-<!--#echo var="name" -->-2008-01-04.tar.gz</a></li>
<li>Isabelle 2007: <a href="../release/afp-<!--#echo var="name" -->-2007-11-27.tar.gz">afp-<!--#echo var="name" -->-2007-11-27.tar.gz</a></li>

</ul>    </td></tr>
  </tbody>
</table>
<!-- entry data end -->

</td> </tr> </table>

</body>
</html>