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

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

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

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

История

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

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

См. также

• Алгоритмическая разрешимость
• Элиминация кванторов

Ссылки

• Алгоритм Тарского — лекции Ю. В. Матиясевича (видео)
• Свободная реализация алгоритма