A Constructive Formalisation of Semi-algebraic Sets and Functions

Boris Djalal 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Semi-algebraic sets and semi-algebraic functions are essential to specify and certify cylindrical algebraic decomposition algorithms. We formally define in Coq the base operations on semi-algebraic sets and functions using embedded first-order formulae over the language of real closed fields, and we prove the correctness of their geometrical interpretation. In doing so, we exploit a previous formalisation of quantifier elimination on such embedded formulae to guarantee the decidability of several first-order properties and keep our development constructive. We also exploit it to formalise formulae substitution without having to handle bound variables .
Liste complète des métadonnées

Cited literature [25 references]  Display  Hide  Download

https://hal.inria.fr/hal-01643919
Contributor : Boris Djalal <>
Submitted on : Tuesday, November 21, 2017 - 5:30:27 PM
Last modification on : Friday, April 27, 2018 - 2:30:01 PM

File

CPP_2018_paper_Boris_Djalal.pd...
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01643919, version 1

Collections

Citation

Boris Djalal. A Constructive Formalisation of Semi-algebraic Sets and Functions. Certified Programs and Proofs, Jan 2018, Los Angeles, California, United States. ⟨hal-01643919⟩

Share

Metrics

Record views

620

Files downloads

190