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

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