Formalizing the Face Lattice of Polyhedra
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, in...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2022-05-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/7436/pdf |
| _version_ | 1797268509482287104 |
|---|---|
| author | Xavier Allamigeon Ricardo D. Katz Pierre-Yves Strub |
| author_facet | Xavier Allamigeon Ricardo D. Katz Pierre-Yves Strub |
| author_sort | Xavier Allamigeon |
| collection | DOAJ |
| description | 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$. |
| first_indexed | 2024-04-25T01:33:37Z |
| format | Article |
| id | doaj.art-9efc2b3e111647cfb13ae78165495090 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:33:37Z |
| publishDate | 2022-05-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-9efc2b3e111647cfb13ae781654950902024-03-08T10:38:41ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742022-05-01Volume 18, Issue 210.46298/lmcs-18(2:10)20227436Formalizing the Face Lattice of PolyhedraXavier AllamigeonRicardo D. KatzPierre-Yves StrubFaces 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$.https://lmcs.episciences.org/7436/pdfcomputer science - logic in computer sciencemathematics - combinatoricsmathematics - optimization and control |
| spellingShingle | Xavier Allamigeon Ricardo D. Katz Pierre-Yves Strub Formalizing the Face Lattice of Polyhedra Logical Methods in Computer Science computer science - logic in computer science mathematics - combinatorics mathematics - optimization and control |
| title | Formalizing the Face Lattice of Polyhedra |
| title_full | Formalizing the Face Lattice of Polyhedra |
| title_fullStr | Formalizing the Face Lattice of Polyhedra |
| title_full_unstemmed | Formalizing the Face Lattice of Polyhedra |
| title_short | Formalizing the Face Lattice of Polyhedra |
| title_sort | formalizing the face lattice of polyhedra |
| topic | computer science - logic in computer science mathematics - combinatorics mathematics - optimization and control |
| url | https://lmcs.episciences.org/7436/pdf |
| work_keys_str_mv | AT xavierallamigeon formalizingthefacelatticeofpolyhedra AT ricardodkatz formalizingthefacelatticeofpolyhedra AT pierreyvesstrub formalizingthefacelatticeofpolyhedra |