*Originating authors are Reinhard Oldenburg and Michele Artigue*.

How do computer packages do abstract algebraic problems such as proving statements “for all ” or finding whether a Real Number with certain conditions exists?

Recent advances draw on theorems in mathematical logic, as well as improvements in computing.

High school students learn how to solve problems such as the following: « For what values of the real number c, does the polynomial have two distinct real roots ? », and algorithmically get the answer: or . Doing so, they have in some sense, found a way of transforming the sentence expressing the problem and and involving the two existential quantifiers ‘there exists ’ and ‘there exists ’ into the sentence or which no longer includes quantifiers. For what kind of problems is this possible, theoretically but also practically with an effective computer program? In 1938, thanks to a theorem of elimination of quantifiers proved by the logician Alfred Tarski, a decisive step was achieved regarding these questions, but this was not at all the end of the story… READ MORE