Конспект по Логическо програмиране
за II курс информатика, I поток, уч. година 2001/2002
  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. Заместване на променлива с терм в логическа формула. Преименуване на свързана променлива.
  31. Привеждане на логическа формула в пренексен вид.
  32. Скулемизация.