Метод Вонга

В этом методе используется сконструированная конъюнктивно - нормальная форма:

X,L ® X;R

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

Для того, чтобы придти к такому виду выражения, необходимо выполнить ряд условий:

1. Замена импликации в строке на ДНФ:

2. Избавление от знака отрицания « ù » переносом из одной части строки в другую.

3. Расщепление на строки (левой и правой части строки Вонга).

4. Замена логических связок на «,» (правило перечисления).

5. Критерий доказательства вывода. В результате освобождения строки Вонга от логических связок имеем ⊦ , т.е. строка Вонга имеет вид:

⊦ .

Если в левом списке и правом списке найдутся одинаковые переменные, то из P выводимо S (P ⊦. S).

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