__NOTOC__ Алгоритм Тарского — универсальный алгоритм, позволяющий установить истинность или ложность любой замкнутой арифметической формулы первого порядка с переменными для вещественных чисел. Основан на теореме Зайденберга — Тарского.
Алгоритм Тарского позволяет проверить истинность или ложность любого высказывания о конечном количестве вещественных чисел. Такое высказывание можно записать на стандартном языке математической логики первого порядка. С помощью введения декартовых координат к подобному виду можно привести, например, любую задачу евклидовой геометрии — что в принципе позволяет автоматически доказывать любую теорему элементарной геометрии. Матиясевич Ю. В. «Алгоритм Тарского» // Компьютерные инструменты в образовании, 2008, Выпуск № 6Theoretical Computer Science: взгляд математика // Компьютерра, № 2 от 22 января 2001 года
Для аналогичного языка с переменными, принимающими только рациональные значения, алгоритм, подобный алгоритму Тарского, невозможен.
История Алгоритм разработан в 1948 году американским логиком Альфредом Тарским. Существование подобного алгоритма длительное время считалось невозможным, поэтому его создание стало своего рода революцией.Алгоритм Тарского // семинар «Введение в Computer Science», доклад Матиясевича (2004)
Время работы первоначального варианта алгоритма нельзя было ограничить никакой башней экспонент от длины формулы. Впоследствии алгоритм был улучшен, Г. Е. Коллинз предложил алгоритм время работы которого ограничено двойной экспонентой. Однако на практике и этот алгоритм малоэффективен. В 1974 году было получено доказательство того, что время работы любого алгоритма для этой задачи зависит по крайней мере экспоненциально от длины исходного утверждения.
См. также Алгоритмическая разрешимость Элиминация кванторов
Примечания
Ссылки Алгоритм Тарского — лекции Ю. В. Матиясевича (видео) Свободная реализация алгоритма
Категория:Математическая логика Категория:Аналитическая геометрия Категория:Алгоритмы