Implementing the cylindrical algebraic decomposition within the Coq system

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

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. © 2007 Cambridge University Press.
Original languageEnglish
Title of host publicationMathematical Structures in Computer Science
Pages99-127
DOIs
Publication statusPublished - Feb 2007
Externally publishedYes

Publication series

NameMathematical Structures in Computer Science
ISSN (Print)0960-1295

Fingerprint

Dive into the research topics of 'Implementing the cylindrical algebraic decomposition within the Coq system'. Together they form a unique fingerprint.

Cite this