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

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. Скулемизация.