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.
Document type :
Journal articles
Complete list of metadatas

https://hal.inria.fr/hal-00819489
Contributor : Assia Mahboubi <>
Submitted on : Wednesday, May 1, 2013 - 4:07:17 PM
Last modification on : Saturday, January 27, 2018 - 1:32:20 AM

Identifiers

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⟩

Share

Metrics

Record views

185