Конспект по Логическо програмиране
за II курс информатика, I поток, уч. година 2009/2010
  1. Осигуряване на еднозначен прочит с помощта на разделители и скоби.
  2. Функции и предикати в дадено множество. Сигнатури и структури. Променливи и оценки на променливите.
  3. Термове и атомарни формули на предикатното смятане. Семантика на термовете и атомарните формули.
  4. Променливи на терм и на атомарна формула. Затворени термове и атомарни формули.
  5. Субституции.
  6. Умножение на субституции.
  7. Оператори за присвояване, съответни на субституция.
  8. Субституции, удовлетворяващи дадено множество от атомарни формули в дадена структура.
  9. Хорнови програми и хорнови запитвания.
  10. SLD-резолюция и използването й за търсене на отговор на хорново запитване при дадена хорнова програма.
  11. Преименуващи субституции.
  12. Унификация на атомарни формули и свеждането й до решаване на системи от уравнения между термове. Системи в решен вид. Прости случаи на нерешимост.
  13. Решаване на системи от уравнения между термове. Коректност на метода.
  14. Доказателство за успешно завършване на процеса, чрез който се търси решение на система от уравнения между термове.
  15. Най-общ унификатор на две атомарни формули. Най-обща резолвента на хорново запитване и положителна хорнова клауза.
  16. Търсене на отговор с помощта на най-общи резолвенти.
  17. Ербранови структури. Съществуване и единственост на ербранова структура с отнапред дадено множество на верните затворени атомарни формули. Свеждане на вярност при оценка към вярност на затворен частен случай.
  18. Изводимост на затворена атомарна формула чрез логическа програма. Минимален ербранов модел за логическа програма.
  19. Tеорема за пълнота на SLD-резолюцията.
  20. Резолвента на хорново запитване и крайна редица от хорнови клаузи.
  21. Дърво на търсенето за дадено хорново запитване при дадена хорнова програма. Операционна семантика на хорновите програми.
  22. Литерали и дизюнкти. Метод на резолюцията за множества от дизюнкти.
  23. Свеждане на въпроса за съществуване на модел за множество от дизюнкти към същия въпрос за множество от затворени дизюнкти.
  24. Теорема за компактност за множества от затворени дизюнкти.
  25. Метод на Дейвис и Пътнам.
  26. Пълнота на метода на резолюцията
  27. Формули на предикатното смятане. Еднозначност на прочита им. Семантика на формулите. Свободни променливи на формула. Затворени формули.
  28. Тъждествена вярност и изпълнимост на формула. Модели за множество от формули. Прилагане на субституция към безкванторна формула.
  29. Представяне на безкванторна формула чрез крайно множество от дизюнкти.
  30. Еквивалентни формули. Импликация и еквиваленция.
  31. Заместване на променлива с терм във формула, която е в пренексен вид. Преименуване на свързана променлива на такава формула.
  32. Привеждане на формули в пренексен вид.
  33. Скулемизация.
  34. Теорема на Ербран.