Implementing the cylindrical algebraic decomposition within the Coq system
- 1 February 2007
- journal article
- research article
- Published by Cambridge University Press (CUP) in Mathematical Structures in Computer Science
- Vol. 17 (1), 99-127
- https://doi.org/10.1017/s096012950600586x
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.Keywords
This publication has 16 references indexed in Scilit:
- Proving Formally the Implementation of an Efficient gcd Algorithm for PolynomialsLecture Notes in Computer Science, 2006
- QEPCAD BACM SIGSAM Bulletin, 2004
- Interactive Theorem Proving and Program DevelopmentTexts in Theoretical Computer Science An EATCS Series, 2004
- QEPCAD BACM SIGSAM Bulletin, 2003
- Setoids in type theoryJournal of Functional Programming, 2003
- Subresultants revisitedTheoretical Computer Science, 2003
- The Analysis of Linear Partial Differential Operators IPublished by Springer Science and Business Media LLC ,2003
- REDLOGACM SIGSAM Bulletin, 1997
- Partial Cylindrical Algebraic Decomposition for quantifier eliminationJournal of Symbolic Computation, 1991
- Quantifier elimination for real closed fields by cylindrical algebraic decompostionPublished by Springer Science and Business Media LLC ,1975