 |
Лекция 8. Принцип резолюции для ИВ и ИП 1 порядка
|
|
|
|
Лекция 8. Принцип резолюции для ИВ и ИП 1 порядка
1. Получение множества дизъюнктов.
2. Принцип резолюции.
3. Унификация.
4. Теорема Робинсона
Итак, последовательным применением алгоритма приведения к ПНФ, алгоритма Сколема и алгоритма приведения к КНФ с сохранением свойства невыполнимости любая формула F может быть представлена набором дизъюнктов, объединенных кванторами общности. Такую формулу будем называть формулой, представленной в Сколемовской стандартной форме (ССФ).
В дальнейшем формулы вида " x1 " x2 … " xr [D1 & D2 & … & Dk], где D1, D2, …, Dk –дизъюнкты, а x1, x2, …, xr – различные переменные, входящие в эти дизъюнкты, будет удобно представлять как множество дизъюнктов S = {D1, D2, …, Dk}. Например, множеству дизъюнктов S = {Ø P(x, f(x)), P(x, y) Ú Ø R(x, g(y)), Q(x) Ú P(x, a)} соответствует следующая формула, представленная в ССФ: " x " y (Ø P(x, f(x)) & (P(x, y) Ú Ø R(x, g(y))) & (Q(x) Ú P(x, a))). И, наконец, когда говорят, что множество дизъюнктов S = {D1, D2, …, Dk} невыполнимо (противоречиво), то всегда подразумевают невыполнимость формулы " x1 " x2 … " xr [D1 & D2 & … & Dk], где x1, x2, …, xr – различные переменные, входящие в дизъюнкты.
Основная идея принципа резолюции заключается в проверке, содержит ли множество дизъюнктов S пустой (ложный) дизъюнкт £. Если это так, то S невыполнимо. Если S не содержит £, то следующие шаги заключаются в виде новых дизъюнктов до тех пор, пока не будет получен £ (что всегда будет иметь место для невыполнимого S). Таким образом, принцип резолюции рассматривается как правило вывода, с помощью которого порождаются новые дизъюнкты из S.
По существу принцип резолюции является расширением modus ponens на случай произвольных дизъюнктов с любым числом литер. Действительно, имея P и P ® Q, что равносильно Ø P Ú Q, можно вывести Q путем удаления контрарной пары P и Ø P. Расширение состоит в том, что если любые два дизъюнкта С1 и С2, имеют контрарную пару литер (P и Ø P), то, вычеркивая ее, мы формируем новый дизъюнкт из оставшихся частей двух дизъюнктов. Этот вновь сформированный дизъюнкт будем называть резольвентой дизъюнктов С1 и С2.
|
|
|
Пример 1 Пусть
C1: P Ú Ø Q Ú R,
C2: Ø P Ú Ø Q.
Тогда резольвента С: Ø Q Ú R.
Обоснованность получения таким образом резольвенты вытекает из следующей теоремы.
Теорема 6. Резольвента С, полученная из двух дизъюнктов С1 и С2, является логическим следствием этих дизъюнктов.
Если в процессе вывода новых дизъюнктов мы получим два однолитерных дизъюнкта, образующих контрарную пару, то резольвентой этих двух дизъюнктов будет пустой дизъюнкт £.
Таким образом, выводом пустого дизъюнкта £ из невыполнимого множества дизъюнктов S называется конечная последовательность дизъюнктов С1, С2, …, Сk такая, что любой Ci (i = 
) является или дизъюнктом из S, или резольвентой, полученной принципом резолюции, и Сk = £.
Вывод пустого дизъюнкта может быть наглядно представлен с помощью дерева вывода, вершинами которого являются или исходные дизъюнкты, или резольвенты, а корнем – пустой дизъюнкт.
Пример 2. Пусть S: 1. P Ú Q,
2. Ø P Ú Q,
3. P Ú Ø Q,
4. Ø P Ú Ø Q.
Тогда резольвентами будут: 5. Q (1, 2),
6. Ø Q (3, 4),
7. ð (5, 6).
Дерево вывода представлено на Рис. 1.
| ð |
| Q |
| Ø Q |
| Ø P Ú Q |
| P Ú Ø Q |
| Ø P Ú Ø Q |
| P Ú Q |
Рис. 1.
|
|
|
В заключение приведем пример вывода формулы из множества посылок принципом резолюции. Напомним, что доказательство вывода формулы G из множества посылок F1, F2, …, Fn сводится к доказательству противоречивости формулы F1 & F2 & … & Fn & Ø G (процедура опровержения).
Снова рассмотрим пример «горничная и дворецкий». Имеем следующее множество дизъюнктов:
1. Ø P Ú Q,
2. Ø Q Ú R,
3. Ø R Ú L,
Ø M Ú Ø L, и отрицание заключения Ø (Ø P Ú Ø M)
4. P,
5. M.
| P |
| Ø P Ú Q |
| Q |
| R |
| L |
| Ø M |
| ð |
| Ø Q Ú R |
| Ø R Ú L |
| Ø M Ú Ø L |
| M |
Дерево вывода представлено на Рис. 2.
Рис. 2.
Принцип резолюции для логики предикатов
Если в логике высказываний нахождение контрарных пар не вызывает трудностей, то для логики предикатов это не так. Действительно, если мы имеем дизъюнкты типа C1: P(x) Ú Ø R(x),
C2: Ø P(g(y)) Ú Q(y),
то резольвента может быть получена только после применения к С1 подстановки g(y) вместо х.
Имеем C¢ 1: P(g(y)) Ú Ø R(g(y)),
C2: Ø P(g(y)) Ú Q(y),
C: Ø R(g(y)) Ú Q(y).
Однако для случая
C1: P(a) Ú Ø R(x),
C2: Ø P(g(y)) Ú Q(y),
очевидно, никакая подстановка в контрарную пару неприменима и никакая резольвента не образуется. Дадим определение того, что является подстановкой.
Подстановкой будем называть конечное множество вида {t1/x1, t2/x2, …, tn/xn}, где любой ti – терм, а любая xi – переменная (1 £ i £ n), отличная от ti.
Подстановка называется фундаментальной, если все ti (1 £ i £ n), являются фундаментальными термами. Подстановка, не имеющая элементов, называется пустой подстановкой и обозначается через e.
Пусть Q = {t1/x1, t2/x2, …, tn/xn} – подстановка и W – выражение. Тогда WQ будем называть примером выражения W, полученного заменой всех вхождений в W переменной xi (1 £ i £ n), на вхождение терма ti. WQ будет называться фундаментальным примером выражения W, если Q – фундаментальная подстановка.
Например, применив к W = {P(x, f(y)) Ú Ø Q(z)} фундаментальную подстановку Q = {a/x, g(b)/y, f(a)/z}, получим фундаментальный пример WQ = {P(a, f(g(b))) Ú Ø Q(f(a))}.
|
|
|
Пусть Q = { t1/x1, t2/x2, …, tn/xn} и l = {u1/y1, u2/y2, …, um/ym} – две подстановки. Тогда композицией Q◦ l двух подстановок Q и l называется подстановка, состоящая из множества { t1l/x1, t2l/x2, …, tnl/xn, u1/y1, u2/y2, …, um/ym}, в котором вычеркиваются все til/xi в случае til = xi и uj/yj, если yj находится среди x1, x2, …, xn.
Пример 4. Q = {g(x, y)/x, z/y} и l = {a/x, b/y, c/w, y/z}. Q◦ l = {g(a, b)/x, y/y, a/x, b/y, c/w, y/z} = {g(a, b)/x, c/w, y/z}.
Можно показать, что композиция подстановок ассоциативна, т. е. (Q◦ l)◦ m = Q◦ (l◦ m).
Подстановку Q будем называть унификатором для множества выражений {W1, W2, …, Wk}, если W1Q = W2Q = … = WkQ. Будем говорить, что множество выражений {W1, W2, …, Wk} унифицируемо, если для него имеется унификатор. Унификатор s для множества выражений {W1, W2, …, Wk} называется наиболее общим унификатором (НОУ) тогда и только тогда, когда для каждого унификатора Q для этого множества выражений найдется подстановка l такая, что Q = s◦ l.
Пример 5. W = {P(x, a, f(g(w))), P(z, y, f(u))}. Тогда s = {z/x, a/y, g(w)/u} есть НОУ, а Q = {b/x, a/y, g(c)/u, b/z, c/w} есть унификатор, т. е. {b/x, a/y, g(c)/u, b/z, c/w} = {z/x, a/y, g(w)/u} ◦ {b/z, c/w}.
Опишем теперь алгоритм унификации, который находит НОУ, если множество выражений W унифицируемо, и сообщает о неудаче, если это не так.
1. Установить k = 0, Wk = W, sk = e. Перейти к пункту 2.
2. Если Wk не является одноэлементным множеством, то перейти к пункту 3. В противном случае положить s = sk и окончить работу.
3. Каждая из литер в Wk рассматривается как цепочка символов, и выделяются первые подвыражения литер, не являющиеся одинаковыми у всех элементов Wk, т. е. образуется так называемое множество рассогласований типа {xk, tk}. Если в этом множестве xk – переменная, а tk – терм, отличный от xk, то перейти к пункту 4. В противном случае окончить работу: Wk не унифицируемо.
4. Пусть sk+1 = sk◦ {tk/xk} и Wk+1 = Wk {tk/xk}.
5. Установить k: = k + 1 и перейти к пункту 2.
Пример 6. Найти НОУ для W = {P(y, g(z), f(x)), P(a, x, f(g(y)))}.
1. k = 0, s0 = e и W0 = W.
2. Так как W0 не является одноэлементным множеством, то перейти к пункту 3.
3. {y, a}, т. е. {a/y}.
4. s1 = s0 ◦ {a/y} = e ◦ {a/y} = {a/y}.
W1 = W0 {a/y} = {P(a, g(z), f(x)), P(a, x, f(g(a)))}.
5. Так как W1 опять неодноэлементно, то множество рассогласований будет {g(z), x}, т. е. {g(z)/x}.
|
|
|
6. s2 = s1 ◦ {g(z)/x} = {a/y, g(z)/x}.
W2 = W1 {g(z)/x} = {P(a, g(z), f(g(z))), P(a, g(z), f(g(a)))}.
7. Имеем {z, a}, т. е. {a/z}.
8. s3 = s2 ◦ {a/z} = {a/y, g(a)/x, a/z}.
W3 = W2 {a/z} = {P(a, g(a), f(g(a))), P(a, g(a), f(g(a)))} = {P(a, g(a), f(g(a)))}.
s3 = {a/y, g(a)/x, a/z} есть НОУ для W.
Можно показать, что алгоритм унификации всегда завершается на шаге 2, если множество W унифицируемо, и на шаге 3 – в противном случае.
Пусть С1 и С2 – два дизъюнкта, не имеющие общих переменных (это всегда можно получить переименованием переменных). И пусть L1 и L2 = Ø L1 – литеры в дизъюнктах С1 и С2 соответственно, имеющие НОУ s. Тогда бинарной резольвентой для С1 и С2 является дизъюнкт вида C = (C1s - L1s) È (C2s - L2s). Бинарная резольвента может быть получена одним из четырех способов:
1. резольвента для С1 и С2;
2. резольвента для С1 и фактора дизъюнкта С2;
3. резольвента для фактора дизъюнкта С1 и С2;
4. резольвента для фактора дизъюнкта С1 и фактора дизъюнкта С2.
Пример 7. Пусть C1= P(f(g(a))) Ú Ø R(b), C2 = Ø P(x) Ú Ø P(f(y)) Ú Q(y). Тогда C2s = C¢ 2 = Ø P(f(y)) Ú Q(y) и резольвентой для С1 и С¢ 2 будет С = Ø R(b) Ú Q(g(a)) (s = g(a)/y).
Принцип резолюции обладает важным свойством – полнотой, которое устанавливается следующей теоремой.
Теорема 7. (Теорема о полноте Дж. Робинсона). Множество дизъюнктов S невыполнимо тогда и только тогда, когда существует вывод принципом резолюции из S пустого дизъюнкта.
Вернемся к примеру
Все люди – животные: " y (S(y) ® C(y)).
Следовательно, голова человека является головой животного:
" x ($y (S(y) & V(x, y)) ® $z (C(z) & V(x, z))).
Посылку и отрицание заключения представим в виде следующего набора дизъюнктов:
1. Ø S(y) Ú C(y),
2. S(b),
3. V(a, b),
4. Ø C(z) Ú Ø V(a, z).
Дерево вывода имеет следующий вид (Рис. 3. )
.
| S(b) |
| Ø S(y) Ú C(y) |
| (s = b/y) C(b) |
| (s = b/z) Ø V(a, b) |
| ð |
| Ø C(z) Ú Ø V(a, z) |
| V(a, b) |
Рис. 3.
|
|
|
