Конспект по Логическо програмиране
за II курс информатика, I поток, уч. година 2008/2009

1. Осигуряване на еднозначен прочит с помощта на скоби и разделители.
2. Функции и предикати в дадено множество. Сигнатури и структури. Променливи и оценки на променливите.
3. Термове и атомарни формули над дадена сигнатура. Затворени термове и атомарни формули. Променливи на терм и на атомарна формула.
4. Семантика на термовете и атомарните формули.
5. Субституции.
6. Умножение на субституции.
7. Оператори за присвояване, съответни на субституция. Субституции, удовлетворяващи дадено множество от атомарни формули в дадена структура.
8. Хорнови програми и хорнови запитвания. SLD-резолюция.
9. Използване на SLD-резолюция за търсене на отговори на хорнови запитвания въз основа на хорнови програми.
10. Преименуващи субституции.
11. Унификация на атомарни формули и свеждането й до решаване на системи от уравнения между термове. Системи в решен вид. Прости случаи на нерешимост.
12. Решаване на системи от уравнения между термове. Коректност на метода.
13. Доказателство за успешно завършване на процеса, чрез който се търси решение на система от уравнения между термове.
14. Най-общ унификатор на две атомарни формули. Най-обща резолвента на хорново запитване и положителна хорнова клауза.
15. Търсене на отговор с помощта на най-общи резолвенти.
16. Ербранови структури. Съществуване и единственост на ербранова структура с отнапред дадено множество на верните затворени атомарни формули. Свеждане на вярност при оценка към вярност на затворен частен случай.
17. Изводимост на затворена атомарна формула чрез логическа програма. Минимален ербранов модел за логическа програма.
18. Tеорема за пълнота на SLD-резолюцията.
19. Пропадащи и успяващи хорнови запитвания при дадена хорнова програма.
20. Литерали и дизюнкти. Метод на резолюцията за множества от дизюнкти.
21. Свеждане на въпроса за съществуване на модел за множество от дизюнкти към същия въпрос за множеството на техните затворени частни случаи.
22. Теорема за компактност за множества от затворени дизюнкти.
23. Метод на Дейвис и Пътнам.
24. Пълнота на метода на резолюцията.
25. Формули на предикатното смятане. Еднозначност на прочита им. Семантика на формулите. Тъждествена вярност и изпълнимост на формула. Модели за множество от формули. Свободни променливи на формула. Затворени формули.
26. Представяне на безкванторна формула чрез крайно множество от дизюнкти.
27. Еквивалентни формули. Импликация и еквиваленция.
28. Прилагане на субституция към безкванторна формула. Пренексни формули. Заместване на променлива с терм в пренексна формул. Преименуване на свързана променлива на такава формула.
29. Привеждане на формули в пренексен вид.
30. Скулемизация.
31. Теорема на Ербран.