Математическая логика и теория алгоритмов — различия между версиями

Материал из Кафедра математической кибернетики
Страница-перенаправление
Перейти к: навигация, поиск
м
 
(не показаны 9 промежуточные версии 2 участников)
Строка 1: Строка 1:
 +
#REDIRECT [[Математическая логика и логическое программирование (группа 318)]]
  
 +
<!--
 
Обязательный курс для студентов 241 группы 4 семестра обучения. Курс читает профессор [[Захаров Владимир Анатольевич|В. А. Захаров]].
 
Обязательный курс для студентов 241 группы 4 семестра обучения. Курс читает профессор [[Захаров Владимир Анатольевич|В. А. Захаров]].
  
Строка 10: Строка 12:
 
Лекция 2. '''Классическая логика предикатов первого порядка. Синтаксис. Термы и формулы.Семантика. Интерпретация. Выполнимость формул.''' '''[[Media: Lect241_2.pdf| Лекция 2.]]'''     
 
Лекция 2. '''Классическая логика предикатов первого порядка. Синтаксис. Термы и формулы.Семантика. Интерпретация. Выполнимость формул.''' '''[[Media: Lect241_2.pdf| Лекция 2.]]'''     
  
Лекция 3. '''Выполнимые и общезначимые формулы. Модели. Логическое следование.        Проблема общезначимости. Семантические таблицы.'''       
+
Лекция 3. '''Выполнимые и общезначимые формулы. Модели. Логическое следование.        Проблема общезначимости. Семантические таблицы.''' '''[[Media: Lect241_3.pdf| Лекция 3.]]'''
 +
      
  
Лекция 4. '''Подстановки. Табличный вывод. Корректность табличного вывода.'''       
+
Лекция 4. '''Подстановки. Табличный вывод. Корректность табличного вывода.''' '''[[Media: Lect241_4.pdf| Лекция 4.]]'''
 +
      
  
Лекция 5. '''Полнота табличного вывода. Теорема Левенгейма-Сколема.          Теорема компактности Мальцева. Автоматическое доказательство теорем.'''     
+
Лекция 5. '''Полнота табличного вывода. Теорема Левенгейма-Сколема.          Теорема компактности Мальцева. Автоматическое доказательство теорем.''' '''[[Media: Lect241_5.pdf| Лекция 5.]]'''
 +
      
  
Лекция 6. '''Общая схема метода резолюций. Равносильные формулы.          Теорема о равносильной замене. Предваренная нормальная форма. Сколемовская стандартная форма. Системы дизъюнктов.'''  
+
Лекция 6. '''Общая схема метода резолюций. Равносильные формулы.          Теорема о равносильной замене. Предваренная нормальная форма. Сколемовская стандартная форма. Системы дизъюнктов.''' '''[[Media: Lect241_6.pdf| Лекция 6.]]'''
 +
 
  
Лекция 7. '''Эрбрановские интерпретации. Теорема Эрбрана. Задача унификации.'''     
+
Лекция 7. '''Эрбрановские интерпретации. Теорема Эрбрана. Задача унификации.''' '''[[Media: Lect241_7.pdf| Лекция 7.]]'''
 +
    
  
Лекция 8. '''Алгоритм унификации.'''  
+
Лекция 8. '''Алгоритм унификации.''' '''[[Media: Lect241_8.pdf| Лекция 8.]]'''
 +
 
  
Лекция 9. '''Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций.'''     
+
Лекция 9. '''Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций.''' '''[[Media: Lect241_9.pdf| Лекция 9.]]'''     
  
Лекция 10. '''Полнота резолютивного вывода.'''    
+
Лекция 10. '''Полнота резолютивного вывода.''' '''[[Media: Lect241_10.pdf| Лекция 10.]]'''   
  
Лекция 11. '''Стратегии резолютивного вывода. Вычислительные возможности метода резолюций.'''
+
Лекция 11. '''Стратегии резолютивного вывода. Вычислительные возможности метода резолюций.''' '''[[Media: Lect241_11.pdf| Лекция 11.]]'''
 +
 
 +
Лекция 12. '''Интуиционистская логика.''' '''[[Media: Lect241_12.pdf| Лекция 12.]]'''
 +
 
 +
Лекция 13. '''Модальные логики.''' '''[[Media: Lect241_13.pdf| Лекция 13.]]'''
 +
 
 +
Лекция 14. '''Задача верификации программ. Логика Хоара.''' '''[[Media: Lect241_14.pdf| Лекция 14.]]'''
 +
 
 +
Лекция 15. '''Аксиоматические теории. Элементарная геометрия. Теория множеств. Арифметика Пеано.''' '''[[Media: Lect241_15.pdf| Лекция 15.]]'''
  
 
== Основная литература ==
 
== Основная литература ==
Строка 45: Строка 61:
  
 
[[Категория:Лекционные курсы кафедры МК]]
 
[[Категория:Лекционные курсы кафедры МК]]
 +
-->

Текущая версия на 12:19, 7 февраля 2019