A Constructive Formalisation of Semi-algebraic Sets and Functions - Archive ouverte HAL Access content directly
Conference Papers Year : 2018

A Constructive Formalisation of Semi-algebraic Sets and Functions

(1)
1
Boris Djalal

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 .
Fichier principal
Vignette du fichier
CPP_2018_paper_Boris_Djalal.pdf (680.41 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01643919 , version 1 (21-11-2017)

Identifiers

  • HAL Id : hal-01643919 , version 1

Cite

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⟩
431 View
334 Download

Share

Gmail Facebook Twitter LinkedIn More