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

Алгоритм Тарского — универсальный

формулы первого порядка с переменными для вещественных чисел

. Основан на теореме Зайденберга — Тарского.

Алгоритм Тарского позволяет проверить истинность или ложность любого

автоматически доказывать любую теорему элементарной геометрии.^[1]^[2]

Для аналогичного языка с переменными, принимающими только

невозможен^[1]

.

История

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

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

См. также

Примечания

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

Ссылки

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

[instr08-1] ¹ ² Матиясевич Ю. В. «Алгоритм Тарского» // Компьютерные инструменты в образовании, 2008, Выпуск № 6

[kt-2] ¹ ² Theoretical Computer Science: взгляд математика // Компьютерра, № 2 от 22 января 2001 года

[3] Алгоритм Тарского Архивная копия от 29 марта 2017 на Wayback Machine // семинар «Введение в Computer Science», доклад Матиясевича (2004)

[1]

[2]

[3]