×

zbMATH — the first resource for mathematics

Algorithmes d’élimination des quantificateurs. (French) Zbl 0594.03016
Summary: Le principe de l’élimination des quantificateurs sur les corps réels clos est un résultat classique (Tarski 1948) de la théorie des modèles. Le développement récent de la géométrie semi- algébrique et du calcul formel ont remis cette question d’actualité. Je m’attacherai dans cet exposé à la comparaison entre trois algorithmes d’élimination issus des travaux de A. Seidenberg [Ann. Math., II. Ser. 60, 365-374 (1954; Zbl 0056.018)], L. Hörmander [The analysis of linear partial differential operators. Vol. II (1983; Zbl 0521.35002)] et G. E. Collins [Computer Algebra, Symbolic and Algebraic Computation, Comput. Suppl. 4, 79-81 (1982; Zbl 0495.03016)].

MSC:
03C10 Quantifier elimination, model completeness and related topics
68W30 Symbolic computation and algebraic computation
PDF BibTeX XML Cite