Конспект по Логическо програмиране
за II курс информатика, I поток, уч. година 2002/2003
- Префиксни изрази над дадено множество от думи.
- Функции и предикати в дадено множество. Сигнатури и структури.
- Термове и атомарни формули.
- Логически формули.
- Запазване на тъждествената вярност и на изпълнимостта на логическа формула в дадена структура при поставяне или премахване на съответен вид квантори.
- Субституции.
- Оператори за присвояване, съответни на дадена субституция.
- Умножение на субституции.
- Частни случаи и варианти на безкванторна формула.
- Ербранови структури.
- Модел за множество от формули.
- Еквивалентни формули.
- Положителни и отрицателни хорнови клаузи, хорнови програми, хорнови цели. Изпълнимост на хорнова цел при дадено множество от положителни хорнови клаузи.
- Изводимост на затворена атомарна формула от множество от положителни хорнови клаузи. Минимален ербранов модел за такова множество. Следствия от съществуването му.
- Резолвента на хорнова цел с хорнова клауза. Резолвентни редици.
- Намиране на удовлетворяващи субституции за изпълнимите цели.
- Пълнота на резолюцията на хорнови цели с хорнови клаузи.
- Търсене на атомарна формула, която е частен случай на всяка от две дадени атомарни формули. Унификатори и унифицируемост на атомарни формули.
- Решаване на системи от уравнения между термове.
- Доказателство за успешно завършване на процеса, чрез който се търси решение на система от уравнения между термове.
- Най-общ унификатор на две атомарни формули. Най-обща резолвента на хорнова цел и хорнова клауза.
- Резолвенти на хорнова цел с редица от хорнови клаузи. Канонични резолвенти. Пълнота на резолюцията на хорнови цели с хорнови клаузи при използване на най-общи резолвенти.
- Дърво на търсенето за дадена хорнова цел при дадена хорнова програма. Пропадащи и успяващи цели.
- Представяне на безкванторни формули в конюнктивна нормална форма.
- Метод на резолюцията за множества от дизюнкти.
- Заместване на променлива с терм в произволна формула.
- Преименуване на свързана променлива. Привеждане на формули в пренексен вид.
- Скулемизация.