Метод резолюций в ИВ

Напомним, что если X — логическая переменная, а σ∈{0,1} то выражение

Xσ = { x если σ=1
¬x если σ=0

или

Xσ = { 1 если x=σ
0 если x≠σ

называется литерой. Литеры X и ¬X называются контрарными. Конъюнктом называется конъюнкция литер. Дизъюнктом называется дизъюнкция литер.

Пусть D1=B1vA , D2=B2v¬A — дизъюнкты. Дизъюнкт B1vB2 называется резольвентой дизъюнктов D1 и D2 по литере А и обозначается через resA(D1,D2). Резольвентой дизъюнктов D1 и D2 называется резольвента по некоторой литере и обозначается через res(D1,D2). Очевидно, что res(A,¬A)=0. Действительно, т.к. A=Av0 и ¬A=¬Av0, то res(A,¬A)=0v0=0. Если дизъюнкты D1 и D2 не содержат контрарных литер, то резольвент у них не существует.

Пример. Если

D1=AvBvC, D2=¬Av¬BvQ, то

resA(D1,D2)=BvCv¬BvQ, resB(D1,D2)=AvCv¬AvQ,

resC(D1,D2) не существует.

Утверждение. Если res(D1,D2) существует, то D1,D2+res(D1,D2).

Пусть S=(D1,D2,…,Dn) ? множество дизъюнктов. Последовательность формул F1,F2,…,Fn называется резолютивным выводом из S, если для каждой формулы Fk выполняется одно из условий:

1. Fk∈S;

2. существуют j, k<i такие, что Fi=res(Fj,Fk).

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

Отметим, что метод резолюций можно использовать для проверки выводимости формулы F из данного множества формул F1,F2,…,Fn. Действительно, условие F1,F2,…,Fn+F равносильно условию F1,F2,…,Fn,¬F├ (множество формул противоречиво), что в свою очередь равносильно условию Q├, где Q=F1∧F2∧…∧Fn∧(¬F). Приведем формулу Q к КНФ: Q=D1∧D2∧…∧Dm, тогда Q├ ⇔D1∧D2∧…∧Dm+ ⇔ D1,D2,…,Dm├. Таким образом, задача проверки выводимости F1,F2,…,Fn├F сводится к проверке противоречивости множества дизъюнктов S={D1,D2,…,Dm}, что равносильно существованию резолютивного вывода 0 из S.

Пример. Проверить методом резолюций соотношение А→(В→С), CD→Е, ¬F→D&(¬)E ├ А→(В→F).

Согласно утверждению надо проверить на противоречивость множество формул S = {А→(В→С), CD→Е, ¬F→D&(¬)E, ¬(А→(В→F))}.

Приведем все формулы из S к КНФ:

S={¬Av¬BvC,¬(CD)vE,FvD¬E,¬(¬Av¬BvF)}={¬Av¬BvC,¬Cv¬DvE,(FvD)(Fv¬E),AB¬F}.

Таким образом, получаем множество дизъюнктов S={¬Av¬BvC,¬Cv¬DvE,FvD,Fv¬E,A,B,¬F}

Построим резолютивный вывод из S, заканчивающийся 0:

1. resA{¬Av¬BvC,A}=¬BvC;

2. resB{¬BvC,B}=C;

3. resD{¬Cv¬DvE,FvD}=¬CvEVF;

4. resE{¬CvEvF,Fv¬E}=¬CvF;

5. resC{C,¬CvF =F;

6. res{F,¬F}=0.

Итак, заключаем, что формула А→(В→F) выводима из множества формул А→(В→С), CD→Е, ¬F→D&(¬)E.

Отметим, что метод резолюций достаточен для обнаружения возможной выполнимости данного множества дизъюнктов S. Для этого включим в множество S все дизъюнкты, получающиеся при резолютивных выводах из S. Из теоремы о полноте метода резолюций вытекает следствие: Если множество дизъюнктов S содержит резольвенты всех своих элементов, то S выполнимо тогда и только тогда, когда 0∉S.