Принцип резолюций. 
Системы поддержки принятия решений часть 1

В сущности, в основе принципа лежит несложная схема рассуждений. Пусть Л, В и С — формулы, и имеются два дизъюнкта: 1) (А + С) и 2) (В + С), которые мы будем считать истинными. Предположим теперь, что С — И.

Подставив это значение в первое выражение, получим дизъюнкт вида А + Я, который является истинным при любом А. Подставив С = И во второе выражение, получим дизъюнкт В + Л, из которого однозначно следует, что В = Я, поскольку принято, что весь дизъюнкт истинный.

Положим теперь С = Л. Второй дизъюнкт истинный при любом В, но первый принимает вид А лЛ, откуда следует, что А = Я.

Все это означает, что, независимо от интерпретации формулы С, — либо А, либо В истинный. Это можно отобразить в виде нового дизъюнкта (А + В), исключив контрарные формулы С и С.

Другими словами, выполняется правило.

Правило особенно эффективно, если А и В — дизъюнкты, а С — высказывание. Это правило называется правилом резолюции, а новый полученный дизъюнкт — резольвентой. Он формируется как «сумма» оставшихся формул, за исключением контрарных, т. е. разных по знаку.

Для дизъюнктов (j) + q + 7) и (т + г), например, резольвента будет иметь вид (р + с/ + т). Для дизъюнктов (р + г) и (г) соответственно (р), а вот в случае (р) и (р) обе литеры «уничтожаются». Это — пример получения пустого дизъюнкта. Еще один пример: имеются два дизъюнкта — (х + у) и (х + у). Получаемые здесь резольвенты (х + х) или (у + у) равны 1; они не несут информации, поэтому их следует отбрасывать.

В логическом плане каждый полученный дизъюнкт-резольвента равносилен обоим дизыонктам-родителям, участвовавшим в резолюции (они так и называются — родители). Он становится очередной гипотезой и участвует в резолюции на равных с другими. Это касается и пустого дизъюнкта, но, будучи поставлен в ряд гипотез Я, он делает формулу типа (3.11) равной 0, что и является ее доказательством.

Метод резолюций легко представить в виде несложного регулярного алгоритма. Это позволяет успешно применять ЭВМ для решения задач вывода, хотя и здесь возможны неожиданные трудности. Дело в том, что машина ищет резолюцию слепо, методом перебора. При таком поиске путь к результату может быть весьма долгим. Возможны также случаи простого «зацикливания» машины. Простейший пример: имеется два дизъюнкта р wp + q. При машинной реализации резольвента q может порождаться неограниченное число раз. Предусматривая подобные случаи, применяют специальные стратегии поиска резольвент и соответствующее программирование. Некоторые такие стратегии мы рассмотрим в следующем параграфе.

В заключение отметим такое важное обстоятельство: множество резольвент (вместе с родительскими дизъюнктами) образует не что иное, как математическую модель некоторой предметной области. Каждая новая резольвента добавляет новое состояние в пространство состояний МПрО, а поиск решения в пространстве состояний представлен операцией логического вывода.

Несмотря на известные недостатки, заключающиеся главным образом в возможности неограниченного порождения резольвент и в отсутствии тем самым гарантий быстрого поиска решения, метод резолюций является одном из самых мощных инструментов в решении задач логического вывода. Он обладает двумя существенными достоинствами: (1) логичен, так как резольвенты являются логическими следствиями предложений-родителей, а (2) обладает полнотой, так как в процессе вывода результат получается за счет применения только одного и того же правила. Представляет интерес свойство завершаемое™ метода резолюций: если множество {Я} невыполнимо, то пустой дизъюнкт может быть найден посредством резолюций. Это и понятно: пустой дизъюнкт есть резольвента множества {Я}, а поскольку оно невыполнимо, то он не может быть следствием выполнимого множества. По этому поводу даже есть лемма: если множество {Я} невыполнимо и содержит резольвенты своих элементов, то оно обязательно содержит пустой дизъюнкт.

Метод резолюций применяется не только в рамках исчисления высказываний и предикатов (см. далее), к нему нередко сводится процедура вывода в некоторых других моделях представления знаний (продукционные ПЗ, СС, фреймы). Широко известный язык программирования Пролог специально создан для реализации процедур, основанных на методе резолюций. Что же касается указанных недостатков, то в значительной степени они уменьшаются или даже исключаются путем применения специальной стратегии целенаправленного поиска резольвент. Ниже мы коснемся этого подробнее.

Основное назначение метода резолюций — порождение логических следствий из системы гипотез {#} (причем эта система должна быть представлена в нормальной конъюнктивной форме). Это может быть порождение с целью общего обзора следствий, или же это будет поиск пустого дизъюнкта при реализации принципа дедукции — меняется только цель. Резольвента есть логическое следствие своих родителей. Однако обратного утверждать нельзя!