Search Results

Documents authored by Obua, Steven


Document
Proving Bounds for Real Linear Programs in Isabelle/HOL

Authors: Steven Obua

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)


Abstract
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 demonstrate that via reflection and 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.

Cite as

Steven Obua. Proving Bounds for Real Linear Programs in Isabelle/HOL. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{obua:DagSemProc.05021.18,
  author =	{Obua, Steven},
  title =	{{Proving Bounds for Real Linear Programs in Isabelle/HOL}},
  booktitle =	{Mathematics, Algorithms, Proofs},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5021},
  editor =	{Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.18},
  URN =		{urn:nbn:de:0030-drops-4351},
  doi =		{10.4230/DagSemProc.05021.18},
  annote =	{Keywords: Certified proofs, Kepler conjecture}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail