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

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

Определение 34: Если два или более литерала (с одиниковым знаком) дизъюнкта C имеют наиболее общий унификатор s, то Cs - называется склейкой C.

Пример 17. Рассмотрим дизъюнкты:

Пусть C= P(x)Ъ P(f(y))Ъ ШQ(x).

Тогда 1 и 2 литералы имеют наиболее общий унификатор s = {f(y)/x}. Следовательно, Cs=P(f(y))Ъ ШQ(f(y)) есть склейка C.

Определение 35: Пусть C₁ и C₂ – два дизъюнкта, которые не имеют никаких общих переменных. Пусть L₁ и L₂ - два литерала в C₁ и C₂ соответственно. Если L₁ и ШL₂ имеют наиболее общий унификатор s, то дизъюнкт (C₁s - L₁s) И (C₂s - L₂s) называется резольвентой C₁ и C₂.

Пример 16:Пусть C₁= P(x)Ъ Q(x) и C₂= ШP(a)Ъ R(x). Так как x входит в C₁ и C₂, то мы заменим переменную в C₂ и пусть C₂= ШP(a)Ъ R(y). Выбираем L₁= P(x) и L₂=ШP(a). L₁ и L₂ имеют наиболее общий унификатор s={a/x}. Следовательно, Q(a)Ъ R(y) – резольвента C₁ и C₂.

Пример 17:Доказать, что формула R(a, z) выводима из множества дизъюнктов S={ШP(x, f(x))Ъ R(x, f(x), g(x)), Q(x, g(x)) Ъ R(x, f(x), g(x)), ØQ(x, g(x)) Ù P(x, f(x))}.

Пусть C₁=ШP(x, f(x))Ъ R(x, f(x), C₂= Q(x, g(x)) Ъ R(x, f(x), C₃=ØQ(x, g(x)) Ъ P(x, f(x)). Добавим к множеству S единичный дизъюнкт C₄=ШR(a, z).

Так как в дизъюнктах C₁ , C₂ , C₃ есть одинаковая переменная x, то заменим её в C₂ на y, а в C₃ на u. Таким образом, решение исходной задачи сводится к доказательству противоречивости следующего множества дизъюнктов:

C₁=ШP(x, f(x))Ъ R(x, f(x);

C₂= Q(y, g(y)) Ъ R(y, f(y);

C₃=ØQ(u, g(u)) Ъ P(u, f(u));

C₄=ШR(a, z).

Найдём резольвенту C₅ дизъюнктов C₁ и C₃ и добавим её к множеству дизъюнктов, для чего произведём унификацию переменных x и u, таким образом, что u заменим на x, и получим C₅= R(x, f(x)) Ъ ØQ(x, g(x)).

Найдём резольвенту C₆ дизъюнктов C₂ и C₅ и добавим её к множеству дизъюнктов, для чего произведём унификацию переменных y и x, таким образом, что y заменим на x, и получим C₆= R(x, f(x)) Ъ R(x, f(x))= R(x, f(x)).

Найдём резольвенту C₇ дизъюнктов C₂ и C₆ и добавим её к множеству дизъюнктов, для чего произведём замену переменной x на константу a, а переменную z заменим на функцию f(a), таким образом получим C₇= я, то есть пустой дизъюнкт.

Алгоритм метода резолюций.

Шаг 1. Если в S есть пустой дизъюнкт, то множество противоречиво (невыполнимо), иначе перейти к шагу 2.

Шаг 2. Найти в исходном множестве S такие дизъюнкты или склейки дизъюнктов C₁ и C₂, которые содержат унифицируемые контрараные литералы L₁ О C₁ и L₂ О C₂. Если таких дизъюнктов нет, то исходное множество выполнимо, иначе перейти к шагу 3.

Шаг 3. Вычислить резольвенту C₁ и C₂ и добавить ее в множество S. Перейти к шагу 1.