A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory

DOI10.1007/s10817-022-09616-4OpenAlexW4206367340MaRDI QIDQ2102926

Andreas Lochbihler

Publication date: 12 December 2022

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-022-09616-4

zbMATH Keywords

optimizationprobabilityinfinite graphIsabelle/HOLflow network

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

A theory of composition for differential obliviousness

Uses Software

• Isabelle/HOL
• Locales
• Transfer
• Lifting
• Zoo Probabilistic Systems
• Edmonds-Karp
• Archive Formal Proofs
• Probabilistic_While
• MFMC_Countable

Cites Work

• Unnamed Item
• Unnamed Item
• Menger's theorem for graphs containing no infinite paths
• The Max-Flow Min-Cut theorem for countable networks
• Proofs of randomized algorithms in Coq
• Menger's theorem for infinite graphs
• From types to sets by local type definition in higher-order logic
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• Deciding bisimilarity and similarity for probabilistic processes.
• Random walks in Dirichlet environment: an overview. Dedicated to Dominique Bakry on the occasion of his 60th birthday
• Exploring the structure of an algebra text with locales
• Locales: a module system for mathematical theories
• Funktionen auf Produkträumen mit vorgegebenen Marginal-Funktionen
• Sur le théorème de Zorn
• Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
• Formalizing the Edmonds-Karp Algorithm
• Probability on Trees and Networks
• Truly Modular (Co)datatypes for Isabelle/HOL
• A General Framework for Probabilistic Characterizing Formulae
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• A Formalized Hierarchy of Probabilistic System Types
• Transfinite Constructions in Classical Type Theory
• Maximal Flow Through a Network
• Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems
• Formal certification of code-based cryptographic proofs
• Semantics of Probabilistic Processes
• The Existence of Probability Measures with Given Marginals
• Types for Proofs and Programs
• A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks

This page was built for publication: A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory