Linear Programming in Isabelle/HOL
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917624882921472 |
|---|---|
| author | Parsert, Julian |
| author_facet | Parsert, Julian |
| contents | Linear programming describes the problem of optimising a linear objective function over a set of constraints on its variables. In this paper we present a solver for linear programs implemented in the proof assistant Isabelle/HOL. This allows formally proving its soundness, termination, and other properties. We base these results on a previous formalisation of the simplex algorithm which does not take optimisation problems into account. Using the weak duality theorem of linear programming we obtain an algorithm for solving linear programs. Using Isabelle's code generation mechanism we can generate an external solver for linear programs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_19639 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Linear Programming in Isabelle/HOL Parsert, Julian Logic in Computer Science Linear programming describes the problem of optimising a linear objective function over a set of constraints on its variables. In this paper we present a solver for linear programs implemented in the proof assistant Isabelle/HOL. This allows formally proving its soundness, termination, and other properties. We base these results on a previous formalisation of the simplex algorithm which does not take optimisation problems into account. Using the weak duality theorem of linear programming we obtain an algorithm for solving linear programs. Using Isabelle's code generation mechanism we can generate an external solver for linear programs. |
| title | Linear Programming in Isabelle/HOL |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2403.19639 |