2.3.3. Метод резолюций

Методику продемонстрируем на примере. Пусть требуется доказать:

.

Сначала поступают точно так же, как и по методике Вонга, только необходимо преобразовать клаузу таким образом, чтобы слева от символа ? был ноль ?:

Затем из дизъюнктов составляют резолюции до тех пор, пока не получится ноль.

Выпишем по порядку все посылки и далее начнем их «склеивать». Дизъюнкты можно перебирать автоматически в соответствии с возрастанием порядковых номеров. Такая стратегия поиска нуля очень непродуктивна. К решению данной задачи можно подойти творчески.

В итоге получим:

1. АU В 5. (1; 4)
2. СU А 6. (2; 4) С
3. 7. (3; 5)
4. 8. (6; 7) ?

Иначе, произведенные раннее преобразования, можно представить в следующем виде:

<< | >>
Источник: Лекции - Дискретная математика. 2016

Еще по теме 2.3.3. Метод резолюций: