Метод резолюций для ИВ. Хорновские дизъюнкты.

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

или

называется литерой. Литеры X и ¬X называются контрарными. Конъюнктом называется конъюнкция литер. Дизъюнктом называется дизъюнкция литер.
     Пусть D₁=B₁vA , D₂=B₂v¬A - дизъюнкты. Дизъюнкт B₁vB₂ называется резольвентой дизъюнктов D₁ и D₂ по литере А и обозначается через res_A(D₁,D₂). Резольвентой дизъюнктов D₁ и D₂ называется резольвента по некоторой литере и обозначается через res(D₁,D₂). Очевидно, что res(A,¬A)=0. Действительно, т.к. A=Av0 и ¬A=¬Av0, то res(A,¬A)=0v0=0. Если дизъюнкты D₁ и D₂ не содержат контрарных литер, то резольвент у них не существует.
     Пример. Если
     D₁=AvBvC, D₂=¬Av¬BvQ, то
     res_A(D₁,D₂)=BvCv¬BvQ, res_B(D₁,D₂)=AvCv¬AvQ,
     res_C(D₁,D₂) не существует.
     Утверждение. Если res(D₁,D₂) существует, то D₁,D₂+res(D₁,D₂).
     Пусть S=(D₁,D₂,…,D_n) ? множество дизъюнктов. Последовательность формул F₁,F₂,…,F_n называется резолютивным выводом из S, если для каждой формулы F_k выполняется одно из условий:
     1. F_k∈S;
     2. существуют j, k<i такие, что F_i=res(F_j,F_k).
     Теорема. (о полноте метода резолюций). Множество дизъюнктов S противоречиво в том и только в том случае, когда существует, резолютивный вывод из S, заканчивающийся 0.
     Отметим, что метод резолюций можно использовать для проверки выводимости формулы F из данного множества формул F₁,F₂,…,F_n. Действительно, условие F₁,F₂,…,F_n+F равносильно условию F₁,F₂,…,F_n,¬F├ (множество формул противоречиво), что в свою очередь равносильно условию Q├, где Q=F₁∧F₂∧…∧F_n∧(¬F). Приведем формулу Q к КНФ: Q=D₁∧D₂∧...∧D_m, тогда Q├ ⇔D₁∧D₂∧...∧D_m+ ⇔ D₁,D₂,...,D_m├. Таким образом, задача проверки выводимости F₁,F₂,…,F_n├F сводится к проверке противоречивости множества дизъюнктов S={D₁,D₂,...,D_m}, что равносильно существованию резолютивного вывода 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. res_A{¬Av¬BvC,A}=¬BvC;
         2. res_B{¬BvC,B}=C;
         3. res_D{¬Cv¬DvE,FvD}=¬CvEVF;
         4. res_E{¬CvEvF,Fv¬E}=¬CvF;
         5. res_C{C,¬CvF =F;
         6. res{F,¬F}=0.
     Итак, заключаем, что формула А→(В→F) выводима из множества формул А→(В→С), CD→Е, ¬F→D&(¬)E.
     Отметим, что метод резолюций достаточен для обнаружения возможной выполнимости данного множества дизъюнктов S. Для этого включим в множество S все дизъюнкты, получающиеся при резолютивных выводах из S. Из теоремы о полноте метода резолюций вытекает следствие: Если множество дизъюнктов S содержит резольвенты всех своих элементов, то S выполнимо тогда и только тогда, когда 0∉S.

ХОРНОВСКИЕ ДИЗЪЮНКТЫ

  На этом шаге мы рассмотрим хорновские дизънкты.
 

    Дизъюнкт - это совокупность литер, одни из которых не содержат, а другие содержат знак отрицания. Если первые записывать через точку с запятой слева от знака ":-", а вторые - без знака отрицания через запятую справа от знака ":-" и в конце каждого дизъюнкта ставить точку, то получим выражение вида:
    A₁;A₂;…;A_n:- B₁,B₂,…,B_m

    Из каждых двух дизъюнктов, представленных в таком виде, используя метод резолюций, можно получить новый дизъюнкт, являющийся следствием двух первых. Если одна и та же атомарная формула появляется в левой части одного дизъюнкта (литера без отрицания) и в правой части другого (литера с отрицанием), то новый дизъюнкт, полученный в результате слияния исходных дизъюнктов и вычеркивания повторяющейся рассматриваемой атомарной формулы, является следствием исходных дизъюнктов. При форме записи это означает вычеркивание контрарных пар, находящихся по разные стороны от знака ":-". Например, даны два дизъюнкта:
    A;B;C:-D,E,F.
    G;H:-A,M,N.
Полученный в результате их слияния и вычеркивания повторяются литеры A новый дизъюнкт:
    B;C;G;H:-D,E,F,M,N
является следствием исходных. Вычеркивание повторяющейся слева и справа от знака ":-" литеры А аналогично рассмотренномy ранее вычеркиванию контрарной пары А и ~А.

    Метод резолюций допускает сопоставление нескольких литер в левой части одного дизъюнкта с несколькими литерами в правой части другого.

    Если дизъюнкты содержат переменные, то для получения резольвенты атомарные формулы не обязательно должны быть идентичными, они должны быть лишь сопоставимыми (унифицируемыми). При сопоставлении формул происходит конкретизация значений переменных (конкретизация переменных), в результате которой формулы становятся идентичными. Например, при сопоставлении формул A(x) и A(b) происходит конкретизация переменной x, которая принимает значение, равное b.

    Хорновский дизъюнкт - это дизъюнкт, содержащий не более одной литеры без отрицания. Например:
    A:-B,C,D;
    A:-B₁,B₂,B_n.

    Приведенным хорновским дизъюнктам эквивалентны следующие формулы логики предикатов первого порядка:
    BÙCÙD ®A;
    B₁ÙB₂Ù B_n ®A
(переменные в этих формулах не указаны).

    Существует два вида хорновских дизъюнктов.

    Хорновский дизъюнкт с заголовком - это дизъюнкт, содержащий одну литеру без отрицания. Он может содержать одну или несколько литер с отрицанием или не содержать их вообще, например:
    A:-B,C, ...,D;
    A:-B;
    A:-.

    Последний из приведенных дизъюнктов можно записывать без знака ":-", то есть в виде А.

    Хорновский дизъюнкт без заголовка - это дизъюнкт, не содержащий литер без отрицания, например:
    :-B,C, ...,D;
    :- A.

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

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

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

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

    Хорновские дизъюнкты были выбраны в качестве основы для создания программных систем автоматического доказательства теорем.

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