scientific article; zbMATH DE number 7566066

MaRDI QIDQ5094138

Pierre-Yves Strub, Xavier Allamigeon, Ricardo D. Katz

Publication date: 2 August 2022

Full work available at URL: https://arxiv.org/abs/2104.15021

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

linear programmingsimplex methodconvex polyhedraformalization of mathematicsface lattice

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Uses Software

• Apron
• Coq
• PPL

Cites Work

• Unnamed Item
• Unnamed Item
• A counterexample to the Hirsch conjecture
• On the graph structure of convex polyhedra in \(n\)-space
• Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof
• Mathematical problems for the next century
• The diameters of network-flow polytopes satisfy the Hirsch conjecture
• The HOL Light theory of Euclidean space
• Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL
• A Modular Formalisation of Finite Group Theory
• Central Path Curvature and Iteration-Complexity for Redundant Klee—Minty Cubes
• Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
• Log-Barrier Interior Point Methods Are Not Strongly Polynomial
• Formalization of Incremental Simplex Algorithm by Stepwise Refinement
• Algebraic and Topological Tools in Linear Optimization
• Canonical Structures for the Working Coq User
• Pragmatic Quotient Types in Coq
• An Improved Tight Closure Algorithm for Integer Octagonal Constraints
• Euler’s Polyhedron Formula in mizar
• A formalization of convex polyhedra based on the simplex method