City: Test Saint Petersburg Novosibirsk Kazan Language: Русский English

Tarski's Algorithm
Saint Petersburg / autumn 2008, посмотреть все семестры

Enroll in the course to get notifications and to be able to submit home assignments.
Register to enroll now Login

Среди многочисленных результатов о разрешимости массовых проблем одним из самых замечательных является алгоритм Тарского, позволяющий установить истинность или ложность любой замкнутой арифметической формулы первого порядка с переменными для вещественных чисел. В качестве «бесплатного» приложения он дает разрешимость «элементарной» геометрии (через введенный Р. Декартом «метод координат»).

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

  • легка для понимания,
  • легка для программирования,
  • очень неэффективна (по сравнению с современными «продвинутыми» алгоритмами).

Лекции основаны на докладе Hoon Hong 2002–го года.

Date and time Class|Name Venue|short Materials
07 September
10:40–12:10
Лекции 1-2, Lecture ПОМИ РАН slides