Вопросы/задания: Вопросы к экзамену

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

НА ЭКЗАМЕНЕ МОЖНО ПОЛЬЗОВАТЬСЯ:

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. Построить дерево вычислений для Пролог-программы.

Файл скачан с сайта StudIzba.com

При копировании или цитировании материалов на других сайтах обязательно используйте ссылку на источник