Алгоритм Тарського — універсальний алгоритм, що дозволяє встановити істинність або хибність будь-якої замкнутої арифметичної формули першого порядку зі змінними для дійсних чисел.
Алгоритм Тарського дозволяє перевірити істинність або хибність будь-якого висловлювання про кінцеву кількість дійсних чисел. Таке висловлювання можна записати на стандартній мові математичної логіки першого порядку. За допомогою введення декартових координат до подібного виду можна навести, наприклад, будь-яку задачу евклідової геометрії — що дозволяє автоматично доводити будь-яку теорему елементарної геометрії.[1][2]
Варто зазначити, що для аналогічної мови зі змінними, які приймають лише раціональні значення, алгоритм, подібний алгоритму Тарського, неможливий.[1]
Історія
Алгоритм був розроблений у 1948 році американським логіком Альфредом Тарським. Існування подібного алгоритму тривалий час вважалося неможливим, тому його створення стало революцією.[3]
Однак на практиці алгоритм виявився малоефективним. У 1974 році було отримано суворий доказ того, що час роботи будь-якого алгоритму для цієї задачі залежить принаймні експоненціально від довжини вихідного твердження.[2]
Примітки
Джерела
