МАТЕМАТИЧЕСКАЯ ЛОГИКА И ЛОГИЧЕСКОЕ ПРОГРАММИРОВАНИЕ.

           НА ЭКЗАМЕНЕ МОЖНО ПОЛЬЗОВАТЬСЯ:
           1. Списком правил вывода и поиска вывода в натуральном исчислении.
           2. Списком правил вывода в секвенциальном исчислении.

           ВОПРОСЫ.
           1. Язык логики предикатов: синтаксис и семантика. (Формула, свобод-
      ные и связанные вхождения переменных,  замкнутая формула, интерпретация.
      Примеры вычисления истинности формул в конечных интерпретациях.)
           2. Модель,  контрпример,  общезначимость и  логическое  следование.
      (Содержательный смысл логического следования. Теорема о дедукции. Приме-
      нение теоремы о дедукции к незамкнутым формулам.)
           3. Поиск  логического вывода в секвенциальном исчислении.  (Примеры
      построения выводов и контрпримеров. Пример формулы, не являющейся общез-
      начимой и не имеющей конечных контрпримеров.)
           4. Корректность секвенциального исчисления.  (Понятие  корректности
      исчисления. Теорема о корректности.)
           5. Полнота секвенциального исчисления. (Понятие полноты исчисления.
      Стандартная стратегия поиска вывода. Теорема о полноте.)
           6. Исчисление натурального вывода как модель содержательного  дока-
      зательства.  (Примеры  натуральных выводов и соответствующих им содержа-
      тельных доказательств.  Исключение гипотез.  Особенности применения пра-
      вил, вводящих и уничтожающих кванторы.)
           7. Поиск логического вывода в натуральном исчислении.  (Правила по-
      иска вывода. Примеры построения выводов по этим правилам.)
           8. Корректность натурального исчисления.  (Понятие корректности ис-
      числения. Теорема о корректности.)
           9. Полнота натурального исчисления.  (Понятие  полноты  исчисления.
      Теорема о полноте.)
           10. Эквивалентные преобразования в логике предикатов. (Отношение эк-
      вивалентности.  Три вида эквивалентности логических формул,  связь между
      ними.)
           11. Теоремы об отношении эквивалентности |=(А>B)&(В>A). (Пары экви-
      валентных формул,  замена эквивалентных подформул,  приведение к предва-
      ренной и конъюнктивной нормальным формам.)
           12. Теоремы об отношениях эквивалентности |=А<=>|=B и  А|=┴<=>B|=┴.
      (Замыкание  формул  кванторами общности,  приведение к скулемовской нор-
      мальной форме.)
           13. Поиск логического вывода методом резолюций. (Общая схема и при-
      меры построения выводов.)
           14. Корректность  метода резолюций.  (Понятие корректности исчисле-
      ния. Теорема о корректности.)
           15. Полнота метода резолюций.  (Понятие полноты исчисления. Теорема
      о полноте.)
           16. Эрбрановские  интерпретации.  (Эрбрановские  универсум и базис.
      Теорема о невыполнимости в эрбрановских интерпретациях. Теорема Эрбрана)
           17. Логика высказываний:  синтаксис,  семантика, секвенциальный вы-
      вод.  (Логика высказываний как частный случай логики предикатов.  Истин-
      ностные таблицы.  Секвенциальное исчисление для логики высказываний: от-
      личия поиска вывода и построения контрпримеров от логики предикатов.)
           18. Дедуктивный  поиск ответов на вопросы.  (Примеры поиска ответов
      на вопросы методом резолюций.  Неконструктивность классической логики  и
      ее конструктивность по отношению к логическим программам.)
           19. Модели множеств хорновских  дизъюнктов.  (Примеры  эрбрановских
      базисов, универсумов и моделей множеств хорновских дизъюнктов. Теорема о
      пресечении эрбрановских моделей.)
           20. Наименьшая эрбрановская модель. (Теорема об устройстве наимень-
      шей эрбрановской модели множества хорновских дизъюнктов.  Содержательный
      смысл и примеры построения наименьшей эрбрановской модели.)
           21. Декларативная семантика Пролога. (Теоремы главном свойстве наи-
      меньшей эрбрановской модели и о декларативной семантике.)
           22. Подстановки и унификаторы.  Наиболее общий унификатор. (Теорема
      о композиции подстановок. Алгоритм унификации. Теорема об алгоритме уни-
      фикации.)
           23. SLD-резолюция:  поиск  логического вывода.  (Примеры построения
      SLD-выводов. SLD-резолюция, как стратегия метода резолюций.)
           24. Корректность SLD-резолюции.
           25. Полнота SLD-резолюции с правилом выбора.
           26. Полнота SLD-резолюции с наиболее общим унификатором.
           27. Процедурная семантика Пролога.  (Примеры построения SLD-деревь-
      ев. Стандартная стратегия построения SLD-дерева.  Примеры программ,  для
      которых стандартная стратегия неполна.)
           28. Семантика операторов fail,  cut и not. Гипотеза замкнутости ми-
      ра.
           29. Алгоритмическая полнота Пролога.
           30. Теорема Черча о неразрешимости логики предикатов.

           ТИПИЧНЫЕ ЗАДАЧИ.
           1. Записать логическое суждение в виде замкнутой формулы.
           2. Построить модель/контрпример формулы.
           3. Построить вывод формулы в натуральном/секвенциальном исчислении.
           4. Построить вывод формулы методом резолюций.
           5. Написать Пролог-программу.
           6. Построить наименьшую эрбрановскую модель для Пролог-программы.
           7. Построить дерево вычислений для Пролог-программы.