Математическая логика и теория алгоритмов

3. Логическое следствие из множества формул логики выска­ зываний. 4. Проблема дедукции логики высказываний. Решение проблемы дедукции с использованием противоречивости специальной формулы. 5. Литералы, контрарные литералы, дизъюнкты. 6. Бинарные резольвенты дизъюнктов логики высказываний. 7. Теорема о полноте метода резолюций. 8. Метод резолюций в логике высказываний. 9. Метод насыщения уровня. 10. Стратегии вычеркивания. 11. Лок-резолюция. Теорема о полноте метода лок-резолюций. Зависит ли результат лок-резолюции от изменения индексов литера­ лов? 12. Метод резолюций для хорновских дизъюнктов. 13. Определение логического следствия для формул логики пре­ дикатов. 14. Определение сколемовских стандартных форм. Для каждой ли формулы логики предикатов существует сколемовская стандартная форма? 15. Единственна ли сколемовская стандартная форма для заданной формулы логики предикатов? 16. Алгоритмы нахождения сколемовских стандартных форм. 17. Когда формула равносильна своей сколемовской стандарт­ ной форме? 18. Унификация. Алгоритмы унификации. 19. Метод резолюции в логике предикатов, отличия от метода резолюций в логике высказываний. 20. Приложение метода резолюций для анализа силлогизмов Аристотеля. 21. Использование метода резолюций в ПРОЛОГе при работе с фактами. 22. Для каких задач вводится ANS-предикат? 23. Приведите примеры введения правил в ПРОЛОГе. 24. Рекурсивное задание правил в ПРОЛОГе. 129