Artículo
Formalizing the Face Lattice of Polyhedra
Fecha de publicación:
05/2022
Editorial:
Technische Universität Braunschweig
Revista:
Logical Methods in Computer Science
ISSN:
1860-5974
Idioma:
Inglés
Tipo de recurso:
Artículo publicado
Clasificación temática:
Resumen
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.
Archivos asociados
Licencia
Identificadores
Colecciones
Articulos(CIFASIS)
Articulos de CENTRO INT.FRANCO ARG.D/CS D/L/INF.Y SISTEM.
Articulos de CENTRO INT.FRANCO ARG.D/CS D/L/INF.Y SISTEM.
Citación
Allamigeon, Xavier; Katz, Ricardo David; Strub, Pierre Yves; Formalizing the Face Lattice of Polyhedra; Technische Universität Braunschweig; Logical Methods in Computer Science; 18; 2; 5-2022; 1-23
Compartir
Altmétricas