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

Урок о семантике логики высказываний показал, что общезначимость и выполнимость разрешимы с помощью таблицы истинности ценой, которая удваивается с каждой переменной, и обещал методы, не требующие её перебора. Урок о семантическом следовании и эквивалентности свёл всякое следование к невыполнимости: $\Gamma \models \varphi$ тогда и только тогда, когда $\Gamma \cup \{\neg\varphi\}$ невыполнимо. Уроки о нормальных формах и об их алгоритме дали всякой формуле конъюнктивную форму, общезначимость которой видна с первого взгляда, а выполнимость не видна. Если это так, недостаёт процедуры, которая решала бы вопрос о невыполнимости конъюнкции дизъюнктов, действуя на самих дизъюнктах. Такая процедура есть резолюция, предложенная Джоном Аланом Робинсоном в 1965 году на основе идей Мартина Дэвиса и Хилари Патнэма (1960); она составляет ядро программ, которые сегодня решают вопрос о выполнимости формул с миллионами переменных. В отличие от системы раздела о выводе, отношения которой с семантикой изучают уроки о корректности и полноте и о теореме компактности, резолюция не выводит заключений: она опровергает множества. Этот урок доказывает, что она делает это корректно и полно.

Как и в предыдущих уроках, $p$, $q$, $r$, $s$ и $t$ обозначают переменные от $v_1$ до $v_5$; буква $v$ без индекса, а также $w$ обозначают оценки; и $V(\varphi)$ есть множество переменных формулы $\varphi$.

Дизъюнкты и множества дизъюнктов

Напомним из урока о нормальных формах, что литерал есть переменная или отрицание переменной и что противоположный литералу $\ell$ литерал, записываемый $\ell^{*}$, есть литерал той же переменной с другим знаком; два противоположных литерала образуют контрарную пару. По лемме об отрицании литерала $v(\ell^{*}) = 1 - v(\ell)$ для всякой оценки $v$. Там дизъюнкт был дизъюнкцией литералов; здесь удобно забыть порядок и повторения, которые не меняют значения, и оставить только множество.

Дизъюнкт есть конечное множество литералов. Дизъюнкт без литералов называется пустым дизъюнктом и обозначается $\Box$. Оценка $v$ выполняет дизъюнкт $C$, что записывается $v \models C$, если некоторый литерал из $C$ принимает значение $1$ при $v$; в противном случае $v$ его опровергает. Дизъюнкт из одного литерала называется единичным. Переменные дизъюнкта образуют множество $V(C)$; переменные множества $S$ дизъюнктов образуют множество $V(S)$, объединение предыдущих. Оценка выполняет множество $S$ дизъюнктов, $v \models S$, если она выполняет каждый его дизъюнкт; $S$ выполнимо, если его выполняет некоторая оценка, и невыполнимо в противном случае. Наконец, если $S$ есть множество дизъюнктов, а $C$ есть дизъюнкт, то $S \models C$ означает, что всякая оценка, выполняющая $S$, выполняет $C$.

Из определения следуют два крайних случая, которые стоит зафиксировать. Пустой дизъюнкт не имеет литералов; поэтому ни один его литерал не принимает значения $1$, и ни одна оценка его не выполняет: $\Box$ невыполним, и всякое множество, которое его содержит, тоже. Пустое множество дизъюнктов, напротив, не имеет дизъюнктов, которые нужно выполнить, и всякая оценка его выполняет. Их не следует путать: $\{\Box\}$ невыполнимо, а $\emptyset$ выполняется всеми оценками.

Дизъюнкт, содержащий контрарную пару, называется тавтологичным: он не налагает никакого условия, и его можно удалить из любого множества, не меняя моделей этого множества. Записывать дизъюнкты как множества не прихоть обозначений. Если из $(p \vee q)$ и $(p \vee \neg q)$ хотят получить $p$, дизъюнкция даёт $(p \vee p)$, которая эквивалентна $p$, но не является той же формулой; с множествами $\{p\} \cup \{p\} = \{p\}$, и слияние повторяющихся литералов происходит само собой.