Mathematical Structures in Computer Science

Table of Contents - 2007 - Volume 17, Issue 01  

Paper

Implementing the cylindrical algebraic decomposition within the Coq system

ASSIA MAHBOUBIa1

a1 INRIA Sophia Antipolis, 2004, routes des Lucioles – B.P. 93, 06902 Sophia Antipolis Cedex, France Email: assia.mahboubi@sophia.inria.fr

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.

(Received December 01 2005)

(Revised June 29 2006)