Formalizing the Face Lattice of Polyhedra
In: EISSN: 1860-5974 ; Logical Methods in Computer Science ; https://inria.hal.science/hal-03915661 ; Logical Methods in Computer Science, 2022, 2022
academicJournal
Zugriff:
International audience ; Faces play a central role in the combinatorial and computational aspects of polyhedra. In this paper, we present the first formalization of faces of polyhedra in the proof assistant Coq. This builds on the formalization of a library providing the basic constructions and operations over polyhedra, including projections, convex hulls and images under linear maps. Moreover, we design a special mechanism which automatically introduces an appropriate representation of a polyhedron or a face, depending on the context of the proof. We demonstrate the usability of this approach by establishing some of the most important combinatorial properties of faces, namely that they constitute a family of graded atomistic and coatomistic lattices closed under interval sublattices. We also prove a theorem due to Balinski on the $d$-connectedness of the adjacency graph of polytopes of dimension $d$.
Titel: |
Formalizing the Face Lattice of Polyhedra
|
---|---|
Autor/in / Beteiligte Person: | Allamigeon, Xavier ; Katz, Ricardo ; Strub, Pierre-Yves ; (TROPICAL), TROPICAL ; Centre de Mathématiques Appliquées - Ecole Polytechnique (CMAP) ; École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) ; Centro Franco Argentino de Ciencias de la Información y de Sistemas Rosario (CIFASIS) ; Consejo Nacional de Investigaciones Científicas y Técnicas Buenos Aires (CONICET)-Universidad Nacional de Rosario Santa Fe ; Laboratoire d'informatique de l'École polytechnique Palaiseau (LIX) ; École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS) ; ANR-18-CE25-0014,scrypt,Compilation sécurisée de primitives cryptographiques(2018) ; ANR-17-CE40-0018,CAPPS,Analyse Combinatoire de Polytopes et de Subdivisions Polyédrales(2017) ; ANR-11-LABX-0056,LMH,LabEx Mathématique Hadamard(2011) |
Link: | |
Zeitschrift: | EISSN: 1860-5974 ; Logical Methods in Computer Science ; https://inria.hal.science/hal-03915661 ; Logical Methods in Computer Science, 2022, 2022 |
Veröffentlichung: | HAL CCSD ; Logical Methods in Computer Science Association, 2022 |
Medientyp: | academicJournal |
DOI: | 10.46298/lmcs-18(2:10)2022 |
Schlagwort: |
|
Sonstiges: |
|