Дискретная математика:
логика, группы, графы, фракталы

Акимов О.Е.

1.4. Введение в логику высказываний

Метод Вонга

Близким к методу резолюций является метод Вонга, в котором тоже используется сконструированная конъюнктивно-дизъюнктивная нормальная форма представления исходной клаузы, а аксиому порядка заменяет клауза Вонга:

X, L ⇒ X; R,

здесь X пробегает некоторые буквы, входящие в клаузу, а L и R — определенные комбинации дизъюнктов и конъюнктов.

Конструктивная процедура доказательства сводится к последовательной разбивке дизъюнктов или конъюнктов таким образом, чтобы слева и справа от метаимпликации появилась одна и та же буква X. Если в результате такой разбивки все конечные клаузы приобретают вид клаузы Вонга, то и исходная клауза была составлена верно. Разберем метод Вонга на примере доказательства справедливости правила отделения:

А, А → В ⇒ В     или     А, А ∨ В ⇒ В.

Здесь имеется только один дизъюнкт, который можно разбить на две новых клаузы:

А, А ⇒ В     и     А, В ⇒ В.

Вторая клауза удовлетворяет и аксиоме порядка и клаузе Вонга. В качестве Х в ней выступает терм В, L = А и R = 0. Первая же клауза тоже будет удовлетворять необходимым требованиям, но только после того, как терм А из левой части клаузы с противоположным знаком перенести в правую часть. Тогда будем иметь:

А ⇒ А; В     где Х = А, L = 1 и R = В.

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

X ∨ Y, (X → Y) ∨ U, Z → (Y → W) ⇒ (W → X) → (Z → X).

Приведем ее в соответствующую конъюнктивно-дизъюнктивную нормальную форму:

X ∨ Y, X ∨ Y ∨ U, Z ∨ Y ∨ W ⇒ W ∧ X; Z; X.

Далее разобьем первый дизъюнкт, в результате получим две производные клаузы:

1. X, X ∨ Y ∨ U, Z ∨ Y ∨ W ⇒ W ∧ X; Z; X ,
2. Y, X ∨ Y ∨ U, Z ∨ Y ∨ W ⇒ W ∧ X; Z; X .

Клауза (1) отбрасывается, так как она удовлетворяет клаузе Вонга. Разбивая дизъюнкт клаузы (2), получаем еще три клаузы: 

2.1. Y, X, Z ∨ Y ∨ W ⇒ W ∧ X; Z; X,
2.2. Y, Y, Z ∨ Y ∨ W ⇒ W ∧ X; Z; X,
2.3. Y, U, Z ∨ Y ∨ W ⇒ W ∧ X; Z; X.

Клаузы (2.1) и (2.2) сводятся к одной клаузе — 

2.1. Y, Z ∨ Y ∨ W ⇒ W ∧ X; Z; X.

Разобьем ее: 

2.1.1. Y, Z ⇒ W ∧ X; Z; X,
2.1.2. Y, Y ⇒ W ∧ X; Z; X,
2.1.3. Y, W ⇒ W ∧ X; Z; X.

Первые две клаузы удовлетворяют клаузе Вонга. У клаузы (2.1.3) нужно разбивать конъюнкт:

2.1.3.1. Y, W ⇒ W; Z; X,
2.1.3.2. Y, W ⇒ X; Z; X.

Теперь обе клаузы имеют вид клаузы Вонга.

Но у нас осталась еще ветвь (2.3). Она отличается от рассмотренной ветви (2.1) наичием непарного терма U, который, однако, не может повлиять на конечный результат, т.е. разбиение клаузы (2.3) практически полностью совпадает с разбиением клаузы (2.1). Следовательно, исходная клауза была записана верно.