Commit 853b029c authored by nipkow's avatar nipkow
Browse files

new entry Cartan_FP

parent 38de4f7e4d60
......@@ -3286,6 +3286,20 @@ abstract = This article contains a formalisation of the Akra-Bazzi method
proof methods, see the accompanying paper (publication forthcoming).
depends-on = Landau_Symbols
[Cartan_FP]
title = The Cartan Fixed Point Theorems
author = Lawrence Paulson <http://www.cl.cam.ac.uk/~lp15/>
date = 2016-03-08
topic = Mathematics/Analysis
abstract =
The Cartan fixed point theorems concern the group of holomorphic
automorphisms on a connected open set of C<sup>n</sup>. Ciolli et al.
have formalised the one-dimensional case of these theorems in HOL
Light. This entry contains their proofs, ported to Isabelle/HOL. Thus
it addresses the authors~ remark that "it would be important to write
a formal proof in a language that can be read by both humans and
machines".
[Gauss_Jordan]
title = Gauss-Jordan Algorithm and Its Applications
author = Jose Divasón <http://www.unirioja.es/cu/jodivaso>, Jesús Aransay <http://www.unirioja.es/cu/jearansa>
......
This diff is collapsed.
chapter AFP
session Cartan_FP (AFP) = "HOL-Multivariate_Analysis" +
description {* The Cartan Fixed Point Theorems. *}
options [timeout = 300]
theories
Cartan
document_files
"root.bib"
"root.tex"
%% This BibTeX bibliography file was created using BibDesk.
%% http://bibdesk.sourceforge.net/
%% Created for Larry Paulson at 2016-03-08 17:12:34 +0000
%% Saved with string encoding Unicode (UTF-8)
@article{ciolli-cartan,
Author = {Ciolli, Gianni and Gentili, Graziano and Maggesi, Marco},
Date-Added = {2016-03-08 17:11:17 +0000},
Date-Modified = {2016-03-08 17:12:34 +0000},
Doi = {10.1007/s10817-010-9198-6},
Journal = {J. Autom. Reason.},
Keywords = {Cartan fixed point theorems, Complex analysis, Formal proving},
Month = oct,
Number = {3},
Pages = {319-336},
Publisher = {Springer},
Title = {A Certified Proof of the {Cartan} Fixed Point Theorems},
Url = {http://dx.doi.org/10.1007/s10817-010-9198-6},
Volume = {47},
Year = {2011},
Bdsk-Url-1 = {http://dx.doi.org/10.1007/s10817-010-9198-6}}
\documentclass[11pt,a4paper]{report}
\usepackage{isabelle,isabellesym}
\usepackage{amssymb}
% this should be the last package used
\usepackage{pdfsetup}
% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}
\begin{document}
\title{The Cartan Fixed Point Theorems}
\author{Lawrence C. Paulson}
\maketitle
\begin{abstract}
The Cartan fixed point theorems concern the group of holomorphic automorphisms on a connected open set of $\mathbb{C}^n$. Ciolli et al.\ \cite{ciolli-cartan} have formalised the one-dimensional case of these theorems in HOL Light. This entry contains their proofs, ported to Isabelle/HOL\@. Thus it addresses the authors’ remark that ``it would be important to write a formal proof in a language that can be read by both humans and machines.''
\end{abstract}
\tableofcontents
% include generated text of all theories
\input{session}
\bibliographystyle{abbrv}
\bibliography{root}
\end{document}
......@@ -24,6 +24,7 @@ BytecodeLogicJmlTypes
Card_Number_Partitions
CCS
Call_Arity
Cartan_FP
Case_Labeling
Category
Category2
......
<!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=utf-8">
</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>&nbsp;</p>
<h1><font class="first">T</font>he
<font class="first">C</font>artan
<font class="first">F</font>ixed
<font class="first">P</font>oint
<font class="first">T</font>heorems
</h1>
<p></p>
<table width="80%" class="data">
<tbody>
<tr><td class="datahead" width="20%">Title:</td>
<td class="data" width="80%">The Cartan Fixed Point Theorems</td></tr>
<tr><td class="datahead">Author:</td>
<td class="data"><a href="http://www.cl.cam.ac.uk/~lp15/">Lawrence Paulson</a></td></tr>
<tr><td class="datahead">Submission date:</td>
<td class="data">2016-03-08</td></tr>
<tr><td class="datahead" valign="top">Abstract:</td>
<td class="abstract">
The Cartan fixed point theorems concern the group of holomorphic
automorphisms on a connected open set of C<sup>n</sup>. Ciolli et al.
have formalised the one-dimensional case of these theorems in HOL
Light. This entry contains their proofs, ported to Isabelle/HOL. Thus
it addresses the authors~ remark that "it would be important to write
a formal proof in a language that can be read by both humans and
machines".
</td></tr>
<tr><td class="datahead" valign="top">BibTeX:</td>
<td class="formatted">
<pre>@article{Cartan_FP-AFP,
author = {Lawrence Paulson},
title = {The Cartan Fixed Point Theorems},
journal = {Archive of Formal Proofs},
month = mar,
year = 2016,
note = {\url{http://afp.sf.net/entries/Cartan_FP.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="Cartan_FP" -->
<!--#set var="binfo" value="../browser_info/current/AFP/${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:
None </td></tr>
</tbody>
</table>
<!-- entry data end -->
</td> </tr> </table>
</body>
</html>
......@@ -49,6 +49,13 @@ A <a href="devel.shtml">development version</a> of the archive is available as w
<td class="head">2016</td>
</tr>
<tr><td class="entry">
2016-03-08:
<a href="entries/Cartan_FP.shtml">The Cartan Fixed Point Theorems</a>
<br>Author:
<a href="http://www.cl.cam.ac.uk/~lp15/">Lawrence Paulson</a>
</td></tr>
<tr><td class="entry">
2016-03-01:
<a href="entries/LTL.shtml">Linear Temporal Logic</a>
......
......@@ -356,6 +356,7 @@
<a href="entries/Special_Function_Bounds.shtml">Special_Function_Bounds</a> &nbsp;
<a href="entries/Landau_Symbols.shtml">Landau_Symbols</a> &nbsp;
<a href="entries/Akra_Bazzi.shtml">Akra_Bazzi</a> &nbsp;
<a href="entries/Cartan_FP.shtml">Cartan_FP</a> &nbsp;
</div>
<h3>Probability Theory</h3>
......
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