Конспект по Логическо програмиране
за II курс информатика, I поток, уч. година 2002/2003
  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. Скулемизация.
www.000webhost.com