Email Gateway (Aug 19 2022 at 16:14): Email Gateway (Aug 19 2022 at 16:14):From: Gergely Buday <gbuday@gmail.com>
Hi,
I did a search on afp but I have not found any formalisation of linear
programming.
Do you know of any attempt?
Email Gateway (Aug 19 2022 at 16:14):From: Peter Lammich <lammich@in.tum.de>
Hi.
Filip Maric has formalized simplex.
http://argo.matf.bg.ac.rs/downloads/formalizations/Simplex.zip
Email Gateway (Aug 19 2022 at 16:15):From: Tobias Nipkow <nipkow@in.tum.de>
http://link.springer.com/chapter/10.1007%2F11541868_15#page-1
Tobias
Email Gateway (Aug 19 2022 at 16:15):From: Gergely Buday <gbuday@gmail.com>
Well this is behind a paywall.
What I have found is an extended abstract:
http://drops.dagstuhl.de/opus/volltexte/2006/435/pdf/05021.ObuaSteven.ExtAbstract.435.pdf
and the code in src/HOL/Matrix_LP, I guess that is the implementation.
Last updated: Nov 21 2024 at 12:39 UTC