Implementing the cylindrical algebraic decomposition within the Coq system

Assia Mahboubi 1
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : The Coq system is a Curry-Howard based proof assistant. Therefore, it contains a full functional, strongly typed programming language, which can be used to enhance the system with powerful automation tools through the implementation of reflexive tactics. We present the implementation of a cylindrical algebraic decomposition algorithm within the Coq system, whose certification leads to a proof producing decision procedure for the first-order theory of real numbers.
Type de document :
Article dans une revue
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2007, 17 (1), pp.99-127. 〈10.1017/S096012950600586X〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00819489
Contributeur : Assia Mahboubi <>
Soumis le : mercredi 1 mai 2013 - 16:07:17
Dernière modification le : samedi 27 janvier 2018 - 01:32:20

Identifiants

Collections

Citation

Assia Mahboubi. Implementing the cylindrical algebraic decomposition within the Coq system. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2007, 17 (1), pp.99-127. 〈10.1017/S096012950600586X〉. 〈hal-00819489〉

Partager

Métriques

Consultations de la notice

121