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

Алгоритм Тарського — універсальний алгоритм, що дозволяє встановити істинність або хибність будь-якої замкнутої арифметичної формули першого порядку зі змінними для дійсних чисел.

Алгоритм Тарського дозволяє перевірити істинність або хибність будь-якого висловлювання про кінцеву кількість дійсних чисел. Таке висловлювання можна записати на стандартній мові математичної логіки першого порядку. За допомогою введення декартових координат до подібного виду можна навести, наприклад, будь-яку задачу евклідової геометрії — що дозволяє автоматично доводити будь-яку теорему елементарної геометрії.

Варто зазначити, що для аналогічної мови зі змінними, які приймають лише раціональні значення, алгоритм, подібний алгоритму Тарського, неможливий.

Історія

Алгоритм був розроблений у 1948 році американським логіком Альфредом Тарським. Існування подібного алгоритму тривалий час вважалося неможливим, тому його створення стало революцією.

Однак на практиці алгоритм виявився малоефективним. У 1974 році було отримано суворий доказ того, що час роботи будь-якого алгоритму для цієї задачі залежить принаймні від довжини вихідного твердження.

Примітки

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

Джерела

• Теория рекурсивных функций и эффективная вычислимость. — М. : Мир, 1972. — 416 с.(рос.)
• Алгоритм Тарського [ 8 травня 2013 у Wayback Machine.] — лекції Ю. В. Матіясевича (відео)
• Вільна реалізація алгоритму [ 25 квітня 2016 у Wayback Machine.]