5.Так как / K , то находим в K дизъюнкты-посылки C1 = ( , ) и C2 = ( , ). Отрезаемые литеры L1 = ( , ) и L2 = ( , ), их НОУ ε.

6.Резольвента C1 и C2 есть . Добавляем её в K .

7.Так как K , то K противоречиво, что и требовалось доказать.

Вывод пустого дизъюнкта может быть наглядно представлен с помощью дерева вывода, вершинами которого являются или исходные дизъюнкты, или резольвенты, а корнем — пустой дизъюнкт.

Пример 1.15. Дерево вывода для примера 1.14 изображено на рис. 1.1. Рядом с резольвентами указан НОУ их дизъюнктов-посылок.

ε

Рис. 1.1. Дерево вывода для примера 1.14

1.8. Стратегии метода резолюций

В множестве дизъюнктов существует, как правило, не одна пара дизъюнктов, к которым можно применить правило резолюций, поэтому при автоматическом доказательстве теорем методом резолюций б´ольшая часть вычислений приходится на поиск дизъюнк- тов-посылок. Неограниченное применение правила резолюций может вызвать порождение большого количества излишних дизъюнктов.

Реализация процедуры выбора дизъюнктов-посылок из множества дизъюнктов называется стратегией метода резолюций.

Стратегии можно разделить на два класса:

1)полные стратегии — гарантируют нахождение доказательства теоремы, если оно существует (в их основе лежит полный перебор);

2) неполные стратегии — могут в некоторых случаях не находить доказательства, но они работают быстрее, чем полные.

Рассмотрим следующие полные стратегии.

1.8.1. Стратегия насыщения уровня

Пусть K — исходное множество дизъюнктов. Обозначим K0 само множество дизъюнктов и назовём его уровнем нулевого порядка. Уровень первого порядка K1 — объединение K

с множеством всех резольвент, непосредственно порождённых от дизъюнктов K . Тогда

уровень -го порядка K состоит из объединения множества K −1 и множества резольвент, порождённых из K −1. Значение называется уровнем опровержения.

Стратегия насыщения уровня предполагает последовательное порождение всех резольвент уровня 1-го порядка, затем уровня 2-го порядка и т. д. до получения пустого дизъюнкта.

Таким образом, данная стратегия является стратегией поиска в ширину.

Пример 1.16. Докажем с помощью метода резолюций противоречивость множества дизъюнктов

K = { , , , , },

используя стратегию насыщения уровня.

Уровень нулевого порядка K0 составляют дизъюнкты

D1 = ,

D2 = ,

D3 = ,

D4 = .

D5 = .

Уровень первого порядка K1 будут составлять дизъюнкты из K0, а также

D6 = (резольвента D1 и D2),

D7 = (резольвента D1 и D2),

D8 = (резольвента D2 и D3),

D9 = (резольвента D1 и D4),

D10 = (резольвента D3 и D4),

D11 = (резольвента D3 и D5),

D12 = (резольвента D4 и D5).

Уровень второго порядка K2 будут составлять дизъюнкты из K1, а также

D13 = (резольвента D1 и D6),

D14 = (резольвента D2 и D6),

D15 = (резольвента D1 и D7),

D16 = (резольвента D2 и D7),

D17 = (резольвента D3 и D7),

D18 = (резольвента D4 и D7),

D19 = (резольвента D1 и D8),

D20 = (резольвента D6 и D8),

D21 = (резольвента D2 и D9),

D22 = (резольвента D6 и D9),

D23 = (резольвента D8 и D9),

D24 = (резольвента D5 и D10).

В итоге получили пустой дизъюнкт. Противоречивость K доказана (за 19 шагов).

Как видно из примера 1.16, порождено множество лишних дизъюнктов. Так, D6 и D7 — тождественно истинные дизъюнкты. Удаление или добавление тождественно истинного дизъюнкта не влияет на выполнтмость множества дизъюнктов, поэтому такие дизъюнкты должны быть удалены из вывода. Далее, некоторые дизъюнкты порождаются неоднократно, например, , , . Это делает стратегию насыщения уровня неприменимой на практике.