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

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