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

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