Skip to Main content Skip to Navigation
New interface
Journal articles

Implementing the cylindrical algebraic decomposition within the Coq system

Assia Mahboubi 1 
1 MARELLE - Mathematical, Reasoning and Software
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.
Document type :
Journal articles
Complete list of metadata
Contributor : Assia Mahboubi Connect in order to contact the contributor
Submitted on : Wednesday, May 1, 2013 - 4:07:17 PM
Last modification on : Saturday, June 25, 2022 - 11:10:00 PM




Assia Mahboubi. Implementing the cylindrical algebraic decomposition within the Coq system. Mathematical Structures in Computer Science, 2007, 17 (1), pp.99-127. ⟨10.1017/S096012950600586X⟩. ⟨hal-00819489⟩



Record views