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