Куценко Д. А. Математическая логика. Метод резолюций в логике предикатов |
6 |
|||||||
1. |
Положим σv0 = ε и W0 = W . |
|
|
|
|
|
||
2. |
Так как |W0| ≠ 1, то σv0 не является НОУ для W . Поэтому находим множество несогла- |
|||||||
|
сованности D0 = { ( ), |
}. |
|
|
|
|
|
|
3. |
В D0 имеется переменная 0 |
= , которая не встречается в 0 = ( ). Пусть λ0 |
= |
|||||
|
= { 0/ 0} = { ( )/ }. |
|
|
|
|
|
|
|
4. |
Пусть σv1 = σv0 λ0 = ε { ( )/ } = { ( )/ }, |
|
|
|
||||
|
W1 |
= |
|
λ0 |
= ( ), ( ) , , |
{ ( )/ } = |
|
|
|
|
W0 |
= { ( ( ), ( )), ( ( ) }), ( ) . |
|
||||
|
|
|
|
|
{ ( |
) ( |
) } |
|
5. |
Так как |W1| ≠ 1, то σv1 не является НОУ для W . Поэтому находим множество несогла- |
|||||||
|
сованности D1 = { ( ), |
( )}. |
|
|
|
|
||
6. |
В D1 нет элемента, который был бы переменной. Следовательно, W неунифицируемо. |
|||||||
{ ( ) }
Итак, множество выражений W = ( ), ( ) , ( , ) неунифицируемо.
Отметим, что алгоритм унификации всегда завершает работу для любого конечного непустого множества выражений, так как иначе породилась бы бесконечная последова-
тельность W σv, W σv, W σv, . . . конечных непустых множеств, обладающая тем свойством,
0 1 2
что каждое последующее множество содержит на одну переменную меньше, чем преды-
дущее (а именно, W σv содержит , а W σv её уже не содержит). Но это невозможно, так
+1
как W содержит только конечное число различных переменных.
1.6. Склейки и резольвенты
Если две или более литер (с одинаковым знаком) дизъюнкта C имеют НОУ σv, то Cσvназывается склейкой C. Если склейка Cσv— однолитерный дизъюнкт, то она называется единичной склейкой.
Пример 1.11. Пусть C = ( ) |
( ) ( ). Тогда литеры ( ) и |
( ) |
имеют НОУ |
|||||||||||
|
|
|
|
|
( |
|
) |
|
|
|
|
|
( |
) |
= ( )/ |
|
|
|
) |
|
( |
) |
|
||||||
σv |
{ |
}. Следовательно, C |
|
|
( |
() |
|
|
|
|
|
есть склейка C. |
||
Пусть |
C1 и |
|
|
|
1) |
(называемые |
дизъюнктами-посылками), которые |
|||||||
C2 — два дизъюнкта |
||||||||||||||
не имеют никаких общих переменных. Пусть L1 и L2 — две литеры в C1 и C2 соответственно |
||||||||||||||
(т. е. L1 C1, L2 C2). Если L1 и |
L2 |
имеют НОУ σv, то дизъюнкт |
|
|
||||||||||
|
|
|
|
σv |
σv |
|
σv |
σv |
|
|
||||
|
|
|
(C1 {L1 |
}) |
(C2 |
{L2}) |
|
|
||||||
называется (бинарной) резольвентой C1 и C2. Литеры L1 и L2 называются отрезаемыми литерами.
Пример 1.12. Найдём бинарную резольвенту дизъюнктов
C1 = ( ) ( ), |
C2 = ( ) ( ). |
Так как переменная входит и в C1, и в C2, то мы заменим переменную на в C2,
итогда C2 = ( ) ( ). Выбираем литеры L1 = ( ) и L2 = ( ). Так как L2 = ( ), то L1
иL2 имеют НОУ σv= { / }. Следовательно,
( |
σv σv |
) ( |
σv |
σv |
) |
= |
( |
( ) |
( ) |
= () ), |
( |
|
|
|
|
|
|
|
) |
|
C1 {L1} C2 {L2} |
|
= |
{ ( ), ( )} { ( )} { ( ), ( )} { ( )} = |
|||||||||||||||
|
|
|
|
|
|
|
{ |
|
} { |
} { |
( ) |
} |
= ( ) |
|
( ). |
||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|||||||
1)Дизъюнкты C1 и C1 далее рассматриваются как множества литер, поэтому над ними можно выполнять такие операции, как вычитание ¾ ¿ и объединение ¾ ¿ множеств (см. пример 1.2 на с. 2).
Куценко Д. А. Математическая логика. Метод резолюций в логике предикатов |
7 |
Таким образом, ( ) ( ) бинарная резольвента дизъюнктов C1 и C2, а ( ) и ( ) отрезаемые литеры.
Резольвентой дизъюнктов-посылок C1 и C2 может быть одна из следующих резольвент:
1)бинарная резольвента дизъюнктов C1 и C2;
2)бинарная резольвента дизъюнкта C1 и склейки C2;
3)бинарная резольвента дизъюнкта C2 и склейки C1;
4)бинарная резольвента склейки C1 и склейки C2.
Пример 1.13. Пусть C1 = ( ) |
( ) |
( ) |
и C2 = |
|
( |
( ) |
) |
( ). Склейкой C1 |
|||||||||||||
|
= ( ) |
) |
( ) |
) |
( |
) |
( |
) |
|
( |
|
) |
|
( ) |
) |
( ) |
|
||||
является C1′ |
|
( |
|
|
( |
|
|
|
|
|
|
|
|
|
|
( |
|
|
|||
|
|
|
|
|
)) |
|
. Бинарной резольвентой C1′ |
и C2 является |
( |
) |
|
. |
|||||||||
Следовательно, |
|
( ) |
( ) |
есть резольвента C1 и C2. |
|
|
|
|
|
|
|
|
|
||||||||
|
( ( |
|
|
|
|
|
|
|
|
|
|
|
|
|
|||||||
1.7. Алгоритм метода резолюций
Основной идеей метода резолюций является проверка того, содержит ли множество дизъюнктов K пустой дизъюнкт . Если это так, то K невыполнимо. Если K не содержит , то следующие шаги заключаются в выводе новых дизъюнктов до тех пор, пока не будет получен (что всегда будет иметь место для невыполнимого K ). Таким образом, принцип резолюции рассматривается как правило вывода, с помощью которого из K порождаются новые дизъюнкты.
Сформулируем алгоритм метода резолюций для логики предикатов. Исходным данным для него является множество дизъюнктов K , противоречивость которого нужно доказать.
Шаг 1. Если в K есть пустой дизъюнкт ( K ), то выдать «K противоречиво» и завершить работу. В противном случае перейти к шагу 2.
Шаг 2. Найти в K такие дизъюнкты или склейки дизъюнктов C1 и C2, которые содержат унифицируемые литеры L1 и L2 соответственно. Если таких дизъюнктов нет, то выдать «K непротиворечиво» и завершить работу. В противном случае перейти к шагу 3.
Шаг 3. Вычислить резольвенту C1 и C2, добавить её в K и возвратиться к шагу 1.
Пример 1.14. Пусть задано множество дизъюнктов
K = { ( ) ( ), ( ), ( , ), ( ) ( , )}.
Докажем его противоречивость с помощью метода резолюций.
1. Так как / K , то находим в K дизъюнкты-посылки C1 = ( ) ( ) и C2 = ( ).
В этом случае отрезаемыми литерами являются L1 = ( ) и L2 = ( ), их НОУ { / }.
2.Резольвентой C1 и C2 является ( ). Добавляем её в K .
3.Так как / K , то находим в K дизъюнкты-посылки C1 = ( ) и C2 = ( ) ( , ). Отрезаемыми литерами являются L1 = ( ) и L2 = ( ), их НОУ { / }.
4.Резольвентой C1 и C2 является ( , ). Добавляем её в K .