Кафедра математической логики и теории алгоритмов

Механико-математического факультета МГУ


Спецкурс «Компьютерная логика» Профессор С.Н. Артёмов

email: SArtemov@gc.cuny.edu

Из двух направлений в математической логике — классического (Фреге, Гильберт, Гёдель, Тарский) и интуиционистского (Брауэр, Колмогоров, Карри, Чёрч) — последнее оказывает наибольшее влияние на области науки, лежащие вне пределов традиционной логики. Интуиционистская логика и функциональные исчисления были открыты в первой трети ХХ века как средства изучения оснований математики и впоследствии оказались мостом, соединяющим доказательства и вычислительные программы. К настоящему времени можно говорить о новом научном направлении «Компьютерная Логика», выросшем на интуиционистской традиции в математической логике и ставшем неотьемлемой частью как математической логики так и Computer Science.

Программа:

  • Интуиционистская логика: исходная семантика Брауэра-Гейтинта-Колмогорова. Исчисление. Модели.
  • Генценовские исчисления и естественный вывод.
  • Модальная логика, модели. Гёделевское сведение интуиционистской логики к модальной.
  • Типовая комбинаторная логика, типовое лямбда-исчисление. Изоморфизм Карри-Ховарда естественных выводов и типовых лямбда-термов.
  • Полиномы доказательств и формулы, несущие доказательства. Логика доказательств.
  • Решение задачи Гёделя о реализуемости модальной и интуиционистской логики в классической логике доказательств. Математическая форма семантики Брауэра-Гейтинта-Колмогорова
  • Функциональная логика доказательств.
  • Рефлекcивная комбинаторная логика и лямбда-исчисление.

Спецкурс будет читаться с 24 февраля по 7 марта 2003 года

понедельник с 18:05 ауд. 12-12
четверг с 18:05 ауд.13-04
пятница с 16:20 ауд. 14-14

В некоторые дни возможно изменение аудитории на 13-05

Первая лекция состоится …>>


Страница спецкурса http://markov.math.msu.ru/rus/cl.htm