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

DOI10.1007/S10817-022-09616-4OpenAlexW4206367340MaRDI QIDQ2102926FDOQ2102926

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

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

zbMATH Keywords

optimizationprobabilityinfinite graphIsabelle/HOLflow network

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (4)

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

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)