Detalle del congreso

Autores: Xavier Allamigeon; Ricardo D. Katz.

Resumen: We present a formalization of convex polyhedra in the proof assistant Coq. The cornerstone of our work is a complete implementation of the simplex method, together with the proof of its correctness and termination. This allows us to define the basic predicates over polyhedra in an effective way (i.e. as programs), and relate them with the corresponding usual logical counterparts. To this end, we make an extensive use of the Boolean reflection methodology. The benefit of this approach is that we can easily derive the proof of several essential results on polyhedra, such as Farkas Lemma, duality theorem of linear programming, and Minkowski Theorem.

Tipo de reunión: Conferencia.

Tipo de trabajo: Artículo Completo.

Producción: A Formalization of Convex Polyhedra Based on the Simplex Method.

Reunión científica: 8th International Conference on Interactive Theorem Proving.

Lugar: Brasilia.

Institución organizadora: Universidad de Brasilia.

Publicado: Sí

Lugar publicación: Berlín Heidelberg

Mes de reunión: 9

Año: 2017.