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