lec12

Литерал – произвольный атом или его отрицание. Дизъюнкт – выражение вида:

x1 x2 … xj … xk C1 C2 … Ci … Cn,

где Ci – литералы, (i=1..n);

x1, x2, … xj, … xk – все переменные встречающиеся в C1…Cn, (j=1..k).

Пустой дизъюнкт – дизъюнкт не содержащий ни одного литерала (как и в исчислении высказываний). Обозначение □.

22

Дизъюнкт может быть представлен в одном из следующих видов:

(1)x1 … xk (A1 A2 … Am B1 B2 … Be);

(2)x1 … xk ((A1 A2 … Am) ← (B1 B2 … Be));

(3)x1 … xk (A1 A2 … Am ← B1 B2 … Be);

(4) x1 … xk (A1, A2, … Am ← B1, B2, … Be);

(5){C1, C2, … Ci, … Cm, Cm+1, Cm+2, … Cm+j, … Cm+e},

–теоретико-множественное представление, где Ci=Ai, i=1..m; Cj+m= Bj, j=1..e;

(6){A1, A2, … Am, B1, B2, … Be};

(7)A1, A2, … Am ← B1, B2, … Be.

23

Каждый дизъюнкт является предложением.

!!! обратное – неверно. Но каждое предложение можно привести к СНФ.

Пример 12.5.

а) х y z (P(x,y) Q(y,z) R(x,y,z))

– дизъюнкт вида (1): х1=х, х2=y, х3=z; A1=P(x,y); B1=Q(y,z); B2=R(x,y,z). б) х y (P(x,f(y)), R(x,y) ← Q(x,y))

–дизъюнкт вида (4): х1=х, х2=y; A1=P(x,f(y)); A2= R(x,y); B1= Q(x,y). в) {P(x,f(y)), Q(x,y)}

–дизъюнкт вида (6): A1=P(x,f(y)); B1=Q(x,y).

Основной пример ƍ – предложение, полученное из дизъюнкта ƍ путём удаления кванторов и подстановки вместо всех переменных констант.

24

Хорновским дизъюнктом называется дизъюнкт вида:

x1 … xk (A ← B1, B2, … Bi, … Be),

где A, B1, B2, … Be – атомы, (e≥1); Bi – предпосылки хорновского дизъюнкта; А – заключение хорновского дизъюнкта.

Целевым утверждением (или целью) называется хорновский дизъюнкт, не содержащий заключения:

x1 … xk ( ← B1, B2, … Bi, … Be),

где Bi – подцели данной цели.

Факт – хорновский дизъюнкт, не содержащий ни одной предпосылки:

x1 … xk ( A ← )

25

Для каждой формулы ƍ логики предикатов с множеством свободных переменных x1, x2, … xk справедливо выражение, такое что:

ⱶ ƍ ⱶ х1 ... хk ƍ

Т.о. можно изучать предложение « х1 ... хk ƍ» вместо формулы ƍ.

Поскольку переменные во всех дизъюнктах считаются связанными кванторами всеобщности можно переименовать эти переменные, чтобы применять операцию резолюции для получения резольвенты двух дизъюнктов. Такое переименование называется нормализацией переменных.

26

Точно так же, как в логике высказываний, для множества дизъюнктов S в логике предикатов резолютивный вывод из S это конечная последовательность дизъюнктов C1, C2, … Ci, … Cn, что для каждого Ci (1≤i≤n):

Ci S, либо

Ci R({Cj,Ck}) при 1≤j,k<i.

R({Cj,Ck}) – множество резольвент Cj и Ck.

Утверждение 12.1. Если предложение Ϭ логики предикатов выводимо методом резолюции из множества S предложений логики предикатов:

S ⱶ Ϭ, то S { Ϭ} ⱶ □

т.е. из множества S выводим пустой дизъюнкт (□ никогда не выполним).

Утверждение 12.2. Пусть S – множество дизъюнктов и R*(S) – множество всех резольвент S. Если множество □ R*(S), то S – невыполнимо и наоборот, если S – невыполнимо, то множество R*(S) содержит □.

28

Переменная x свободна для терма t в формуле , если никакая из переменных терма t не становится связанной после подстановки терма t на все места свободных вхождений переменной x в формуле .

Обозначение: free(x,t, ) – «переменная х свободна для терма t в формуле ».

Пример 12.7. Проверка свободна ли переменная для терма в формуле.

= y P(х,y).

Здесь переменная х не свободна для терма y в формуле , поскольку после подстановки терма у на места свободных вхождений переменной х переменная у становится связанной. С другой стороны, переменная х свободна для терма z в формуле , если z есть переменная отличная от y, так как после замены переменной х на терм z в формуле переменная z, единственная переменная терма z, не становится связанной. Более того, y свободна для y в формуле (так как не содержит свободных вхождений переменной y).

30