Методику продемонстрируем на примере. Пусть требуется доказать:
.
Сначала поступают точно так же, как и по методике Вонга, только необходимо преобразовать клаузу таким образом, чтобы слева от символа Þ был ноль Æ:
Затем из дизъюнктов составляют резолюции до тех пор, пока не получится ноль.
Выпишем по порядку все посылки и далее начнем их «склеивать». Дизъюнкты можно перебирать автоматически в соответствии с возрастанием порядковых номеров. Такая стратегия поиска нуля очень непродуктивна. К решению данной задачи можно подойти творчески.
В итоге получим:
|
1. А |
5. (1; 4) |
|
2. С |
6. (2; 4) С |
|
3. |
7. (3; 5) |
|
4. |
8. (6; 7) |
В
Иначе, произведенные ранее преобразования, можно представить в следующем виде:
