We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Formalizing the Face Lattice of Polyhedra

Abstract: 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$.
Subjects: Logic in Computer Science (cs.LO); Combinatorics (math.CO); Optimization and Control (math.OC)
Cite as: arXiv:2104.15021 [cs.LO]
  (or arXiv:2104.15021v4 [cs.LO] for this version)

Submission history

From: Xavier Allamigeon [view email] [via LOGICAL proxy]
[v1] Fri, 30 Apr 2021 14:19:11 GMT (39kb)
[v2] Thu, 16 Dec 2021 17:13:08 GMT (40kb)
[v3] Tue, 19 Apr 2022 15:25:59 GMT (40kb)
[v4] Tue, 17 May 2022 07:08:02 GMT (49kb,D)

Link back to: arXiv, form interface, contact.