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. Метод резолюций:

  1. 2. Методи регулювання в аграрному правi
  2. 5. Правовi методи регулювання сiльського господарства
  3. Предмет і метод адміністративного права
  4. Трудова дисципліна та методи її забезпечення
  5. 4. Методи правового регулювання в АП. Імперативний та диспозитивний метод правов. Регулювання агр.. відносн
  6. 37. Форми і методи держ. регулювання сільського господарства.
  7. § 2. Метод административного права
  8. § 3. Преступления, посягающие на регламентированные международным правом средства и методы ведения воины
  9. 4.1.Методы управления
  10. Следственный осмотр документов, его задачи и методы фиксации
  11. ГАЛИЛЕЙ
  12. Галилей выделил два основных метода исследования природы:
  13. Характерні ознаки адміністративних методів державного управління:
  14. 2.3. Исчисление высказываний
  15. 2.3.3. Метод резолюций
  16. Тема 4. Автоматическое доказательство теорем
  17. 4.1. Постановка задачи