Термове и формули на предикатното смятане от първи ред. Хорнови клаузи. Унификация. Mетод на резолюцията в предикатното смятане от първи ред.
Анотация
Дефинират се синтактичните понятия терм и формула от даден език на предикатното смятане. Дава се семантика на термовете и формулите в дадена структура за езика. Доказва се, че множество от затворени универсални формули има модел точно тогава, когато множеството от частните му случаи е булево изпълнимо. Дефинира се понятието съждителен резолютивен извод и се доказва теоремата за коректност и пълнота на резолютивната изводимост. Описва се метода на резолюцията. Дефинира се понятието хорнов дизюнкт и се доказва, че изпълнимите множества от хорнови дизюнкти имат най-малък модел.
Примерни типове задачи, свързани с въпроса:
- Практически задачи – за дефиниране на предикат с помощта на Пролог; за проследяване на изпълнението на програма на Пролог.
- Теоретични задачи – за определимост и неопределимост на свойства в дадена структура; показване на изпълнимост на множество от предикатни формули чрез посочване на структура; доказване на неизпълнимост на множество от предикатни формули с помощта на метода на резолюцията.
Литература: [11], [12], [18], [26].
- Логическо Програмиране, въпрос 2. Термове и предикатни формули в език на предикатното смятане от 1ви ред.
- от началото (дефиниция на терм)
- до стойност на терм (това всъщност е семантика на терм)
- Логическо Програмиране, въпрос 3. Семантика на предикатни формули, определими подмножества, изображения.
- най-вече точката за стойност на предикатна формула
- булева изпълнимост и частни случаи
- хубаво е да се прегледа цялата тема, дефинициите в началото се ползват в твърденията
- твърдение 1
- твърдение 2
- Логическо Програмиране, въпрос 9. Съждителна резолюция.
- Логическо Програмиране, въпрос 15. Хорнови дизюнкти.
