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

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