Алгоритм Тарского

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

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

Следует отметить, что для аналогичного языка с переменными, принимающими только рациональные значения, алгоритм, подобный А.Т., невозможен.

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

Однако на практике алгоритм оказался мало эффективен. В 1974 году было получено строгое доказательство того, что время работы любого алгоритма для этой задачи зависит по крайней мере экспоненциально от длины исходного утверждения.