Skip to Main content Skip to Navigation
Conference papers

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 .
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download
Contributor : Boris Djalal Connect in order to contact the contributor
Submitted on : Tuesday, November 21, 2017 - 5:30:27 PM
Last modification on : Thursday, January 20, 2022 - 5:30:47 PM


Files produced by the author(s)


  • HAL Id : hal-01643919, version 1



Boris Djalal. A Constructive Formalisation of Semi-algebraic Sets and Functions. CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, California, United States. pp.240-251. ⟨hal-01643919⟩



Les métriques sont temporairement indisponibles