A formalization of convex polyhedra based on the simplex method

DOI10.1007/978-3-319-66107-0_3zbMath1468.68315arXiv1706.10269OpenAlexW2886753998WikidataQ129411142 ScholiaQ129411142MaRDI QIDQ5915783

Ricardo D. Katz, Xavier Allamigeon

Publication date: 4 January 2018

Published in: Journal of Automated Reasoning, Interactive Theorem Proving (Search for Journal in Brave)

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

zbMATH Keywords

linear programmingsimplex methodconvex polyhedraformalization of mathematics

Mathematics Subject Classification ID

Special polytopes (linear programming, centrally symmetric, etc.) (52B12) Linear programming (90C05) Extreme-point and pivoting methods (90C49) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (3)

Formalizing the Face Lattice of Polyhedra ⋮ Formalization of the Domination Chain with Weighted Parameters (Short Paper) ⋮ Unnamed Item

Uses Software

• Coq
• z3
• HOL Light
• GitHub
• Vass

Cites Work

• Unnamed Item
• Unnamed Item
• A counterexample to the Hirsch conjecture
• A pivoting algorithm for convex hulls and vertex enumeration of arrangements and polyhedra
• Mathematical problems for the next century
• The HOL Light theory of Euclidean space
• Polytope Lyapunov functions for stable and for stabilizable LSS
• The generalized simplex method for minimizing a linear form under linear inequality restraints
• Linear Programs and Convex Hulls Over Fields of Puiseux Fractions
• Refinements for Free!
• Point-Free, Set-Free Concrete Linear Algebra
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
• Polynomial algorithms in linear programming
• Formalization of Incremental Simplex Algorithm by Stepwise Refinement
• The width of five-dimensional prismatoids
• More bounds on the diameters of convex polytopes
• Theorem Proving in Higher Order Logics
• Fast LCF-Style Proof Reconstruction for Z3

This page was built for publication: A formalization of convex polyhedra based on the simplex method