TY - GEN
T1 - Implementing the cylindrical algebraic decomposition within the Coq system
AU - Mahboubi, Assia
PY - 2007/2
Y1 - 2007/2
N2 - 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. © 2007 Cambridge University Press.
AB - 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. © 2007 Cambridge University Press.
UR - http://www.scopus.com/inward/record.url?scp=33847738667&partnerID=8YFLogxK
U2 - 10.1017/S096012950600586X
DO - 10.1017/S096012950600586X
M3 - Conference contribution
T3 - Mathematical Structures in Computer Science
SP - 99
EP - 127
BT - Mathematical Structures in Computer Science
ER -