Vass: This repository contains following formalizations: logic/LRA.v: Linear real arithmetic and Fourier-Motzkin elimination; logic/Presburger.v: Presburger arithmetic and quantifier elimination; algebra_ext.v: Quantifier elimination principle for linear inequalities; matrix_ext.v: Farkas’ lemma; cone.v: Elementary theory of convex cones.

References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Allamigeon, Xavier; Katz, Ricardo D.: A formalization of convex polyhedra based on the simplex method (2019)