Tarski's algorithm

Abstract

Tarskis algorithm allows to determine whether a given statement about a finite set of real numbers is true of false. Together with the Cartesian coordinate system, it allows to prove automatically a large class of theorems of elementary geometry. The version of the algorithm presented here is suitable for introduction to the subject - it is not difficult to understand the algorithm, it is easy to write a program, but it would be extremely inefficient.