### Abstract

We use the previous formalization of the general simplex algorithm to formulate an algorithm for solving linear programs. We encode the linear programs using only linear constraints. Solving these constraints also solves the original linear program. This algorithm is proven to be sound by applying the weak duality theorem which is also part of this formalization.

### License

BSD License

### Topics

- Mathematics/Algebra

### Session Linear_Programming

- More_Jordan_Normal_Forms
- Matrix_LinPoly
- LP_Preliminaries
- Linear_Programming

### Depends on

- Farkas' Lemma and Motzkin’s Transposition Theorem
- Matrices, Jordan Normal Forms, and Spectral Radius Theory
- Linear Inequalities

## Cite

×

Linear_Programming-AFP

    @article{Linear_Programming-AFP,
      author  = {Julian Parsert and Cezary Kaliszyk},
      title   = {Linear Programming},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Linear_Programming.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Sep 23, 2019 : Isabelle2019