Алгоритм Тарского позволяет установить истинность или ложность любого утвержения про конечное количество вещественных чисел. Вместе с методом координат Декарта это позволяет автоматически доказывать широкий класс теорем элементарной геометрии. Изложенный здесь вариант алгоритма предназначен для первоначального знакомства с этой областью - его нетрудно понять, несложно запрограммировать, но полученная программа будет крайне неэффективной.

Tarski's 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.