Linear Programming

Title:	Linear Programming
Authors:	Julian Parsert and Cezary Kaliszyk
Submission date:	2019-08-06
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.
BibTeX:	@article{Linear_Programming-AFP, author = {Julian Parsert and Cezary Kaliszyk}, title = {Linear Programming}, journal = {Archive of Formal Proofs}, month = aug, year = 2019, note = {\url{http://isa-afp.org/entries/Linear_Programming.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Farkas, Jordan_Normal_Form, Linear_Inequalities
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.