Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] linear programming


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 08:18 UTC