Идея алгоритма унификации

Чтобы унифицировать две формулы, т.е. привести их к абсолютно идентичному виду, применяют подстановки. Переменные, которые стоят на одних и тех же позициях, заменяют на соответствующие им подформулы. Для этого обе формулы просматриваются параллельно в соответствии с их структурами; находятся совпадающие операции, а несовпадающие – ликвидируются за счет подстановок. Унификация оказывается невозможной, если в разных формулах на одном и том же месте оказываются разные операции.

Замечание: с помощью подстановок нельзя заменять константы, а также заменять переменную на формулу, зависящую от этой же переменной.

Использование унификации для применения теорем

Алгоритм унификации можно использовать, чтобы автоматизировать процесс применения некоторой теоремы к некоторой формуле.

Пусть имеется формула F и теорема Т: Е⊢Н. Чтобы применить T к F выполняется унификация E и F. Затем те же подстановки применяются правой части теоремы. Результат есть результат применения T к F.

Пример: F = (x®(y®x))

Т: ((P®Q)®R)⊢(Q®R)

Þ Замена: S(x, P®Q)

Произведя замену S(R, y®(P®Q)), получим окончательный результат:

(x®(y®x)) ⊢ (Q®( y®(P®Q))) – это есть новая теорема.

Замечание: при унификации формулы, конечно, меняются (это не тождественное преобразование). Унификация – это всего лишь способ подогнать формулы так, чтобы было возможно применить теорему;

Системы, основанные на методе резолюций

В них не используется напрямую логический вывод формальной системы. В этих системах вывод основан на принципе доказательства от противного.

Практическая организация доказательства по принципу резолюции

преобразования:

a) Приведение формулы к предваренной нормальной форме.

b) Избавление от кванторов существования:
«$» можно отбросить, заменив все вхождения связываемой переменной на константу ($x A(x) Þ A(c)).

c) Все кванторы «$» удаляются по порядку, после чего все кванторы «"» просто отбрасываются.

d) Замена всех операций на &, Ú и Ø.

e) Опускание отрицаний по законам Де Моргана.

f) По закону AÚ(B&C) = (AÚB)&(AÚC) получаем КНФ.

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