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