"Математическая логика и теория алгоритмов" для студентов, обучающихся по направлению "Информационные технологии".
Весенний семестр 2007/08 учебного года

Экзаменационные вопросы

    Язык логики высказываний и его семантика

  1. Слова, вхождения, формальные языки: определения и примеры.
  2. Язык логики высказываний.
  3. Интерпретация языка логики высказываний, истинностное значение формулы.
  4. Пропозициональные тавтологии, примеры.
  5. Логика высказываний: логическое следствие, теорема о логическом следствии, логически эквивалентные формулы.
  6. Теорема о подстановке пропозициональных формул в пропозициональную тавтологию.
  7. Теорема об эквивалентной замене (семантический вариант) для логики высказываний.
  8. Теорема о выражении булевой функции формулами, находящимися в конъюнктивной и дизъюнктивной нормальных формах.
  9. Теорема о выражении булевой функции пропозициональной формулой, в которую из логических связок входит только одна.
  10. Выражение булевой функции полиномом Жегалкина.

    Общее понятие исчисления

  11. Исчисление и вывод: определения и примеры.
  12. Вывод из гипотез: определения и примеры.

    Исчисление высказываний гильбертовского типа

  13. Формулировка исчисления высказываний гильбертовского типа. Пример вывода.
  14. Теоремы о корректности и непротиворечивости исчисления высказываний гильбертовского типа.
  15. Теорема о дедукции для исчисления высказываний гильбертовского типа.
  16. Техника естественного вывода для исчисления высказываний гильбертовского типа.
  17. Определения совместного, непротиворечивого и полного множеств пропозициональных формул. Теорема о непротиворечивости совместного множества пропозициональных формул.
  18. Теорема о совместности непротиворечивого множества пропозициональных формул (с леммами).
  19. Теоремы о компактности для логики высказываний и о полноте исчисления высказываний гильбертовского типа.
  20. Поиск вывода в исчислении высказываний гильбертовского типа. Алгоритм Британского музея.

    Секвенциальное исчисление высказываний генценовского типа

  21. Систематический поиск контрпримера для пропозициональной формулы.
  22. Формулировка секвенциального исчисления высказываний генценовского типа.
  23. Пример вывода в секвенциальном исчислении высказываний. Дерево поиска вывода и дерево вывода.
  24. Теоремы о корректности и полноте секвенциального исчисления высказываний.
  25. Некоторые правила, допустимые в секвенциальном исчислении высказываний.

    Язык логики предикатов и его семантика

  26. Определение языка первого порядка.
  27. Основные определения, касающиеся вхождений предметных переменных в предикатные формулы.
  28. Интерпретация языка первого порядка, истинностное значение формулы.
  29. Примеры языков первого порядка и их интерпретаций.
  30. Выражение предиката формулой, примеры.
  31. Свободные подстановки.
  32. Конгруэнтные формулы. Лемма о чистоте переменных.
  33. Переименование связанных переменных, правильные подстановки.
  34. Общезначимые предикатные формулы, логическое следствие, теорема о логическом следствии, логически эквивалентные формулы.
  35. Утверждения о логической эквивалентности некоторых предикатных формул, в том числе теорема об эквивалентной замене (семантический вариант). Доказательства нескольких утверждений.
  36. Теорема о предварённой нормальной форме.

    Исчисление предикатов гильбертовского типа

  37. Формулировка исчисления предикатов гильбертовского типа. Пример вывода.
  38. Теоремы о корректности и непротиворечивости исчисления предикатов гильбертовского типа.
  39. Теорема о дедукции для исчисления предикатов гильбертовского типа.
  40. Теорема о выводимости (в исчислении предикатов гильбертовского типа) частного случая пропозициональной тавтологии. Некоторые правила, допустимые в исчислении предикатов гильбертовского типа.
  41. Определения совместного, непротиворечивого и полного множеств предикатных формул. Теорема о непротиворечивости совместного множества предикатных формул.
  42. Теорема о существовании модели (без доказательства). Теорема Лёвенгейма-Скулема, теоремы о компактности для логики предикатов и о полноте исчисления предикатов гильбертовского типа.
  43. Синтаксическая эквивалентность формул. Теорема об эквивалентной замене (синтаксический вариант).

    Секвенциальное исчисление предикатов генценовского типа

  44. Систематический поиск контрпримера для формулы с кванторами.
  45. Формулировка секвенциального исчисления предикатов генценовского типа. Пример вывода в этом исчислении.
  46. Теоремы о корректности и непротиворечивости секвенциального исчисления предикатов.
  47. Теорема о полноте секвенциального исчисления предикатов (без доказательства), соотношение секвенциального исчисления предикатов и исчисления предикатов гильбертовского типа, допустимость правила сечения.

    Формальные аксиоматические теории

  48. Формальные аксиоматические теории: основные определения.
  49. Теории с равенством: определения и примеры.
  50. Теорема о существовании нормальной модели.
  51. Аксиомы элементарной арифметики.
  52. Нестандартная модель арифметики.
  53. Доказательство коммутативности сложения в элементарной арифметике.
  54. Наивная теория множеств. Парадокс Рассела.
  55. Аксиомы теории множеств Цермело-Френкеля.
  56. Теория множеств Цермело-Френкеля: упорядоченная пара и теорема о её основном свойстве.
  57. Отношения и функции в теории множеств Цермело-Френкеля. Аксиома выбора.
  58. Натуральные и целые числа в теории множеств Цермело-Френкеля.

    Метод резолюций и основы логического программирования

  59. Метод резолюций для логики высказываний, теорема о его корректности.
  60. Скулемовская стандартная форма: определение, примеры, представление в виде множества дизъюнктов.
  61. Теорема о выполнимости формулы и её скулемовской стандартной формы.
  62. Эрбрановская интерпретация множества дизъюнктов: определения и примеры.
  63. Теорема о ложности множества дизъюнктов в эрбрановских интерпретациях.
  64. Семантические деревья для множества дизъюнктов: определения и примеры.
  65. Теорема Эрбрана в терминах семантических деревьев.
  66. Теорема Эрбрана в терминах основных примеров дизъюнктов.
  67. Алгоритм проверки невыполнимости множества дизъюнктов, основанный на теореме Эрбрана.
  68. Унификаторы: определения и примеры.
  69. Алгоритм унификации.
  70. Метод резолюций для логики предикатов, его корректность, примеры.
  71. Лемма подъёма.
  72. Теорема о полноте метода резолюций для логики предикатов.
  73. Алгоритм доказательства методом резолюций.
  74. Логическая программа и её декларативная семантика.
  75. SLD-резолюция. Пример представления знаний в виде логической программы и поиска ответа на запрос к логической программе.
  76. Операционная семантика логической программы. Теорема о корректности вычисленной подстановки.

    Теория вычислимости

  77. Машины Тьюринга.
  78. Вычислимые по Тьюрингу функции. Тезис Чёрча.
  79. Нормальные алгорифмы Маркова.
  80. Разрешимые и перечислимые множества натуральных чисел. Теорема Поста.
  81. Теорема о равносильности четырёх определений перечислимого множества натуральных чисел.
  82. Разрешимые и перечислимые отношения на натуральных числах.
  83. Теоремы о проекции.
  84. Разрешимые и перечислимые языки и словарные отношения.
  85. Нумерация вычислимых функций.
  86. Теорема о параметризации.
  87. Универсальные функции. Теорема о непродолжимости универсальной функции.
  88. Понятие массовой проблемы разрешения. Теоремы о неразрешимости проблем самоприменимости и остановки. Пример неперечислимого множества.
  89. Теорема о рекурсии.
  90. Теорема Райса.
  91. Постановка проблемы эквивалентности для ассоциативных исчислений и проблемы равенства для полугрупп.
  92. Теорема о существовании ассоциативного исчисления с неразрешимой проблемой эквивалентности.
  93. Теоремы о неразрешимости проблемы общезначимости и проблемы выводимости для исчисления предикатов.
  94. Перечислимость множества теорем рекурсивно аксиоматизируемой теории.
  95. Эффективно неотделимые множества.
  96. Теорема Гёделя о неполноте арифметики в форме Россера.
  97. Теорема о неразрешимости арифметики.
  98. Вторая теорема Гёделя.

    Элементы теории сложности вычислений

  99. Задачи распознавания, кодирование и языки. Временная и ёмкостная сложность детерминированной машины Тьюринга. Класс P.
  100. Недетерминированная машина Тьюринга, её временная и ёмкостная сложность. Класс NP.
  101. Теорема о совпадении класса NP с классом полиномиально верифицируемых языков.
  102. Теорема о временной сложности детерминированной машины Тьюринга, распознающей язык из класса NP.
  103. Полиномиальная сводимость, NP-полные языки: определения и простейшие теоремы.
  104. Примеры NP-полных языков.

    Исчисление Хоара для доказательства корректности программ

  105. Определение программы и её операционной семантики.
  106. Аксиоматическая семантика программы: формулировка исчисления Хоара. Пример вывода в этом исчислении.
  107. Теорема о корректности исчисления Хоара относительно операционной семантики.