Proving Bounds for Real Linear Programs in Isabelle/HOL

Steven Obua

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Linear programming is a basic mathematical technique for optimizing a linear function on a domain that is constrained by linear inequalities. We restrict ourselves to linear programs on bounded domains that involve only real variables. In the context of theorem proving, this restriction makes it possible for any given linear program to obtain certificates from external linear programming tools that help to prove arbitrarily precise bounds for the given linear program. To this end, an explicit formalization of matrices in Isabelle/HOL is presented, and how the concept of lattice-ordered rings allows for a smooth integration of matrices with the axiomatic type classes of Isabelle. 
 As our work is a contribution to the Flyspeck project, we argue that with the above techniques it is now possible to prove bounds for the linear programs arising in the proof of the Kepler conjecture sufficiently fast.
Original languageEnglish
Title of host publicationTheorem Proving in Higher Order Logics
Subtitle of host publication18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005. Proceedings
EditorsJoe Hurd, Tom Melham
PublisherSpringer Berlin Heidelberg
Number of pages18
ISBN (Electronic)978-3-540-31820-0
ISBN (Print)978-3-540-28372-0
Publication statusPublished - 2005

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


Dive into the research topics of 'Proving Bounds for Real Linear Programs in Isabelle/HOL'. Together they form a unique fingerprint.

Cite this