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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Рассмотрим применение метода резолюций в доказательстве теорем и при планировании действий.


Доказательство теорем. Применим метод резолюций в доказательстве одной простой теоремы из теории групп.

В качестве исходной возьмем следующую аксиоматику теории групп:


F1: ("x,y,z)[(xy)z=x(yz)],

F2: ("x,y)($z)(zx=y),

F3: ("x,y)($z)(xz=y).


Предположим, что нам надо доказать теорему G: ($x)("y)(yx=y), т.е. что в группе существует правая единица.

Наша задача–установить, что формула G есть логическое следствие формул F1, F2, F3. Прежде, чем решать эту задачу, перейдем к другой сигнатуре. Введем символ трехместного предика P, который интерпретируется следующим образом:

P(x,y,z) означает, что xy=z.

В новой сигнатуре формулы F1, F2, F3 и G запишутся так:


F1/=("x,y,z)[(x,y,u)&H(y,,z,v)&P(x,v,w)®P(x,z,w)],

F2/=("x,y)($z)P(z,x,y),

F3/=("x,y)($z)P(x,z,y),

G/=($x)("y)P(y,x,y).


Сформулируем множество T={F1,F2,F3,ØG}, каждую из формул этого множества приведем к сколемовской нормальной форме и удалим кванторы общности (конъюнкция в сколемовских нормальных формах не появится). Получим множество дизъюнктов D1,D2,D3,D4:


D1=ØP(x,y,u)ÚØP(y,z,v)ÚØP(x,v,w)ÚP(u,z,w),

D2=P(f(x,y),x,y),

D3=P(x,g(x,y)y),

D4=ØP(h(x),x,h(x)).


Построим вывод пустого дизъюнкта из множества дизъюнктов D1,...,D4. Пусть эти дизъюнкты–первые дизъюнкты вывода. Заменим переменные в дизъюнкте D2, получим дизъюнкт D2/=P(f(x/,y/),x/,y/). Литералы P(x,y,u) и D2/ унифицируются подстановкой s1={x=f(x/,y/),y= x/, u=y/}. Применим правило резолюций к D1 и D2 (и указанным литералам), получим дизъюнкт


D5="P(x/,,z,v)ÚØP(f(x/,y/)v,w)ÚP(y/,z,w).


Далее, литерал P(f(x/,y/),v,w) и D2 унифицируются подстановкой s2={x/=x,y/=y,v=x,w=y}. Правило резолюций, примененное к D1 и D2, дает дизъюнкт


D6=ØP(x,z,x)ÚP(y,z,y).


Резольвентой дизъюнктов D3 и D6 будет дизъюнкт


D7=P(y,g(y/,y/),y).


(Для получения этой резольвенты заменим переменные в D3, получим D3=P(x/,g(x/,y/),y/) и используем подстановку s3={x=y/,z=g(y/,y/)}. Наконец, из дизъюнктов D4 и D7 с помощью подстановки s4={y=h(g(y/,y/)), x=g(y/,y/)} получаем пустой дизъюнкт.

Планирование действий. Отметим вначале одно свойство метода резюлюций. Пусть сигнатура t состоит из двух символов двухместных предикатов P и Q, которые интерпретируются следующим образом: P(x,y) означает, что х–сын y, Q(x,z) означает, что х–внук z.Рассмотрим формулы:


F1=("x,y,z)[P(x.y)&P(y,x)®Q(x,z)],

F2=("x)($y)P(x,y),

G=("x)($z)Q(x,z),


смысл которых достаточно ясен.

Используя метод резолюцийц, покажем, что G есть логическое следствие F1 и F2. Приведем формулы F1,F2 и ØG к сколемовской нормальной форме, получим дизъюнкты:


D1=ØP(x,y)ÚØP(y,z)ÚQ(x,z),

D2=P(x,f(x)),

D3=ØQ(a,z).


Вывод пустого дизъюнкта получается довольно просто:


D4=ØP(a,y)ÚØP(y,z) ((D1 D3, {x=a}),
D5=ØP(f(a),z) (D2 D4 {x=a, y=f(a)}),
D6=□ ( D2 D5, {x=f(a),z=f(a))}.

Подстановка z=f(f(a)) означает, что дед элемента a есть отец элемента a. Таким образом, метод резолюций не только устанавливает факт логического следствия формулы G из формул F1 и F2, но еще и «подсказывает», как по данному х получить z такой, чтобы формула Q(x,z) была истинна.

Довольно часто интересующая нас переменная участвует не в одной подстановке, как в этом примере переменная z, а в нескольких. Для того, чтобы тследить все подстановки, в которых может изменить значение переменная, к формуле ØG добавляют литерал ответа ANS(z) и заканчивают вывод не пустым дизъюнктом, а литералом ответа.

В качестве примера использования метода резолюций в задачах планирования действий рассмотрим известную в теории искусственного интеллекта задачу об обезъяне и бананах. В задаче говорится об обезъяне, которая хочет съесть бананы, подвешенные к потолку комнаты. Рост обезъяны недостаточен, чтобы достать бананы. Однако в комнате есть стул, встав на который обезъяна может достать бананы. Какие ей надо совершить действия, чтобы достать бананы?

Задачу формализуем следующим образом. Комнату с находящимися в ней обезъяной, стулом и бананами будем называть предметной областью. Конкретной местонахождение в комнате обезъяны, стула и бананов будем называть состоянием предметной области. Рассмотрим два предиката P(x,y,z,s) R(z). Пусть


P(x,y,z,s) означает, что в состоянии s обезъяна находится в точке x, стул – в y, бананы – в z,
R(s) означает, что в состоянии s обезъяна взяла бананы.

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


ИДТИ(x,y,s) – состояние, которое получится из s, если обезъяна из точки x перешла в y,
НЕСТИ(x,y,s) – состояние, которое получится из s, если обезъяна перенесла стул из точки x в y,
БРАТЬ(s) – состояние, которое получится из s, если обезъяна взяла бананы.

Условия задачи запишутся в виде следующих формул:

F1=("x,y,z,s))[P(x,y,z,s)®P(u,y,z, (x,,,u,s))],

F2=("x,z,s)[P(x,x,z,s)®P(u,u,s, (x,u,s)],

F3=("x)[P(x,x,x,s)®R( (s))].


Пусть в начальном состоянии s0 обезъяна находилась в точке а, стул–в точке b, бананы–в точке c. Следовательно, к написанным формулам надо ддобавить формулу

F4=P(a,b,c,s0).

Надо показать, что формула G=($s)R(s) есть логическое следствие формул F1,F2,F3,F4. Из множества формул F1,F2,F3,F4,ØG получим множество дизъюнктов D1–D5 (к дизъюнкту, полученному из ØG добавлен литерал ответа ANS(s)):


D1=ØP(x,y,z,s)ÚP(u,y,z,ИДТИ(x,u,s)),

D2=ØP(x,x,z,s,)ÚP(u,u,z,НЕСТИ(x,u,s)),

D3=ØP(x,x,x,s)ÚR(БРАТЬ(s)),

D4=P(a,b,c,s0),

D5=ØR(s)ÚANS(s).


Последовательность дизъюнктов D1–D5 продолжаем до вывода литерала ответа:


D6=ØP(x,x,x,s)ÚANS(БРАТЬ(s)) (из D3 D5),
D7=ØP(x,x,u,s)ÚANS(БРАТЬ(НЕСТИ(x,u,s))) (из D2 и D6),
D8=ØP(x,y,z,s)ÚANS(БРАТЬ(НЕСТИ((y,z,ИДТИ(x,y,s)))) (из D1 и D7),
D9=ANS(БРАТЬ(НЕСТИ(b,c,ИДТИ((a,b,s0)))) (из D4 и D8).

Итак, для того, чтобы обезъяне взять бананы, надо сначала из точки а идти в точку b, затем из точки b нести стул в точку с и в точке с, встав на стул, взять бананы.

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

Задачи

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

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

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

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


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

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