"Математическая логика и теория алгоритмов" для студентов, обучающихся по направлению "Информационные технологии".
Весенний семестр 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. Теорема о корректности исчисления Хоара относительно операционной семантики.