Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] new in the AFP: Linear Inequalities


view this post on Zulip Email Gateway (Aug 22 2022 at 20:04):

From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Linear Inequalities
by Ralph Bottesch, Alban Reynaud and René Thiemann

We formalize results about linear inqualities, mainly from Schrijver's book. The main results are the proof of the fundamental theorem on linear inequalities, Farkas' lemma, Carathéodory's theorem, the Farkas-Minkowsky-Weyl theorem, the decomposition theorem of polyhedra, and Meyer's result that the integer hull of a polyhedron is a polyhedron itself. Several theorems include bounds on the appearing numbers, and in particular we provide an a-priori bound on mixed-integer solutions of linear inequalities.

[https://www.isa-afp.org/entries/Linear_Inequalities.html]

Enjoy!
Gerwin


Last updated: Mar 28 2024 at 12:29 UTC