Дискретная математика

Раздел 1. Математическая логика

Тема 1. Логика высказываний

Тема 2. Булевы функции

Тема 3. Логика предикатов

Тема 4. Метод резолюций

Тема посвящена рассмотрению метода доказательства того, что формула G является логическим следствием формул F1,F2,...,Fk, который называется методом резолюций. Отметим, что задача о логическом следствии сводится к задаче о выполнимости. Действительно, формула G есть логическое следствие формул F1,F2,...,Fk тогда и только тогда, когда множество формул {F1,F2,...,Fk,ØG} невыполнимо. Метод резолюций, если говорить более точно, устанавливает невыполнимость. Это первая особенность метода. Вторая особенность метода состоит в том, что он оперирует не с произвольными формулами, а с дизъюнктами (или элементарными дизъюнкциями).

§1. Метод резолюций в логике высказываний

Рассмотрим вначале логику высказываний. Напомним, что литералом мы называли атомарную формулу или ее отрицание, дизъюнктом – дизъюнкцию литералов. Дизъюнкт может состоять из одного литерала. На дизъюнкт мы иногда будем смотреть, как на множество литералов, т.е. не будем различать дизъюнкты, которые получаются один из другого с помощью коммутативности и ассоциативности дизъюнкции, а также идемпотентности. Последнее означает, например, что дизъюнкты XÚØYÚX и XÚØY равны. Нам понадобится особый дизъюнкт – пустой, т.е. дизъюнкт, не содержащий литералов. Его мы будем обозначать "квадратиком" □. Будем считать, что пустой дизъюнкт ложен при любой интерпретации. Это означает, что формула F&□ равносильна □, а формула FÚ□ равносильна F. Пустой дизъюнкт есть фактически то же самое, что и атомарная формула 0, но в контексте метода резолюций принято использовать □.


Определение. Литералы L и ØL называются противоположными.


Метод резолюций в логике высказываний основан на правиле резолюций.


Определение. Правилом резолюций в логике высказываний называется следующее правило: из дизъюнктов ХÚF и ØXÚG выводим дизъюнкт FÚG.

Например, из дизъюнктов ØXÚYÚZ и XÚØY выводим дизъюнкты YÚZÚØY. Обратим внимание на то, что в первых двух дизъюнктах есть еще одна пара противоположных литаралов. Условимся, что можно применять правило резолюций не обязательно к самым левым литералам (поскольку мы не различаем дизъюнкты, отличающиеся порядком записи литералов). Тогда правило резолюций, примененное к Y и ØY, даст ØXÚZÚX. Условимся еще о следующем: в дизъюнктах не писать повторяющиеся литералы и не писать □, если есть другие литералы.


Определение. Пусть S – множество дизъюнктов. Выводом из S называется последовательность дизъюнктов


D,D2,...,Dn


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

Например, если S={ØXÚYÚZ, ØYÚU, X}, то последовательность D1=ØXÚYÚZ, D2=ØYÚU, D3=ØXÚZÚU, D4=X, D5=ZÚU – вывод из S. Дизъюнкт ZÚU выводим из S.


Применение метода резолюций основано на следующем утверждении, которое называется теоремой о полноте метода резолюций.


Теорема 4.1. Множество дизъюнктов логики высказываний S невыполнимо тогда и только тогда, когда из S выводим пустой дизъюнкт.


Доказательство. Докажем вначале достаточность.

Отметим, что правило резолюций сохраняет истинность. Это означает, что если j(ØXÚF)=1 и j(XÚG)=1 для некоторой интерпретации j, то j(FÚG)=1. Действительно, пусть j(ØXÚF)=1 и j(XÚG)=1. Тогда если j(F)=1, то и j(FÚG)=1. Если же j(F)=0, то j(ØX)=1, поскольку j(ØXÚF)=1. Но в этом случае j(X)=0 и j(G)=1, так как j(XÚG)=1. Если же j(G)=1, то и j(FÚG)=1.

Пусть из S выводим пустой дизъюнкт. Предположим противное: множество S выполнимо, т.е. существует интерпретация y, при которой все дизъюнкты из S истинны. Выводимость пустого дизъюнкта из S означает, что существует последовательность дизъюнктов D1,…,Dn=□, каждый дизъюнкт которой принадлежит S или получается из предыдущих по правилу резолюций. Если дизъюнкт Dj из этой последовательности принадлежит S, то по предположению y(Dj)=1. Если же он получается из предыдущих по правилу резолюций, то также y(Dj)=1, поскольку правило резолюций сохраняет истинность. При i=n получаем, что y(□)=1. Противоречие показывает, что предположение о выполнимости множества S – ложное предположение. Следовательно, S невыполнимо. Достаточность доказана.

Докажем необходимость. Доказательство проведем индукцией по следующему параметру: d(S)=сумма числа вхождений литералов в дизъюнкты из S минус число дизъюнктов.

Пусть множество дизъюнктов S невыполнимо. Если пустой дизъюнкт принадлежит S, то он выводим из S (вывод в этом случае состоит из одного пустого дизъюнкта) и необходимость теоремы доказана. Будем считать в силу этого, что □ÏS. При этом предположении каждый дизъюнкт содержит хотя бы один литерал и поэтому d³1.

База индукции: d(S)=1. Если d(S)=1, то все дизъюнкты состоят из одного литерала. Поскольку множество S невыполнимо, то в нем должна найтись пара противоположных литералов X и ØX. В таком случае пустой дизъюнкт выводим из S, соответствующий вывод содержит три дизъюнкта: X, ØX, □.

Шаг индукции: d(S)>1. Предположим, что для любого множества дизъюнктов Т такого, что d(Т)<d(S) необходимость теоремы доказана. Пусть


S={D1,D2,…,Dk-1,Dk}.


Так как d(S)>1, то в S существует хотя бы один неодноэлементный дизъюнкт. Будем считать, что это дизъюнкт Dk, т.е. Dk=LÚDk′, где L – литерал и Dk¹□. Наряду с множеством дизъюнктов S рассмотрим еще два множества дизъюнктов


S1={D1,D2,…,Dk-1,L},

S2={D1,D2,…,Dk-1,Dk/}.


Ясно, что S1 и S2 невыполнимы и что d(S1)<a(S) и d(S2)<a(S). По предположению индукции из S1 и S2 выводим пустой дизъюнкт. Пусть


A1,A2,…,Ai,…,Al-1,Al=□                    (1)


вывод пустого дизъюнкта из S1 и


B1,B2,…,Bj,…Bm-1,Bm=□                  (2)


вывод пустого дизъюнкта из S2. Если в первом выводе не содержится дизъюнкта L, то эта последовательность дизъюнктов будет выводом из S и необходимость теоремы доказана. Будем считать, что L содержится в первом выводе, пусть Ai=L. Аналогично предполагаем, что Bj=Dk′.

Если дизъюнкт Е получается из дизъюнктов Е1 и Е2 по правилу резолюций, то будем говорить, что Е непосредственно зависит от Е1 (и от Е2). Транзитивное замыкание отношения непосредственной зависимости назовем отношением зависимости (Другими словами, E зависит от Е/, если существуют дизъюнкты Е1,…,Еn такие, что E=E1,…,En=E/ и Е1 непосредственно зависит от Е2,…,En-1 непосредственно зависит от En). Преобразуем второй вывод следующим образом: к дизъюнкту Bj и всем дизъюнктам, которые от него зависят, добавим литерал L. Новая последовательность дизъюнктов


B1,B2,…,Bj/=Dk/ÚL, B/j+1 ,…,Bm/                    (3)


будет выводом из S. Если дизъюнкт Bm не зависит от Bj, то Bm/ =□. Это означает, что из S выводим пустой дизъюнкт и необходимость теоремы доказана. Предположим, что Bm зависит от Bj. Тогда Bm/=L. Преобразуем теперь первый вывод: на место дизъюнкта Ai (равного L) в этой последовательности подставили последовательность (3). Получим последовательность


A1,…,Ai-1,B1,…,Bj/,B/j+1,…,Bm/=L,Ai+1,…,Al=□.


Эта последовательность является выводом пустого дизъюнкта из множества дизъюнктов S. Следовательно, если множество S невыполнимо, то из S выводим пустой дизъюнкт.

Теорема доказана.


Для доказательства того, что формула G является логическим следствием множества формул F1,…,Fk метод резолюций применяется следующим образом. Сначала составляется множество формул T={F1,…,Fk,ØG}. Затем каждая из этих формул приводится к конъюнктивной нормальной форме и в полученных формулах зачеркиваются знаки конъюнкции. Получается множество дизъюнктов S. И, наконец, ищется вывод пустого дизъюнкта из S. Если пустой дизъюнкт выводим из S, то формула G является логическим следствием формул F1,…,Fk. Если из S нельзя вывести □, то G не является логическим следствием формул F1,…,Fk.

Проиллюстрируем сказанное на примере. Покажем, что формула G=Z является логическим следствием формул F1=ØXÚY®X&Z, F2=ØY®Z. Сформируем множество формул T={F1,F2,ØG}. Приведем формулы F1 и F2 к КНФ (формула ØG сама имеет эту форму). Мы получим, что


F1 равносильна X&(ØYÚZ),

F2 равносильна (YÚZ).


Тогда множество дизъюнктов S равно


{X, ØYÚZ, YÚZ, ØZ}.


Из множества S легко выводится пустой дизъюнкт:


ØYvZ, ØZ, ØY, YÚZ, У, □.


Следовательно, формула G является логическим следствием формул F1, и F2.

§2. Подстановка и унификация

§3. Метод резолюций для логики первого порядка

§4. Эрбрановский универсум множества дизъюнктов

§5. Семантические деревья, теорема Эрбрана

§6. Полнота метода резолюций в логике предикатов

§7. Стратегии метода резолюций

§8. Применение метода резолюций.

§9. Метод резолюций и логическое программирование

Задачи

Ответы, указания и решения

Раздел 2. Теория графов

Тема 5. Раскраски

Тема 6. Ориентированные графы и сети


Fair.ru Ярмарка сайтов
Rambler's Top100 Submitter.ru - Free promoting

Дизайн: Alex © 2002
Все вопросы и предложения можно направлять по адресу cad@mail.ustu.ru