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 :
Pré-publication, Document de travail
2017
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 : jeudi 11 janvier 2018 - 16:35:50

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. 2017. 〈hal-01643919〉

Partager

Métriques

Consultations de la notice

99

Téléchargements de fichiers

37