Formalizing the Face Lattice of Polyhedra

DOI10.1007/978-3-030-51054-1_11OpenAlexW4285751001MaRDI QIDQ5049001

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

Publication date: 9 November 2022

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

Full work available at URL: https://doi.org/10.1007/978-3-030-51054-1_11

Mathematics Subject Classification ID

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

Uses Software

• Apron
• polymake
• SageMath
• PPL
• GitHub
• Vass

Cites Work

• Unnamed Item
• Unnamed Item
• A counterexample to the Hirsch conjecture
• 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
• Refinements for Free!
• Central Path Curvature and Iteration-Complexity for Redundant Klee—Minty Cubes
• Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
• Lectures on Polytopes
• 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
• A Machine-Checked Proof of the Odd Order Theorem
• Pragmatic Quotient Types in Coq
• Euler’s Polyhedron Formula in mizar
• On sub-determinants and the diameter of polyhedra
• A formalization of convex polyhedra based on the simplex method

This page was built for publication: Formalizing the Face Lattice of Polyhedra