"Дополнительные главы математической логики и теории алгоритмов" для магистрантов, обучающихся по направлению "Информационные технологии".
Осенний семестр 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. Синтез УДРД.