"Дополнительные главы математической логики и теории алгоритмов" для магистрантов, обучающихся по направлению "Информационные технологии".
Осенний семестр 2010/11 учебного года.
Экзаменационные вопросы

Лектор Герасимов Александр Сергеевич

Логика высказываний

1. Синтаксис логики высказываний.
2. Исчисление натуральных выводов для логики высказываний.
3. Правила, выводимые в исчислении натуральных выводов для логики высказываний.
4. Семантика логики высказываний.
5. Теорема о корректности исчисления натуральных выводов для логики высказываний.
6. Теорема о полноте исчисления натуральных выводов для логики высказываний.
7. Теорема о семантическом следствии для логики высказываний.
8. Построение КНФ по таблице истинности. Алгоритм проверки общезначимости КНФ. Связь выполнимости и общезначимости пропозициональных формул.
9. Алгоритм проверки выполнимости хорновских формул, теорема о его корректности.
10. Алгоритмы проверки выполнимости пропозициональных формул.

    Логика предикатов

11. Язык первого порядка.
12. Свободные и связанные вхождения предметных переменных в предикатные формулы. Подстановки, свободные подстановки.
13. Исчисление натуральных выводов для логики предикатов.
14. Исчисление натуральных выводов с равенством.
15. Теорема о выводимо эквивалентных предикатных формулах.
16. Интерпретация языка первого порядка. Нормальная интерпретация. Истинностное значение формулы.
17. Примеры языков первого порядка и их интерпретаций.
18. Теорема о семантическом следствии для логики предикатов. Корректность и полнота исчисления натуральных выводов (с равенством) для логики предикатов. Некоторые неразрешимые проблемы для логики предикатов.

    Верификация моделей

19. Синтаксис логики линейного времени LTL.
20. Семантика LTL.
21. Примеры LTL-формул, нахождение их истинностных значений.
22. Примеры LTL-спецификаций.
23. Эквивалентные LTL-формулы. Полные наборы темпоральных связок для LTL.
24. Две попытки моделирования взаимного исключения и верификации моделей.
25. Верификатор моделей NuSMV: простая программа, описываемая ею модель, верификация модели.
26. Верификатор моделей NuSMV: моделирование взаимного исключения и верификация модели.
27. Синтаксис логики деревьев вычислений CTL.
28. Семантика CTL.
29. Примеры CTL-формул, нахождение их истинностных значений.
30. Примеры CTL-спецификаций.
31. Эквивалентные CTL-формулы. Полные наборы темпоральных связок для CTL.
32. Обобщённая логика деревьев вычислений CTL^*.
33. Сравнение выразительных возможностей CTL^*, CTL и LTL.
34. Помечающий алгоритм верификации моделей для CTL.
35. Алгоритм верификации моделей для CTL: более эффективный алгоритм обработки EG.
36. Псевдокод алгоритма верификации моделей для CTL.
37. Монотонные функции. Неподвижные точки функций. Теорема о неподвижных точках монотонной функции.
38. Алгоритм верификации моделей для CTL: корректность алгоритма обработки EG.
39. Алгоритм верификации моделей для CTL: корректность алгоритма обработки EU.
40. Верификация моделей для CTL с ограничениями справедливости.
41. Алгоритм верификации моделей для LTL: базовая стратегия, пример.
42. Алгоритм верификации моделей для LTL: построение автомата, реализация заключительного этапа.

    Двоичные разрешающие диаграммы и символьная верификация моделей

43. Булевы функции. Проблемы эффективности представлений булевых функций.
44. Двоичные разрешающие деревья. Двоичные разрешающие диаграммы (ДРД). Редукции ДРД.
45. Проверка выполнимости, общезначимости и выполнение булевых операций над булевыми функциями, представленными ДРД.
46. Упорядоченные двоичные разрешающие диаграммы (УДРД).
47. Алгоритм редукции УДРД.
48. Алгоритм применения булевой операции к УДРД.
49. Алгоритмы ограничения и квантификации УДРД.
50. Временная сложность построения УДРД.
51. Представление множеств состояний модели с помощью УДРД.
52. Представление отношения переходов модели с помощью УДРД. Построение УДРД, представляющей прообраз множества состояний при отношении переходов модели.
53. Синтез УДРД.