It is nowadays widely known and commonly accepted that computers can prove A=B for a lot of different types of A and B. Algorithms for proving identities have been discovered, refined, implemented and applied with increasing impact during the past two decades. But what about inequalities? Can we also have A less B proved by the computer? As a matter of fact, algorithms for proving (polynomial) inequalities are known since much longer than algorithms for proving (special function) identities, but they have long been considered of theoretical interest only and are therefore still not as widely known as they deserve. We want to make some advertisement for a particularly versatile algorithm for solving problems related to inequalities: George Collins's Cylindrical Algebraic Decomposition algorithm (CAD). In the first lesson, we will explain what the algorithm computes, and see how it is applied in standard situations. The second lesson is devoted to the internals of the algorithm. Knowing how the algorithm works may help in applying it more efficiently. Finally, in the third lesson, we will discuss nonstandard applications of the algorithm. In particular, we will show how certain inequalities about non-polynomial quantities can be proven with CAD by constructing suitable sufficient conditions whose truth can be checked with CAD.
Sprache der Kurzfassung:
Englisch
Vortragstyp:
Hauptvortrag / Eingeladener Vortrag auf einer Tagung
Forschungs-