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

DOI10.1007/S10817-022-09616-4MaRDI QIDQ2102926zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• The Max-Flow Min-Cut theorem for countable networks
• A measure-theoretical max-flow-min-cut problem
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• Formalizing the Edmonds-Karp algorithm
• On Gale's feasibility theorem for certain infinite networks

Cites work

• scientific article; zbMATH DE number 1301860 (Why is no real title available?)
• A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks
• A formalized hierarchy of probabilistic system types. Proof pearl
• A general framework for probabilistic characterizing formulae
• Deciding bisimilarity and similarity for probabilistic processes.
• Exploring the structure of an algebra text with locales
• Formal certification of code-based cryptographic proofs
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• Formalizing the Edmonds-Karp algorithm
• From types to sets by local type definition in higher-order logic
• Funktionen auf Produkträumen mit vorgegebenen Marginal-Funktionen
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Locales: a module system for mathematical theories
• Maximal Flow Through a Network
• Menger's theorem for graphs containing no infinite paths
• Menger's theorem for infinite graphs
• Probabilistic functions and cryptographic oracles in higher order logic
• Probability on trees and networks
• Proofs of randomized algorithms in Coq
• Random walks in Dirichlet environment: an overview. Dedicated to Dominique Bakry on the occasion of his 60th birthday
• Semantics of probabilistic processes. An operational approach
• Sur le théorème de Zorn
• The Existence of Probability Measures with Given Marginals
• The Max-Flow Min-Cut theorem for countable networks
• Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems
• Transfinite constructions in classical type theory
• Truly modular (co)datatypes for Isabelle/HOL
• Types for Proofs and Programs
• \(*\)-liftings for differential privacy

Cited in

(4)

• The Max-Flow Min-Cut theorem for countable networks
• Formalizing the Edmonds-Karp algorithm
• A measure-theoretical max-flow-min-cut problem
• A theory of composition for differential obliviousness

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2102926)