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

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

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

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

Історія

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

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

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

Посилання
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.