Доказательства невыполнимости, основанные на принципе резолюций

Доказательства невыполнимости логических формул очень важны в ИИ (Искусственный Интеллект). Способы таких доказательств, основанные на принципе резолюций, выделяются среди прочих тем, что они дают возможность использовать средства автоматического доказательства, применяемые в логическом программировании.

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

При условии, что? S:

• 1)выбираем l, s₁ и s₂, такие что и ;
• 2) вычисляем резольвенту r;
• 3) заменяем S на S.

В качестве примера проверим невыполнимость множества:

S=.

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

• 1. .
• 2. .
• 3. .
• 4. .

Затем вычисляются и добавляются к S резольвенты. В списке, который приводится ниже, каждый дизъюнкт — резольвента некоторых из предшествующих дизъюнктов. Номера их приведены в скобках справа от соответствующей резольвенты.

• 5. (1,3).
• 6. (1,4).
• 7. (2,3).
• 8. (2,4).
• 9. (2,5).
• 10. (3,6).
• 11. (3,8).
• 12. (4,5).
• 13. (4,7).
• 14.? (4,9).

Замечание. Алгоритм проверки невыполнимости — недетерминированный, вообще говоря, возможен не один выбор для l, s₁ и s_2. В приведённом примере мы выбирали дизъюнкты s₁ и s₂ в лексикографическом порядке номеров. Такая стратегия неоптимальна. Некоторые резольвенты оказались ненужными, а также вычислялись в некоторых случаях более одного раза. Для сравнения продемонстрируем теперь применение этого же алгоритма с минимумом резолюций:

• 5. (1,4).
• 6. (2,4).
• 7. (3,6).
• 8.? (5,7).

Ясно, что принятая стратегия может значительно влиять на процесс выполнения алгоритма. Тем не менее упомянем два важных свойства, не зависящих от используемой стратегии.

Прежде всего, если множество S не содержит ни одной пары дизъюнктов, допускающих резольвенту, то оно выполнимо (разумеется, за исключением случая, когда оно содержит пустой дизъюнкт). Интерпретация I получается заданием l (p)=И тогда и только тогда, когда положительная литера p принадлежит одному из дизъюнктов множества S.

Во-вторых, если выполнение этого алгоритма закончилось «нормально» после порождения пустого дизъюнкта, то установлена невыполнимость исходного множества S. Это непосредственное следствие леммы 1.

Может случиться, что выполнение алгоритма не завершится, хотя число различных дизъюнктов, которые могут быть порождены с помощью резолюций, очевидно, конечно. Например, такое явление имеет место для множества. Резольвентный дизъюнкт q будет порождаться неограниченное число раз. Рассмотрим также случай невыполнимого множества. Оптимальная стратегия установит невыполнимость посредством построения резольвент q, а затем ?. Напротив, «неадекватная» стратегия приведёт к зацикливанию, которое только что было отмечено. Таким образом, можно констатировать, что стратегия влияет не только на эффективность алгоритма, но и на его завершаемость.

Представляет интерес свойство завершаемости метода резолюций: конечное множество S невыполнимо тогда и только тогда, когда пустой дизъюнкт может быть выведен из S с помощью резолюций. Из леммы 1 следует достаточность этого условия. Пустой дизъюнкт, будучи невыполнимым, не может быть логическим следствием из выполнимого множества дизъюнктов. Необходимость сформулированного условия приведена в следующей лемме.

Лемма (2). Если множество дизъюнктов S невыполнимо и содержит резольвенты своих элементов, то оно обязательно содержит пустой дизъюнкт. резолюция логика высказывание предикат Число различных дизъюнктов, которые можно составить на основе конечного множества S, конечно. Таким образом, лемма 2 лаёт простое общее средство решения вопроса о выполнимости или невыполнимости конечного множества дизъюнктов.

Проиллюстрируем лемму одним очень простым примером. Рассмотрим множество дизъюнктов:

S=.

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

Рис. 1.

Второй этап состоит в том, что каждому узлу N дерева сопоставляется некоторый дизъюнкт с. Этот дизъюнкт будет зависеть од дизъюнктов с ₁ и с _2, которые уже сопоставлены двум узлам, следующим за N. Две соответствующие дуги помечены двумя противоположными литерами, скажем и. Если один из дизъюнктов, например с ₁ не содержит ни, ни её отрицание, то можно выбрать с= с ₁, в противном случае с будет резольвентой для с ₁ и с ₂ по отношению к. Этот результат, полученный для множества S, иллюстрируется рисунком 2.

Рис. 2.

Заметим, что каждый узел помечен дизъюнктом, при котором ложна частичная интерпретация, соответствующая этому узлу. Таким образом, корень будет помечен пустым дизъюнктом. Наконец, по построению каждый дизъюнкт является элементом S или получен из S с помощью резолюции. Число резольвент, которые надо вычислить для установления невыполнимости множества дизъюнктов S, не больше числа невисячих узлов семантического дерева. Максимальное значение этой величины равно, где n-число различных высказываний, входящих в S. Тем самым показано, что резолюция неэффективна, если применяется только что описанная простая стратегия. Отметим, что некоторые стратегии выбора приводят к лучшим реализациям.

Лемма 2 остаётся справедливой для бесконечного S. Отсюда следует, что бесконечное множество дизъюнктов невыполнимо тогда и только тогда, когда в нём найдётся конечное невыполнимое подмножество. Приведём непосредственное следствие, отражающее свойство завершаемости принципа резолюции.

Следствие. Если множество S формул невыполнимо, то этот факт всегда можно установить методом резолюций.