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