TY - GEN
T1 - Formalizing the Face Lattice of Polyhedra
AU - Allamigeon, Xavier
AU - Katz, Ricardo D.
AU - Strub, Pierre Yves
N1 - Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
PY - 2020/1/1
Y1 - 2020/1/1
N2 - 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 sublattices.
AB - 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 sublattices.
UR - https://www.scopus.com/pages/publications/85088267619
U2 - 10.1007/978-3-030-51054-1_11
DO - 10.1007/978-3-030-51054-1_11
M3 - Conference contribution
AN - SCOPUS:85088267619
SN - 9783030510534
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 185
EP - 203
BT - Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Proceedings
A2 - Peltier, Nicolas
A2 - Sofronie-Stokkermans, Viorica
PB - Springer
T2 - 10th International Joint Conference on Automated Reasoning, IJCAR 2020
Y2 - 1 July 2020 through 4 July 2020
ER -