__NOTOC__ Алгоритм Тарського — універсальний алгоритм, що дозволяє встановити істинність або хибність будь-якої замкнутої арифметичної формули першого порядку зі змінними для дійсних чисел.
Алгоритм Тарського дозволяє перевірити істинність або хибність будь-якого висловлювання про кінцеву кількість дійсних чисел. Таке висловлювання можна записати на стандартній мові математичної логіки першого порядку. За допомогою введення декартових координат до подібного виду можна навести, наприклад, будь-яку задачу евклідової геометрії — що дозволяє автоматично доводити будь-яку теорему елементарної геометрії. Матиясевич Ю. В. «Алгоритм Тарского» // Компьютерные инструменты в образовании, 2008, Выпуск № 6Theoretical Computer Science: взгляд математика // Компьютерра, № 2 от 22 января 2001 года
Варто зазначити, що для аналогічної мови зі змінними, які приймають лише раціональні значення, алгоритм, подібний алгоритму Тарського, неможливий.
Історія Алгоритм був розроблений у 1948 році американським логіком Альфредом Тарським. Існування подібного алгоритму тривалий час вважалося неможливим, тому його створення стало революцією.Алгоритм Тарского // семинар «Введение в Computer Science», доклад Матиясевича (2004)
Однак на практиці алгоритм виявився малоефективним. У 1974 році було отримано суворий доказ того, що час роботи будь-якого алгоритму для цієї задачі залежить принаймні експоненціально від довжини вихідного твердження.
Примітки
Джерела
Алгоритм Тарського — лекції Ю. В. Матіясевича (відео) Вільна реалізація алгоритму