Помощь в написании учебных работ

Имя

1500+ квалифицированных специалистов готовы вам помочь

Выберите тип работыЧасть дипломаДипломная работаКурсовая работаКонтрольная работаРешение задачРефератНаучно - исследовательская работаОтчет по практикеОтветы на билетыТест/экзамен onlineМонографияЭссеДокладКомпьютерный набор текстаКомпьютерный чертежРецензияПереводРепетиторБизнес-планКонспектыПроверка качестваЭкзамен на сайтеАспирантский рефератМагистерская работаНаучная статьяНаучный трудТехническая редакция текстаЧертеж от рукиДиаграммы, таблицыПрезентация к защитеТезисный планРечь к дипломуДоработка заказа клиентаОтзыв на дипломПубликация статьи в ВАКПубликация статьи в ScopusДипломная работа MBAПовышение оригинальностиКопирайтингДругое

ПринимаюПолитику конфиденциальности

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

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

или

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

называется литерой. Литеры 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.