Продолжаем курс математической логики. В этой лекции мы более глубоко рассмотрим метод резолюций. Метод резолюций — это основной метод, который используется в математической логике для того, чтобы проверить, — являются ли некоторые утверждения логическим следствием других утверждений, посылок или гипотез. Метод резолюций сводится к очень простым преобразованиям формулы для того, чтобы проверить ее невыполнимость. Вспомним определение резольвенты. Резольвента строится для двух формул D1 и D2, представленных в виде дизъюнкций литералов. Пусть формула D1 представляет собой дизъюнкт "L или Ф1"; формула D2 представляет собой дизъюнкт "не L или Ф2". Резольвентой двух этих дизъюнктов называется дизъюнкт "Ф1 или Ф2". Оказывается, что резольвента является логическим следствием порождающих ее дизъюнктов. Для того, чтобы это доказать, можно просто проверить, что формула, представляющая собой конъюнкцию двух формул D1 и D2 и отрицание резольвенты, является невыполнимой. Приведем эту формулу, например, к дизъюнктивной нормальной форме. Мы здесь видим, что в каждом конъюнкте, в дизъюнктивной нормальной форме, содержится пара противоположных литер. Это означает, что каждый из этих конъюнктов является невыполнимым. Следовательно, и вся наша функция Ф является невыполнимой. Это говорит о том, что резольвента является логическим следствием порождающих ее дизъюнктов. Построение резольвенты является, конечно, очень простым делом. Из двух дизъюнктов, отличающихся друг от друга только тем, что в один из этих дизъюнктов входит литерал, а в другой из дизъюнктов входит отрицание литерала, — мы простым способом строим просто дизъюнкцию оставшихся частей этих двух дизъюнктов. Чрезвычайно важной является следующая теорема: если к некоторой логической функции конъюнктивно присоединить логическое следствие этой функции, то значение функции не изменится. Для доказательства возьмем две формулы A и B такие, что B является логическим следствием A. Если B является логическим следствием A, то, по определению логического следствия, на всех тех интерпретациях, на которых формула A является истинной, формула B также является истинной. Отсюда очевидно, что конъюнкция двух формул A и B в точности равносильна формуле A. Таким образом, можно видеть, что если B является логическим следствием A, то конъюнкция "A и B" равносильна формуле A. Отсюда вытекает следующее положение: если резольвенту конъюнктивно присоединить к порождающим ее дизъюнктам, то значение истинности исходной формулы не изменится. Легко видеть, что метод резолюций — это обобщение гипотетического силлогизма. Действительно, гипотетический силлогизм представляется следующим образом: из двух утверждений "Если P, то Q" и "Если Q, то S", логическим следствием этих двух утверждений является формула "Если P, то S". Представляя каждую из этих импликаций с помощью отрицания и дизъюнкции, мы видим, что да, действительно, резольвента двух дизъюнктов — это просто другая форма гипотетического силлогизма. Метод резолюции, который мы сейчас рассмотрим, используется для проверки невыполнимости формул. Для проверки невыполнимости формула представляется в конъюнктивной нормальной форме. Пусть эта формула представлена в виде конъюнкции дизъюнктов: D1, D2, Dk и так далее. Для любых двух дизъюнктов, которые содержат противоположные литеры, мы можем построить их резольвенту, а именно: дизъюнкт "Ф1 или Ф2". Поскольку резольвента двух дизъюнктов является логическим следствием порождающих ее дизъюнктов, то эту резольвенту мы можем присоединить к остальным дизъюнктам, считая, что это присоединение конъюнктивно. При этом очевидно, что значение исходной формулы, представленной в конъюнктивной нормальной форме, не изменится. Резолютивным выводом называется такая последовательность дизъюнктов D1, D2 и так далее, что последний дизъюнкт является пустым, а каждый промежуточный дизъюнкт — либо исходный, либо является резольвентой двух каких-либо предшествующих дизъюнктов. Очевидно, что если мы в результате такого вывода получим пустой дизъюнкт, то наша исходная формула является невыполнимой, поскольку пустой дизъюнкт соответствует невыполнимой формуле, а невыполнимая формула может быть логическим следствием только невыполнимой же формулы. Рассмотрим пример проверки невыполнимости логической формулы с помощью метода резолюции. Пусть наша формула F уже представлена в конъюнктивной нормальной форме. Проверим, является ли эта функция невыполнимой. Нашу проверку выполним в несколько шагов. Запишем нашу функцию как набор дизъюнктов, помня, что фактически функция является конъюнкцией всех перечисленных дизъюнктов. Среди наших дизъюнктов будем искать такие, в которые какая-либо из переменных входит с отрицанием, а в другой дизъюнкт — входит без отрицания. Например, дизъюнкт первый и дизъюнкт третий как раз соответствуют этому определению. Дизъюнкт первый: переменная X2 входит с отрицанием; дизъюнкт третий: эта переменная входит без отрицания. Поэтому можно построить резольвенту первого и третьего дизъюнкта, а именно: дизъюнкт "X1 или не X3" и конъюнктивно присоединить этот дизъюнкт к перечисленным выше дизъюнктам. Иными словами, по свойству резольвенты наша новая формула, а именно: конъюнкция всех прежних дизъюнктов и конъюнкция нашей резольвенты, равносильна исходной формуле. На следующих шагах будем искать другие возможные резольвенты. А именно: резольвентой дизъюнктов седьмого и пятого является дизъюнкт, содержащий одну переменную X1. Резольвентой второго и восьмого дизъюнкта является дизъюнкт, содержащий только переменную X2. Присоединяя конъюнктивно эти резольвенты к порождающим их дизъюнктам, мы можем быть уверены, что конъюнкция всех этих дизъюнктов равносильна исходной формуле. Через несколько шагов мы получаем пустую резольвенту. Пустая резольвента соответствует невыполнимой формуле, то есть формуле, которая тождественно равна нулю. Присоединив пустую резольвенту к порождающим ее дизъюнктам, мы получаем невыполнимую функцию, которая равносильна исходной функции. Следствием этого является следующее утверждение: наша исходная функция является невыполнимой. Можно утверждать, что любая формула F невыполнима тогда и только тогда, когда она имеет пустую резольвенту.
