7. Алгоритмы проверки общезначимости и противоречивости в ив

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

1. Алгоритм Квайна. Напомним, что формула φ от пропозициональных переменных А₁, А₂, …, А_k, является тождественно истинной, общезначимой или (что то же самое) доказуемой, если булева функция f_φ : {0, l}^k  {0,1}, соответствующая формуле φ, тождественно равна 1. Для проверки значений функции f_ используется так называемое семантическое дерево, т. е. бинарное корневое дерево, удовлетворяющее следующим условиям:

• каждое ребро помечено литерой ;

• литеры, выходящие из одной вершины, контрарны: A_i, A_i,

• ребра соответствуют литере одной и той же пропозициональной переменной А_i тогда и только тогда, когда они находятся на одинаковом расстоянии от корня (рис. 1).

Рис. 1

Семантическое дерево имеет 2^k висячих вершин и для проверки общезначимости необходимо пройти 2^к маршрутов от корня до этих вершин.

Алгоритм Квайна позволяет проходить не все семантическое дерево, а только его часть. Он состоит в том, что пропозициональным переменным А_i, упорядоченным в набор (Α₁,Α₂,··· A_k), последовательно придаются значения 0 и 1 и анализируются таблицы истинности формул, содержащих меньшее число переменных.

Пример 1. Проверить общезначимость формулы =(((АВ)С)(АВ))(АС).

Упорядочим пропозициональные переменные в набор (А, В, С). Придадим первой переменной А значение f(A) = 1. Тог да формула φ преобразуется следующим образом: (((1В)С)(1В))(1С)  ((ВС)В)С. В полученной формуле переменной В придадим значение f(B) = 1. Тогда преобразованная формула примет вид ((1С)1)С  СС т. е. будет общезначимой. В случае f(B) = 0 имеем ((0С)0)С 0С, что также общезначимо. Рассмотрим теперь случай f(A) = 0. Имеем (0,B,C) = (((0В)С)(0В))(0С) 11 1 = 1. Таким образом, все возможные случаи приводят к тождественно истинным формулам. Следовательно, формула φ тождественно истинна. На рис. 2, изображено семантическое дерево, соответствующее формуле , а на рис. 3 ― часть семантического дерева, которая фактически использовалась для проверки общезначимости.

Рис. 2

Рис. 3

2. Алгоритм редукции решает ту же задачу проверки общезначимости формулы, но используется в том случае, когда в формуле содержится достаточно много импликаций. Идея алгоритма состоит в попытке нахождения значений пропозициональных переменных формулы φ, при которых значение функции f_ равно 0, на основе того, что импликация является ложной в том и только в том случае, когда посылка истинна, а заключение ложно.

Пример 2. Проверить тождественную истинность формулы φ = ((АВ)С)(А(ВС)).

Предположим, что формула φ ложна при некотором наборе значений переменных А, В, С. Тогда истинностная функция f по этим значениям переменных дает следующие значения формул: f((АВ)С) = 1, f(А(ВС)).=0. Тогда из второго равенства получаем f(А) = 1, f(BС) =0, откуда имеем f(В) = 1, f(С) = 0. Однако при этих значениях справедливо f((АВ)С) = 0. Получили противоречие. Таким образом, формула φ тождественно истинна.

3.Метод резолюций в ИВ. Пусть - дизъюнкты. Дизъюнкт называется резольвентой дизъюнктов D₁ и D₂ no литере А и обозначается через res_A(D₁,D₂). Резольвентой дизъюнктов D₁ и D₂ называется их резольвента по некоторой литере и обозначается через res(D₁,D₂)., res (А,А)= 0. В последнем случае нуль будет отождествляться с формулой ΑΑ. Если дизъюнкты D₁ и D₂ не содержат контрарных литер, то резольвент у них не существует.

Пример 3. Если D₁=ABC, D₂=ABD. res_A(D_1,D₂)=BCBD, res_B(D_1,D₂)=ACAD, res_C(D_1,D₂) не существует.

Предложение 1. 1. Если резольвента res(D_1,D₂) существует и не равна нулю, то секвенция D_1,D_2├res(D_1,D₂) доказуема.

2. Если резольвента res(D_1,D₂) равна нулю, то доказуема секвенция D_1,D_{2├ .}.

Доказательство п.2 очевидно в силу доказуемости секвенции А,А├, где А=D₁, А = D₂. Для доказательства п. 1 рассмотрим дизъюнкты и их резольвенту res{D₁,D₂) = . Следующее дерево устанавливает доказуемость секвенции D_1,D_2├res(D_1,D₂):

Пусть S = {D₁,D₂,..., D_m} ― множество дизъюнктов. Последовательность формул φ₁,φ₂,..., φ_n называется резолютивным выводом из множества S, если для каждой формулы φ_i (i = 1,... ,n) выполняется какое-то из следующих условий:

• φ_i S;

• существуют j,k < i такие, что φ_i = res(_j,_k).

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

Доказательство. Противоречивость множества S при наличии резолютивного вывода нуля вытекает из предложения 1. Существование резолютивного вывода нуля из противоречивого множества дизъюнктов выходит за рамки курса.

Отметим, что метод резолюций можно использовать для проверки выводимости формулы φ из данного множества формул ₁,…,_n. Действительно, условие ₁,…,_n├ равносильно условию ₁,…,_n φ├, что в свою очередь равносильно условию ├, где ψ =₁…_n φ. Приведем формулу ψ к ΚΗΦ:  = D₁…D_m, тогда

├ D₁…D_{m├ } D₁,…,D_m├.

Таким образом, задача проверки выводимости φ₁,... ,φ_n\- φ сводится к проверке противоречивости множества дизъюнктов S = { D₁,…,D_m }, что равносильно существованию резолютивного вывода 0 из S.

Пример 4. Проверить методом резолюций доказуемость секвенции A(BC), CDE, FDE├ A(DF).

Согласно утверждению выше нужно проверить на противоречивость множество формул

S = {A(BC), CDE, FDE,( A(DF))}. Приведем все формулы из S к КНФ: S~ {ABC, CDE, FDE, (ABF)} ~ {ABC, CDE, (FD)(FE), ABF}. Отсюда получаем множество дизъюнктов ={ABC, CDE, (FD), FE, A,B,F}.

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

1. res_А (ABC,A) = BC;

2. res_B(BC,B) = C;

3. res_D(CDE, FD) = CEF;

4. res_Е(CEF , FE) = CF;

5. res_C(CCF) = F;

6. res(F,F) = 0.

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

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

Следствие. Если множество S' состоит из всех элементов множества дизъюнктов S, а также всевозможных резольвент всех своих элементов, то S выполнимо тогда и только тогда, когда 0 S'.

Двойственным к правилу резолюций является правило согласия. Пусть K₁= K₁A, K₂= K₂¬A — конъюнкты. Положим (K₁,K₂₎= K₁ K₂, (A,¬A)=1.

Аналогично задается вывод: пусть S = {Κ₁,Κ₂, ..., К_m}― множество конъюнктов. Последовательность формул φ₁, φ₂, ..., φ_n называется выводом из множества S по правилу согласия, если для каждой формулы φ_i (i = 1,... ,n) выполняется какое-то из следующих условий:

• φ_i S;

• существуют j,k < i такие, что φ_i = (_j,_k).

Теорема 4. Множество конъюнктов S = {Κ₁,Κ₂, ..., К_т} общезначимо (т.е. выполняется ├ Κ₁Κ₂ ... К_т ) тогда и только тогда, когда существует вывод из S по правилу согласия, заканчивающийся символом 1.

4.Метод резолюций для хорновских дизъюнктов.

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

Дизъюнкт D называется хорновским, если он содержит не более одной позитивной литеры.

Пример.5. Хорновскими дизъюнктами являются следующие дизъюнкты: ¬А¬В¬СЕ, ¬А¬С, ¬А, Е.

В общем случае хорновские дизъюнкты имеют вид ¬А₁…¬А_n В (что эквивалентно формуле (А₁…А_n )В ) или ¬А₁…¬А_n. Хорновский дизъюнкт вида ¬А₁…¬А_n В называется точным. При этом переменные Α₁,...,Α_n называются фактами, а переменная В ― целью. Хорновский дизъюнкт вида ¬А₁…¬А_n называется негативным. Дизъюнкт D = В называется унитарным позитивным дизъюнктом.

Если S ― множество хорновских дизъюнктов, то невыполнимость множества S проверяется следующим образом. Выбираем в S унитарный позитивный дизъюнкт Ρ и дизъюнкт D из S, содержащий ¬Ρ. После этого заменяем S на {S\{D}){геs(D,Р)} и продолжаем процесс до тех пор, пока S не будет содержать 0 или не найдется дизъюнктов P и D указанного вида. Если на заключительном шаге множество дизъюнктов будет содержать 0, то исходное множество S противоречиво, в противном случае S непротиворечиво.

Пример 6. Проверить на противоречивость множество дизъюнктов S = {Р ¬R¬T, Q, R, T¬P¬R, T¬Q, ¬P¬Q¬R}.

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

№ шага	Р ¬R¬T	Q	R	T¬P¬R	T¬Q	¬P¬Q¬R
1	Р ¬R¬T	Q	R	T¬P¬R	T	¬P ¬R
2	P¬T	Q	R	T¬P	T	¬P
3	P	Q	R	T¬P	T	¬P
4						0

На шаге 4 получаем 0, являющийся резолютивным выводом из S. Следовательно, множество S невыполнимо.

Логические задачи

Аппарат исчислений высказываний позволяет решать так называемые "логические" задачи. При этом самым трудным моментом является построение "модели" задачи, т. е. выделение элементарных высказываний и сведение задачи к проверке некоторых свойств высказываний, возникающих из условий задачи.

Пример 1. На следствии по делу о похищении автомобиля были допрошены четыре гангстера ― Андре, Боб, Стив, Том. Андре сказал, что машину похитил Боб, Боб утверждал, что виноват Том. Том заверил следователя, что Боб лжет. Стив настаивал, что автомобиль угнал не он. Следователю удалось установить, что только один из гангстеров сказал правду. Кто похитил автомобиль?

Решение. Обозначим высказывания "Андре украл", "Боб украл", "Стив украл", "Том украл" через А, В, S и T соответственно. Тогда показания гангстеров имеют вид В, Т, ¬Т, ¬S. Поскольку секвенция ├Т¬T доказуема, или, что тоже самое, формула Т¬T тождественно истинна, то одно из утверждений ― Τ или ¬Т обязательно истинно. Значит, Андре и Стив сказали ложь. Так как утверждение Стива "¬S" ложно, то автомобиль украл Стив.