Farkas' Lemma and Motzkin's Transposition Theorem (Q7361804)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Farkas
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Farkas' Lemma and Motzkin's Transposition Theorem |
AFP entry Farkas |
Statements
17 January 2019
0 references
Ralph Bottesch
0 references
Max W. Haslbeck
0 references
René Thiemann
0 references
Farkas' Lemma and Motzkin's Transposition Theorem (English)
0 references
We formalize a proof of Motzkin's transposition theorem and Farkas' lemma in Isabelle/HOL. Our proof is based on the formalization of the simplex algorithm which, given a set of linear constraints, either returns a satisfying assignment to the problem or detects unsatisfiability. By reusing facts about the simplex algorithm we show that a set of linear constraints is unsatisfiable if and only if there is a linear combination of the constraints which evaluates to a trivially unsatisfiable inequality.
0 references
