|Universiteit Faculteit FNWI English version||3 maart 2005, e-mail|
Woensdag 23 maart 2005
AbstractIt is known since the works of Tarski (1948) that one can decide whether a system of multivariate polynomials has a real solution or not. Modern methods for implementing this algorithm are based on the Cylindrical Algebraic Decomposition (CAD), introduced by Collins (1966). Anyway the complexity of the problem is large and the algorithms involve a wide range of computer algebra tools.
We present an implementation of this algorithm in the Coq system, a proof assistant equipped with a reduction system, which allows the user to program and compute whithin the system. This work intends to use the proof assistant as a single environment for doing computer algebra, while getting a proof of correctness of the computation.
We will present the algorithm and the design of such a tool for a proof assistant.