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

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

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

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

История

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

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

См. также

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

Примечания

1. ↑ ^{1 2} Матиясевич Ю. В. «Алгоритм Тарского» // Компьютерные инструменты в образовании, 2008, Выпуск № 6
2. ↑ ^{1 2} Theoretical Computer Science: взгляд математика // Компьютерра, № 2 от 22 января 2001 года
3. ↑ Алгоритм Тарского // семинар «Введение в Computer Science», доклад Матиясевича (2004)

Ссылки

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

Для улучшения этой статьи желательно?: Дополнить статью (статья слишком короткая либо содержит лишь словарное определение). Проставить интервики в рамках проекта Интервики.