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

1. Осигуряване на еднозначен прочит с помощта на скоби и разделители.
2. Функции и предикати в дадено множество. Сигнатури и структури. Променливи и оценки на променливите.
3. Термове и атомарни формули на предикатното смятане. Семантика на термовете и атомарните формули.
4. Променливи на терм и на атомарна формула. Затворени термове и атомарни формули.
5. Субституции.
6. Оператори за присвояване, съответни на субституция. Субституции, удовлетворяващи дадено множество от атомарни формули в дадена структура.
7. Умножение на субституции.
8. Хорнови програми и хорнови запитвания. SLD-резолюция. Основни семантични свойства на непосредствената и на общата 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. Привеждане на формули в пренексен вид.
32. Скулемизация.
33. Теорема на Ербран.