Главная   Онлайн инструменты по математической логике   Мат. логика теория   Как считает компьютер?   Схемы для ЭВМ    

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

Определение булевой функции
Элементарные булевы функции
Задание булевых функций посредством элементарных
Существенные и несущественные переменные
Эквивалентные функции
Основные эквивалентности
Функциональная полнота
Нормальные формы
Совершенные нормальные формы
Минимизация ДНФ методом Квайна
Карты Карно
Полином Жегалкина
Высказывания
Предикаты
Кванторы
Определение формальной теории
Исчисление высказываний
Теорема о дедукции. Полнота ИВ
Автоматическое доказательство теорем
Метод резолюций в ИВ
Определение алгоритма
Машина Тьюринга
Рекурсивные функции
Алгоритмически неразрешимые задачи
Алгоритмы и их сложности



     Напомним, что если 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.

@ 2010 - 2017 tablica-istinnosti.ru Рейтинг@Mail.ru