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

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

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

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

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

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

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

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

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

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

Начнем с формулировки правила резолюций.


Определение. Правилом резолюций в логике предикатов называется правило из дизъюнктов ØP(t1,...,tn)ÚF и P(s1,...,sn)ÚG выводим дизъюнкт s(F)Ús(G), где s – наиболее общий унификатор множества {P(t1,...,tn), P(s1,...,sn)}. Дизъюнкт s(F)Ús(G) называется бинарной револьвентой первых двух дизъюнктов, а литералы ØP(t1,…,tn) и P(s1,…,sn) отрезаемыми литералами.

Например, с помощью правила резолюций из дизъюнктов ØQ(a,f(x))ÚR(x) и Q(u,z)ÚØP(z) можно вывести дизъюнкт R(x)ÚØP(f(x)), используя подстановку s={u=a, z=f(x)}.


В отличие от логики высказываний, в логике предикатов нам понадобится еще одно правило.


Определение. Правилом склейки в логике предикатов называется правило: из дизъюнкта àP(t1,...,tn)Ú...ÚàP(s1,...,sn)ÚF выводим дизъюнкт s (àP(t1,...,tn)Ú s (F), где s – наиболее общий унификатор множества {P(t1,...,tn),...,P(s1,...,sn)}, à – знак отрицания или его отсутствие. Дизъюнкт s(◊P(t1,…,tn)Ús(F) называется склейкой первого дизъюнкта. (Отметим, что если знак отрицания стоит перед одной из записанных выше атомарных формул, то он стоит и перед другими.)

Например, правило склейки, примененное к дизъюнкту ØР(х,у)ÚØP(у,х)ÚØР(а,а)ÚQ(x,y,v), дает дизъюнкт ØР(а,а)ÚQ(a,a,v).


Определение вывода в логике первого порядка немного отличается от аналогичного определения в логике высказываний.


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


D1,D2,…,Dn,


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


Как и в логике высказываний, дизъюнкт D выводим из S, если существует вывод из S, последним дизъюнктом которого является D.

Приведем пример. Пусть S={ØB(x)ÚØC(x)ÚT(f(x)), C(у)ÚT(f(z)), B(a)}. Тогда последовательность


D1=ØB(x)ÚØC(x)ÚT(f(x)),

D2=C(у)ÚT(f(z)),

D3=ØB(x)ÚT(f(x))ÚT(f(z)),

D4=ØB(x)ÚT(f(x)),

D5=B(a),

D6=T(f(a)).


является выводом из S. Отметим, что D1,D2,D5ÎS, дизъюнкт D3 выводим из D1 и D2 по правилу резолюций, дизъюнкт D6 выводим из D4 и D5 по тому же правилу, а D4 выводим из D3 по правилу склейки.


Как и в логике высказываний, в логике первого порядка есть утверждение, называемое теоремой о полноте. Фактически это утверждение совпадает с формулировкой 4.1. Тем не менее приведем его.


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

Теорема имеет довольно сложное доказательство. Оно будет приведено в §6.


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

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


Рассмотрим пример. Пусть


F1=($х)[П(х) & ("у)(С(у) ® З(х,у))],

F2=("x)("у)[П(х) & Л(у) ®Ø З(х,у)],

G=("x)(C(x)®ØЛ(х)).


Докажем, что формула G является логическим следствием множества формул F1,F2. Для этого достаточно доказать невыполнимость множества Т={F1,F2,ØG}. Каждую из формул множества Т приведем к сколемовской нормальной форме; получим формулы


("y)[П(а) & (ØC(у)ÚЗ(а,у))],

("х)("у)[ØП(х)ÚØЛ(у)ÚØЗ(х,у)],

C(в) & Л(в).


Тогда множество S будет содержать дизъюнкты: D1=П(а), D2=ØC(у)ÚЗ(а,у), D3=ØП(х)ÚØЛ(у)ÚØЗ(х,у), D4=C(в), D5=Л(в). А последовательность дизъюнктов D1, D3, ØЛ(у)ÚØЗ(а,у), D5, ØЗ(а,в), D2, D4, З(а,в), □ будет выводом из S. Cледовательно, формула G является логическим следствием формул F1 и F2.


Введем, как было обещано выше, ряд определений, необходимых в следующих параграфах.

Напомним, что мы условились не писать в дизъюнктах повторяющиеся литералы. Это позволяет нам смотреть, если это необходимо, на дизъюнкт как на множество литералов. Если смотреть на дизъюнкты как на множество литералов, то результат применения правила резодюций к дизъюнктам D1 и D2 с отрезаемыми литералами L1 и L2 можно записать так


D=[s(D1)-s(L1)]È[s(D2)-s(L2)],


где s – наиболее общий унификатор L1 и ØL2.


Определение. Револьвентой дизъюнктов D1 и D2 называется одна из следующих бинарных револьвент:


1) бинарная револьвента дизъюнктов D1 и D2,

2) бинарная револьвента склейки D1 и дизъюнкта D2,

3) бинарная револьвента дизъюнкта D1 и склейки D2,

4) бинарная револьвента склейки D1 и склейки D2.


Приведем пример. Пусть D1=ØP(y)ÚØP(g(x))ÚR(f(y)), D2=P(g(a))ÚQ(b). Склейка дизъюнкта D1 есть дизъюнкт D1/=ØP(g(x))ÚR(f(g(x)). Бинарная револьвента D1 и D2/ равна R(f(g(a)))ÚQ(b). Следовательно, последний дизъюнкт есть револьвента дизъюнктов D1 и D2.


Определение. Если D – дизъюнкт, а s – подстановка, то дизъюнкт s(D) называется примером дизъюнкта D.


Следующее утверждение часто называют леммой о подъеме.


Теорема 4.4. Если D1/ – пример дизъюнкта D1, D2/ – пример дизъюнкта D2 и D/ – револьвента D1/ и D2/, то существует револьвента D дизъюнктов D1 и D2 такая, что D/ – пример D.


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

Так как D1/ – пример D1 и D2/ – пример D2, то существуют подстановки a1 и a2 такие, что D1/=a1(D1) D2/=a2(D2). Последовательность a=(a1,a2) также будет подстановкой и поскольку  D1 и D2 не имеют общих переменных, то D1/=a(D1) и D2/=a(D2).

Дизъюнкт D/ является револьвентой дизъюнктов D1/ и D2/. Это означает, что существуют литералы L1/ÎD1/ и L2/ÎD2/ и подстановка t такие, что t наиболее общий унификатор L1/ и ØL2/ и


D/=(t(D1/)-t(L1/))È(t(D2/)-t(L2/)).                   (1)


(Если при получении револьвенты D/ к дизъюнктам D1/ т D2/ применялись склейки, то будем считать, что они учтены подстановками a1 и a2.)

Пусть L11,…,L1r – литералы дизъюнкта D1, которые подстановкой a переводятся L1/, а L21,…,L2s – литералы дизъюнкта D2, которые подстановкой a переводятся в L2/. Литералы L11,…,L1r, следовательно, унифицируемы, а поэтому существует наибелее общий унификатор b1 для этого множества. Дизъюнкт b1(L11) (равный b1(L12),…,b1(L1r)) обозначим через L1. По определению наиболее общего унификатора найдется подстановка g1,  для которой выполняется равенство a1=g1b1. По аналогичным соображениям, существуют подстановки b2 и g2 такие, что b2 – наиболее общий унификатор множества литералов L21,…,L2s и a2=g2b2. Литерал  b2(L21) обозначим через L2. Дегко видеть, что L1 и L2 не имеют общих переменных. Поскольку дизъюнкты D1 и D2 также не имеют общих переменных, то можно считать, что  b1=b2=b, g1=g2=g и a=gb. Сказанное в этом абзаце иллюстрируется рисунками 4.1 и 4.2.


Рис. 4.1

Рис. 4.2


Литералы L1′ и ØL2′, как отмечено выше, унифицируемы подстановкой t. Следовательно, литералы L1 и ØL2 также унифицируемы (подстановкой tg). Отсюда следует, что существует наиболеее общий унификатор s множества {L1 ØL2} (см.рис.4.3). Возьмем в качестве D дизъюнкт


D=[s(b(D1))–s(L1)]È[s(b(D2]–s(L2)]                      (2)


Ясно, что D – резольвента дизъюнктов D1 и D2. Осталось показать. Что D′ –пример D.


Рис. 4.3


Так как s – наиболее общий унификатор L1 и ØL2, то существует подстановка s такая, что tg=ds. В таком случае из последнего равенства, равенств (1), (2) и a=gb следует, что


D′=(t(D1′)–t(L1′))È(t(D2′)–t(L2′))=[t(a(D1))–t(a(L11))]È[t(a(D2))–(r(a(L21))=

[(ta)(D1)–(ta)(L11)]È[(ta)(D2)–(ta)(L21)]=

[(tgb)(D1)–(tgb)(L11)]È[(tgb)(D2)–(tgb)(L21)]=

[(dsb)(D1)–(dsb)(L11)]È[(dsb)(D2)–(dsb)(L21)]=

d[s(b(D1))–s(L1)]Èd[s(b(D2))–s(L2)]=d(D).


Мы доказали, что D′ – пример D.


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

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

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

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

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

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

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

Задачи

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

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

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

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


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

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