Commit 5abfdaef authored by gerwin.klein@nicta.com.au's avatar gerwin.klein@nicta.com.au
Browse files

web page for MFMC_Countable

parent c41c17f19693
<!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">A</font>
formal
proof
of
the
max-flow
min-cut
theorem
for
countable
networks
</h1>
<p></p>
<table width="80%" class="data">
<tbody>
<tr><td class="datahead" width="20%">Title:</td>
<td class="data" width="80%">A formal proof of the max-flow min-cut theorem for countable networks</td></tr>
<tr><td class="datahead">Author:</td>
<td class="data"><a href="http://www.infsec.ethz.ch/people/andreloc">Andreas Lochbihler</a></td></tr>
<tr><td class="datahead">Submission date:</td>
<td class="data">2016-05-09</td></tr>
<tr><td class="datahead" valign="top">Abstract:</td>
<td class="abstract">
This article formalises a proof of the maximum-flow minimal-cut
theorem for networks with countably many edges. A network is a
directed graph with non-negative real-valued edge labels and two
dedicated vertices, the source and the sink. A flow in a network
assigns non-negative real numbers to the edges such that for all
vertices except for the source and the sink, the sum of values on
incoming edges equals the sum of values on outgoing edges. A cut is a
subset of the vertices which contains the source, but not the sink.
Our theorem states that in every network, there is a flow and a cut
such that the flow saturates all the edges going out of the cut and is
zero on all the incoming edges. The proof is based on the paper
<emph>The Max-Flow Min-Cut theorem for countable networks</emph> by
Aharoni et al. As an application, we derive a characterisation of the
lifting operation for relations on discrete probability distributions,
which leads to a concise proof of its distributivity over relation
composition.
</td></tr>
<tr><td class="datahead" valign="top">BibTeX:</td>
<td class="formatted">
<pre>@article{MFMC_Countable-AFP,
author = {Andreas Lochbihler},
title = {A formal proof of the max-flow min-cut theorem for countable networks},
journal = {Archive of Formal Proofs},
month = may,
year = 2016,
note = {\url{http://isa-afp.org/entries/MFMC_Countable.shtml},
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>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Coinductive.shtml">Coinductive</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="MFMC_Countable" -->
<!--#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-05-09:
<a href="entries/MFMC_Countable.shtml">A formal proof of the max-flow min-cut theorem for countable networks</a>
<br>Author:
<a href="http://www.infsec.ethz.ch/people/andreloc">Andreas Lochbihler</a>
</td></tr>
<tr><td class="entry">
2016-05-05:
<a href="entries/Randomised_Social_Choice.shtml">Randomised Social Choice Theory</a>
......
......@@ -421,6 +421,7 @@
<h3>Graph Theory</h3>
<div class="list">
<a href="entries/MFMC_Countable.shtml">MFMC_Countable</a> &nbsp;
<a href="entries/ShortestPath.shtml">ShortestPath</a> &nbsp;
<a href="entries/Gabow_SCC.shtml">Gabow_SCC</a> &nbsp;
<a href="entries/Graph_Theory.shtml">Graph_Theory</a> &nbsp;
......
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