coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Loic Pottier <Loic.Pottier AT sophia.inria.fr>
- To: "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>, Michel Hirschowitz <hirschom AT clio.unice.fr>, Marc CHIAVERINI <chiaverm AT clio.unice.fr>, lemme AT sophia.inria.fr
- Subject: Solving inequations on reals.
- Date: Thu, 04 May 2000 10:34:30 +0200
A first version of a tactic, called Fourier, that proves linear
inequations and equations on real numbers, with Fourier's algorithm, is
available at:
http://www-sop.inria.fr/lemme/Loic.Pottier/Coq/Fourier.tar
As it uses only the Ring tactic, it may fail in cases when non-trivial
reductions of fractions are needed.
Comments are wellcome!
--------
Une première version d'une tactique, appelée Fourier, qui prouve des
inéquations et des équations linéaires sur les réels, avec l'algorithme
de Fourier, est disponible à l'adresse:
http://www-sop.inria.fr/lemme/Loic.Pottier/Coq/Fourier.tar
Comme elle n'utilise que la tactique Ring, elle peut échouer quand des
réductions de fractions non triviales sont nécessaires.
Tout commentaire est bienvenu!
Loïc Pottier
- Solving inequations on reals., Loic Pottier
Archive powered by MhonArc 2.6.16.