Конспект по Логическо програмиране
за задочници от спец. математика и информатика, 2003 г.
- Префиксни изрази над дадено множество от думи.
 - Функции и предикати в дадено множество. Термове и атомарни формули.
 - Семантика на термовете и атомарните формули.
 - Логически формули и тяхната семантика.
 - Тъждествена вярност и изпълнимост на логическа формула.
 - Субституции. Прилагане на субституция към терм и към безкванторна формула.
 - Умножение на субституции.
 - Оператори за присвояване, съответни на субституция.
 - Частни случаи и варианти на безкванторна формула.
 - Търсене на формула, която е частен случай на две дадени атомарни формули.
 - Решаване на системи от уравнения между термове.
 - Резултатност на метода за решаване на системи от уравнения между термове.
 - Еквивалентни формули. Импликация.
 - Хорнови клаузи и логически програми. Хорнови цели. Изпълнимост на хорнова цел при дадена логическа програма.
 - Резолвента на хорнова цел с положителна хорнова клауза. Резолвентни редици.
 - Субституция, съответна на дадена резолвентна редица.
 - Ербранови структури.
 - Минимален ербранов модел на логическа програма.
 - Пълнота на резолюцията на хорнови цели с положителни хорнови клаузи.
 - Най-обща резолвента на хорнова цел и положителна хорнова клауза. Пълнота на резолюцията, използваща такива резолвенти.
 - Представяне на безкванторнa формулa в конюнктивен нормален вид.
 - Метод на резолюцията за множества от дизюнкти.
 - Пренексни формули. Заместване на свободна променлива с терм в пренексна формула. Преименуване на свързана променлива.
 - Привеждане на логическа формула в пренексен вид.
 - Скулемизация.