nach oben

Journal of Automated Reasoning

Erschienen in:

04.08.2018

A Formalization of Convex Polyhedra Based on the Simplex Method

verfasst von: Xavier Allamigeon, Ricardo D. Katz

Erschienen in: Journal of Automated Reasoning | Ausgabe 2/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We present a formalization of convex polyhedra in the proof assistant Coq. The cornerstone of our work is a complete implementation of the simplex method, together with the proof of its correctness and termination. This allows us to define the basic predicates over polyhedra in an effective way (i.e. as programs), and relate them with the corresponding usual logical counterparts. To this end, we make an extensive use of the Boolean reflection methodology.The benefit of this approach is that we can easily derive the proof of several fundamental results on polyhedra, such as Farkas’ Lemma, the duality theorem of linear programming, and Minkowski’s Theorem.

Vorheriger Artikel Selected Extended Papers of ITP 2017

Nächster Artikel A Formal Proof of the Expressiveness of Deep Learning

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

It can be downloaded by executing

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9477-1/MediaObjects/10817_2018_9477_Figb_HTML.gif

. Instructions for building can be found in the README.md file.

The double index in

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9477-1/MediaObjects/10817_2018_9477_Figad_HTML.gif

and

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9477-1/MediaObjects/10817_2018_9477_Figae_HTML.gif

comes from the fact that column vectors are encoded as matrices (with one column).

When such a d exists, the value of the objective function of \(\mathrm {DualLP}(A,b,0)\) can be made arbitrarily large by considering points of the form \(\alpha d\), for \(\alpha \ge 0\), which obviously belong to \(\mathcal {Q}(A,0)\) (due to the latter property, d is called a dual feasible direction, see Sect. 5.2).

The command

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9477-1/MediaObjects/10817_2018_9477_Figfe_HTML.gif

is synonymous to the command

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9477-1/MediaObjects/10817_2018_9477_Figff_HTML.gif

that is used for local declarations when

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9477-1/MediaObjects/10817_2018_9477_Figfg_HTML.gif

is an identifier and

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9477-1/MediaObjects/10817_2018_9477_Figfh_HTML.gif

is a proposition. This means that h is a proof term of

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9477-1/MediaObjects/10817_2018_9477_Figfi_HTML.gif

. The hypothesis is then added to list of hypotheses (or, equivalently, of variables) of the subsequent statements.

We make a slight abuse of language, since feasibility usually applies to linear programs, or systems of contraints. By extension, we apply it to polyhedra: \(\mathcal {P}(A,b)\) is feasible if it is nonempty.

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9477-1/MediaObjects/10817_2018_9477_Figls_HTML.gif

and

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9477-1/MediaObjects/10817_2018_9477_Figlt_HTML.gif

, the statement

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9477-1/MediaObjects/10817_2018_9477_Figlu_HTML.gif

means that either

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9477-1/MediaObjects/10817_2018_9477_Figlv_HTML.gif

and P, or

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9477-1/MediaObjects/10817_2018_9477_Figlw_HTML.gif

and

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9477-1/MediaObjects/10817_2018_9477_Figlx_HTML.gif

hold. We refer to [14] for an introduction on the way Boolean reflection is used in MathComp.

Armand, M., Faure, G., Grégoire, B., Keller, C., Théry, L., Werner, B.: A modular integration of sat/smt solvers to coq through proof witnesses. In: Jouannaud, J.P., Shao, Z. (eds.) Certified Programs and Proofs, pp. 135–150. Springer Berlin Heidelberg, Berlin (2011)CrossRef

Avis, D.: A revised implementation of the reverse search vertex enumeration algorithm. In: Kalai, G., Ziegler, G.M. (eds.) Polytopes—Combinatorics and Computation. Birkhäuser, Basel (2002). https://doi.org/10.1007/978-3-0348-8438-9_9

Avis, D., Fukuda, K.: A pivoting algorithm for convex hulls and vertex enumeration of arrangements and polyhedra. Discrete Comput. Geom. 8(3), 295–313 (1992). https://doi.org/10.1007/BF02293050 MathSciNetCrossRefMATH

Barthe, G., Forest, J., Pichardie, D., Rusu, V.: Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In: Hagiya, M., Wadler, P. (eds.) Proceedings of FLOPS 2006. Springer Berlin Heidelberg, Berlin (2006). https://doi.org/10.1007/11737414_9

Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) Proceedings of TYPES 2006. Springer, Berlin (2007). https://doi.org/10.1007/978-3-540-74464-1_4

Böhme, S., Weber, T.: Fast lcf-style proof reconstruction for z3. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving, pp. 179–194. Springer Berlin Heidelberg, Berlin (2010)CrossRef

Bremner, D., Deza, A., Hua, W., Schewe, L.: More bounds on the diameters of convex polytopes. Optim. Methods Softw. 28(3), 442–450 (2013). https://doi.org/10.1080/10556788.2012.668906 MathSciNetCrossRefMATH

Cohen, C., Dénès, M., Mörtberg, A.: Refinements for free!. In: Gonthier, G., Norrish, M. (eds.) Proceedings of CPP 2013. Springer, pp. 84–96. Berlin (2013). https://doi.org/10.1007/978-3-319-03545-1_10

Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of POPL 1978, pp. 84–96. ACM Press, Tucson (1978)

10.

Dantzig, G.B.: Maximization of a linear function of variables subject to linear inequalities. In: Activity Analysis of Production and Allocation. Wiley, New York (1951)

11.

Dantzig, G.B., Orden, A., Wolfe, P.: The generalized simplex method for minimizing a linear form under linear inequality restraints. Pac. J. Math. 5(2), 183–195 (1955)MathSciNetCrossRefMATH

12.

Fouilhe, A., Boulmé, S.: A certifying frontend for (sub) polyhedral abstract domains. In: Giannakopoulou, D., Kroening, D. (eds.) Proceedings of VSTTE 2014. Springer, Berlin (2014). https://doi.org/10.1007/978-3-319-12154-3_13

13.

Gonthier, G.: Point-free, set-free concrete linear algebra. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) Proceedings of ITP 2011. Springer, Berlin (2011). https://doi.org/10.1007/978-3-642-22863-6_10

14.

Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Research Report RR-6455, Inria Saclay Ile de France (2016)

15.

Guglielmi, N., Laglia, L., Protasov, V.: Polytope Lyapunov functions for stable and for stabilizable LSS. Found. Comput. Math. 17(2), 567–623 (2017). https://doi.org/10.1007/s10208-015-9301-9 MathSciNetCrossRefMATH

16.

Harrison, J.: The HOL light theory of Euclidean space. J. Autom. Reason. 50, 173–190 (2013)MathSciNetCrossRefMATH

17.

Joswig, M., Loho, G., Lorenz, B., Schröter, B.: Linear programs and convex hulls over fields of puiseux fractions. In: Kotsireas, I.S., Rump, S.M., Yap, C.K. (eds.) Mathematical Aspects of Computer and Information Sciences, pp. 429–445. Springer, Cham (2016)CrossRef

18.

Khachiyan, L.: Polynomial algorithms in linear programming. USSR Comput. Math. Math. Phys. 20(1), 53–72 (1980). https://doi.org/10.1016/0041-5553(80)90061-0 MathSciNetCrossRefMATH

19.

Matschke, B., Santos, F., Weibel, C.: The width of five-dimensional prismatoids. Proc. Lond. Math. Soc. 110(3), 647–672 (2015). https://doi.org/10.1112/plms/pdu064 MathSciNetCrossRefMATH

20.

Obua, S.: Proving bounds for real linear programs in isabelle/hol. In: Hurd, J., Melham, T. (eds.) Theorem Proving in Higher Order Logics, pp. 227–244. Springer Berlin Heidelberg, Berlin (2005)CrossRef

21.

Sakaguchi, K.: Vass. https://github.com/pi8027/vass (2016). Accessed 2 Aug 2018

22.

Santos, F.: A counterexample to the Hirsch conjecture. Ann. Math. 176(1), 383–412 (2012). https://doi.org/10.4007/annals.2012.176.1.7 MathSciNetCrossRefMATH

23.

Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1986)MATH

24.

Smale, S.: Mathematical problems for the next century. Math. Intell. 20, 7–15 (1998)MathSciNetCrossRefMATH

25.

Spasić, M., Marić, F.: Formalization of incremental simplex algorithm by stepwise refinement. In: Giannakopoulou, D., Méry, D. (eds.) Proceedings of FM 2012. Springer, Berlin (2012). https://doi.org/10.1007/978-3-642-32759-9_35

Titel: A Formalization of Convex Polyhedra Based on the Simplex Method
verfasst von: Xavier Allamigeon
Ricardo D. Katz
Publikationsdatum: 04.08.2018
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 2/2019
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-018-9477-1

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 2/2019

Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology

CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics

Selected Extended Papers of ITP 2017

Guarded Cubical Type Theory

Canonicity for Cubical Type Theory

Preface: Special Issue on Homotopy Type Theory and Univalent Foundations

Premium Partner