Алгоритм Тарського
Алгоритм Тарського — універсальний алгоритм, що дозволяє встановити істинність або хибність будь-якої замкнутої арифметичної формули першого порядку зі змінними для дійсних чисел.
Алгоритм Тарського дозволяє перевірити істинність або хибність будь-якого висловлювання про кінцеву кількість дійсних чисел. Таке висловлювання можна записати на стандартній мові математичної логіки першого порядку. За допомогою введення декартових координат до подібного виду можна навести, наприклад, будь-яку задачу евклідової геометрії — що дозволяє автоматично доводити будь-яку теорему елементарної геометрії.[1][2]
Варто зазначити, що для аналогічної мови зі змінними, які приймають лише раціональні значення, алгоритм, подібний алгоритму Тарського, неможливий.[1]
Історія[ред. | ред. код]
Алгоритм був розроблений у 1948 році американським логіком Альфредом Тарським. Існування подібного алгоритму тривалий час вважалося неможливим, тому його створення стало революцією.[3]
Однак на практиці алгоритм виявився малоефективним. У 1974 році було отримано суворий доказ того, що час роботи будь-якого алгоритму для цієї задачі залежить принаймні експоненціально від довжини вихідного твердження.[2]
Примітки[ред. | ред. код]
- ↑ а б Матиясевич Ю. В. «Алгоритм Тарского» // Компьютерные инструменты в образовании, 2008, Выпуск № 6
- ↑ а б Theoretical Computer Science: взгляд математика[недоступне посилання з Май 2018] // Компьютерра, № 2 от 22 января 2001 года
- ↑ Алгоритм Тарского [Архівовано 29 березня 2017 у Wayback Machine.] // семинар «Введение в Computer Science», доклад Матиясевича (2004)
Джерела[ред. | ред. код]
- Роджерс Х. Теория рекурсивных функций и эффективная вычислимость. — М. : Мир, 1972. — 416 с.(рос.)
- Алгоритм Тарського [Архівовано 8 травня 2013 у Wayback Machine.] — лекції Ю. В. Матіясевича (відео)
- Вільна реалізація алгоритму [Архівовано 25 квітня 2016 у Wayback Machine.]
|
Це незавершена стаття з логіки. Ви можете допомогти проєкту, виправивши або дописавши її. |