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 .
Type de document :
Communication dans un congrès
June Andronick and Amy Felty. Certified Programs and Proofs, Jan 2018, Los Angeles, California, United States. Certified Programs and Proofs, 2018
Liste complète des métadonnées

Littérature citée [28 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01643919
Contributeur : Boris Djalal <>
Soumis le : mardi 21 novembre 2017 - 17:30:27
Dernière modification le : vendredi 9 février 2018 - 01:24:44

Fichier

CPP_2018_paper_Boris_Djalal.pd...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01643919, version 1

Collections

Citation

Boris Djalal. A Constructive Formalisation of Semi-algebraic Sets and Functions. June Andronick and Amy Felty. Certified Programs and Proofs, Jan 2018, Los Angeles, California, United States. Certified Programs and Proofs, 2018. 〈hal-01643919〉

Partager

Métriques

Consultations de la notice

302

Téléchargements de fichiers

79