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

После появления ЭВМ метод, основанный на теореме Эрбрана, был использован для практической проверки об-щезначимости формул (путем проверки невыполнимости их отрицаний). Практика показала, что данный метод подходит только для проверки относительно простых формул. При усложнении формул множество основных примеров, кото-рые необходимо проверять, быстро растет и проверка стано-

вится технически невозможной. Алгоритм их проверки, ос-нованный на применении теоремы Эрбрана (и, соответст-венно, семантических деревьев), улучшали, однако недо-пустимо большой объем проверок по-прежнему сохранялся, поскольку сохранялся основной принцип - проверка всех возможных Н - интерпретаций.

Для того, чтобы избежать этого, стали использовать процедуры, в которых невыполнимость доказывается путём построения логического вывода из исходного множества дизъюнктов S пустого дизъюнкта или (что логически экви-валентно) некоторого дизъюнкта D_i и его отрицания ØD_i. Такие процедуры, в отличие от перебора интерпретаций, называют формульными.

Определение. Пустым называется дизъюнкт, не со-держащий литер. Его принято обозначать через ÿ.

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

Наиболее мощной из всех предложенных процедур данного типа является метод резолюций, предложенный Ро-бинсоном в 1965 г.

6.5.1. Метод резолюций в исчислении высказываний

Рассмотрим применение метода резолюций к мно-жествам дизъюнктов S, состоящим только из простых логи-ческих переменных, т.е. являющихся формулами ИВ.

Определение. Принципом резолюции называют сле-дующее правило вывода:

AÚB,Ø AÚC

BÚC

Дизъюнкт BÚC называется резольвентой дизъюнктов AÚB и Ø AÚC.

Смысл принципа резолюции в том, что он сохраняет свойство невыполнимости. Т.е., добавление нового дизъ-юнкта BÚ C к исходному множеству { A Ú B, Ø A Ú C } не приводит к появлению новых случаев невыполнимости при тех же логических значениях их составляющих A, B, C.

Определение. Рассмотрим множество дизъюнктов S. Резолютивным выводом С из S называется конечная после-довательность дизъюнктов С₁ , С₂ ,...,С_k, такая, что С_k = С и каждый С_i (1 £ i £ k) либо принадлежит S либо является резольвентой С₁ , С₂ ,..., С_i-1.

Особенность резолютивного вывода в том, что он, в отличие от обычного вывода в формальных логиках, дока-зывает не тавтологичность, а невыполнимость формул.

Невыполнимость множества дизъюнктов S будет дока-зана, если из S построен вывод пустого дизъюнкта ÿ.

Пример 1. Доказать при помощи метода резолюций невыполнимость множества дизъюнктов S={P, Q, ØPÚ ØQ}.

Решение. 1) резольвента P и ØPÚØQ равна ØQ, 2) резоль-вента Q и ØQ равна ÿ. Следовательно, построен резолютив-ный вывод {P, ØP ÚØQ, ØQ, ÿ} пустого дизъюнкта из S, что доказывает невыполнимость S.

Обозначая применение правила резолюции в виде па-ры ребер, соединяющих исходные дизъюнкты с их резоль-вентой, резолютивный вывод можно изобразить в виде де-рева вывода. В Примере 1 дерево вывода дано на Рис.3.26.