Implementing the cylindrical algebraic decomposition within the Coq system
Implementing the cylindrical algebraic decomposition within the Coq system
复制标题
在 Coq 系统中实现圆柱代数分解
DOI：
10.1017/s096012950600586x
复制
发表时间：
2007
影响因子：
0.5
通讯作者：
A. Mahboubi
中科院分区：
文献类型：
--
作者：
A. Mahboubi
Coq系统是一个基于Curry-Howard的证据助手。因此，它包含了一种全功能、强类型的编程语言，可以用来通过实现反身策略来用强大的自动化工具来增强系统。我们给出了柱面代数分解算法在Coq系统中的实现，它的证明导致了一阶实数理论的证明产生判定过程。
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.