ЛОГИЧЕСКО ПРОГРАМИРАНЕ

СЪДЪРЖАНИЕ

 
Най-нова версия

1. Уводен пример
2. Осигуряване на еднозначен прочит с помощта на скоби и разделители
3. Функции и предикати в дадено множество
4. Сигнатури и структури
5. Променливи и оценки на променливите
6. Термове и атомарни формули на предикатното смятане
7. Семантика на термовете и атомарните формули
8. Променливи на терм и на атомарна формула
9. Затворени термове и атомарни формули
10. Субституции
11. Умножение на субституции
12. Оператори за присвояване, съответни на субституция
13. Субституции, удовлетворяващи дадено множество от атомарни формули в дадена структура
14. Хорнови програми
15. SLD-резолюция
16. Преименуващи субституции. Варианти на положителна хорнова клауза
17. Унификация на атомарни формули и нейното свеждане до решаване на системи от уравнения между термове
18. Явно нерешими системи и системи в решен вид
19. Решаване на системи от уравнения между термове
20. Резултатност на метода, чрез който се търси решение на система от уравнения между термове
21. Най-общ унификатор на две атомарни формули
22. Най-обща резолвента на хорново запитване и положителна хорнова клауза
23. Търсене на отговор с помощта на най-общи резолвенти
24. Ербранови структури
25. Изводимост на затворена атомарна формула чрез логическа програма. Минимален ербранов модел
26. Теорема за пълнота на SLD-резолюцията
27. Пропадащи и успяващи хорнови запитвания при дадена хорнова програма
28. Литерали и дизюнкти
29. Прилагане на субституция към литерал и към дизюнкт
30. Метод на резолюцията за множества от дизюнкти
31. Свеждане на въпроса за съществуване на модел за множество от дизюнкти към същия въпрос за множество от затворени дизюнкти
32. Теорема за компактност за множества от затворени дизюнкти
33. Метод на Дейвис и Пътнам
34. Пълнота на метода на резолюцията
35. Формули на предикатното смятане
36. Семантика на формулите
37. Свободни променливи на формула
38. Затворени формули
39. Тъждествена вярност и изпълнимост на формули
40. Конюнкции и дизюнкции с произволен ненулев краен брой членове
41. Модели за множество от формули
42. Прилагане на субституция към безкванторна формула
43. Представяне на безкванторна формула чрез крайно множество от дизюнкти
44. Еквивалентни формули
45. Импликация и еквиваленция
46. Пренексни формули
47. Заместване на променлива с терм в пренексна формула
48. Преименуване на свързана променлива на пренексна формула
49. Привеждане на формули в пренексен вид
50. Скулемизация
51. Теорема на Ербран

• Азбучен показалец на термините

 
Предишна най-нова версия (незавършена)

• Technical Information
• Встъпителни бележки
• Функции и предикати в дадено множество
• Сигнатури и структури
• Променливи и оценки на променливите
• Уравновесени думи
• Термове и формули на предикатното смятане
• Семантика на термовете и формулите
• Променливи на терм, свободни и свързани променливи на формула
• Затворени термове и затворени формули
• Тъждествена вярност и изпълнимост на формули
• Следване на формула от дадена формула или дадено множество от формули
• Еквивалентни формули

        .   .   .

• Резолюция на положителна елементарна конюнкция с положителна хорнова клауза
• Резолвентни редици
• Намиране на удовлетворяващи субституции
• Пълнота на резолюцията на положителни елементарни конюнкции с положителни хорнови клаузи

        .   .   .

• Безкванторни формули с ограничено ползване на отрицание

        .   .   .

• Представяне на безкванторна формула чрез крайно множество от дизюнкти

        .   .   .

• Прилагане на субституция към произволна формула

        .   .   .

• Скулемизация
• Теорема на Ербран
  • Модели на множества от безкванторни формули и на множества от универсални затворени формули
  • Теорема за компактност за затворени дизюнкти
  • Формулировка и доказателство на теоремата на Ербран
• Пълнота на метода на резолюцията

 
Текстове от междинна версия

• Субституции
• Умножение на субституции
• Оператори за присвояване, съответни на субституция
• Прилагане на субституция към безкванторни формули

        .   .   .

• Варианти на безкванторна формула

        .   .   .

• Намиране на удовлетворяващи субституции за изпълнимите цели
• Най-общ частен случай на хорнова цел, имащ проста резолвента с дадена редица от хорнови клаузи
• Представяне на безкванторни формули в конюнктивна нормална форма

        .   .   .

Последно изменение: 4.06.2010 г.