Ш.И._Галиев_МЛ_и_ТА_2004

Доказательство. Пусть формула (3.4) являете» противоречием, тогда ее отрицание является тавтологией:

	(3.6)
Очевидно, имеем
Следсюэтельно, утверхгдение (3.6) можнозаписатьв виде:
	(3.7)
Из (3.7) по теореме 3.2 получаем, что
(Л,&4г&..,&4„) |-В.	0.*)

Теперь, используя утперлдекие (3.2) теоремы 3.3 и утверждение (3.8), получимтребуемое утверждение (3.5). Теорема доказана.

Используя утверждения (3.2) и (3J) теоремы 3.3, можно полу­ чать следствия из заданного множества формул следующим образом.

Для	заданного множества	формул Л„ Аъ--Ат т -Ь		строим
ИХ	конъюнкцию: C~/4i&/fi4...<tJ,. Для		С находим	с.к.н.ф.:
О*	Й1&Я1&...&О1., здесь	!>< 1USk. -	элементарные	суммы

(диэ-ыонкгы}. Теперь по указанной теореме 3.3 получаем, что каждый днзыонктD,, \< !<к, а также ихконъюнкции яюшотся следствиями из

A„A„...Am, w>l, т. е. имеем: АиАп^Ая^О,для любогоI,ls(s£

/41(Л;,...,/4.ih &-А,, &...&Djr, ДЛЯ любого Г, 1< Гбк Илюбы* I),

Jb.-.i/» si. Sb-.Jri к.

Заметим, что для формул логики предикатов понятие логическо­ го следствия нз данной формулы [данных формул) введено о § 6 гл. 2. Нетрудно убедиться, что теоремы 3.1 - 3.4 остаются в силе и для формул noi-ики предикатов, а частности, теорема3.2 для формул логики предикатов уже доказана (см. теорему 2.1).

4!£№- Ул«й отдапь.

Вотrf vkm гяубохляистина.

ЛюЦзы

§ 2. Резольвента дитыонктовлознки высказываний

Пропозициональные буквы с отрицание*! нибо без отрицания,

Питеры L и 1 L назымкчся контрарными. Например, в дизгюкстах С,=Р>/| Q и />л—1 P^Q^S литеры Р и 1 Р - контрарные Такжеконтрарны льттеры Q и 1Q.

Пустьдля дизъюнктовi>i к Di существуетлитере Ii в В\, кото­ рая контрарналитереXj вi>j. Вычеркнув L\ aIj из£)\ иD: соогветственпо, построим дязъкнгкцию оставшихся частей D, и Di. Получен­ ный таким образом дизъютоггназываете? {бинарной}резольвентойD; и£h. ею частообозначают черезЛ.

Примерь:. I. Пусть£>i“fv£>, Di'l PvГ,тогдаS=Q/T.

2.Пусть Dr-P, Bj- . P-JQ (iV'P=»01 тогда Я-О, ниаче нз P иP=>Qполучаеы Q.

3.Пуст»Oj=1 PvQ (Dr-P^Q). Di= Q^T(Ih=Q=>r), тогдаft--] PvT(R-P=>D. ИначеизP^Q »g=.J получаемР=зГ.

Теорема £5. Пусть для дизъюнктов D и D, существует резольвентаЛ. ТогдаX естьлогическоеследствиекзDi и Dj.

Доказательство. ПустьD|-PvZ>i", ft=l Pv IX,*, где D,‘ - ос­ тавшаяся часть диэъюнета ’=1,2 Докажем, что DiJ)-, ^ D^vDt*. Выпишем всевозможные наборы истинмостних яшкннй бука, вхо­ дящих * D) н Di- Выберем набор, положим А-й, не котором Di=H к Dj-И. Допустим, что на этом ^-м наборе буква Р принимает

значение И, тогда 1 Р=Л. поэтому должно быть D ^-li, следовательно,Л ,^А ’=Я

Таким образом, из истинности Z>i и А получили истинность D\“vOj". В случае, если m t-м набеге Р-Л, то и вновь полу­ чаем, что из истинности £)| и Dj следует истинность D,VDj’ В силу произвольности выбранного набора получаем, что из истинности наследует истинностьдля ОЛ-/А*, чтонтребовало:!, доказать.

Qieiyc* rmmammk перей собой чеяь мзыекат епмвбришенЬя всаюдт .. одним и притом проста

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

Рассмотрим задачу вдоснениг, Судет ли В логические следстанем изЛ^!,...^*, г.«. хсткнналистсдующаязапись:

A,At,.-An,\’В.

В | 1 данной главы показано, что ма задача сводится к выясне­ нию невыполнимостиформы

СМ,&4А...Ы«&1в.

Найден для формулы Ссе к.н.ф., то ссть получим конъюнкцию люъюкктоа: C=Di&A<£..

Множество дизъюнктов {2i,Z)b.->>£t} считается н£|ТЫЛ0Л’1и.ндо гегдаи юлысотогда, когдаформулаСневыполнима.

Методом резолюций называется последовательное получение бинарных реэольвекг из даниьп* дгоьюк-ггов и пновь получаемых адъюнктов. Пусть, например, даныдизмоиггы

0,=Л/Г, £>1=1 Рч/Г, л -1 Г.

Используя D, и Di, затемD, и D>, получим резольвенты D,-T: D*—r. затгмvs 1У\КDa—пустойдюъюнкт,который будем обозначать черяз11

Можнодоказатьследующуютеорему.

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

Существует мною различных подходов к построению выводе с помощью метода резолюций. Рассмотрим некоторые из них: метод насыщения уровня, стратегию вычеркивания, лок-резолюцию и один истоддлядюъюнктавспециального вида.

Ктъ сгазовойты веодупогрузшсх. Невозли равно, таи яу(ииа?

§4. Метод иясыщсння уровня

Рвнее был введен метод резолюций и приведет теорема, утверждающая полноту метода резолюций. Пусть имеем множество дтъктиов S={0i,Db..„Di}. Процедуре получение бинарных резольвент неоднозначна, ибо можно сравнивать £>] и D), затем £>i и Dj или гак-то иначе. Рассмотрим метод насыщения уровня. Он состоит t вытислении всех резольвент всех пар дитыонкгов из 5, добавлении этих резольвент к множеству S, вычислении всех следующих резольвент и повторении этого процесса до тех пор, пока не найдется пустой дизъюнкт 3, либо будет установлено, что пустой дюьюикт получил, нельзя. Это зщчнт, мы порождаем

....гдеJ’-S.aS'^ipejo.ibKfflbi^HD,:

Чтобы запрограммировать уют метод на ЭВМ, можно сперва запиит, дичьюнкты iPuS'v.-vS"', затеи вычислять резольвенты, сравнивал последовательно каждый дизъюнкт

с каждым дизъюнктом fteS"1, который расположен после D,, Когда резольвента вычислена, она присоединяется к концу списка, порож­ денному кэтому времени Перейдем к реализации этого процесса для случаи, iVQ,1PvQ. PvlQ. 1fv l Q).

(2)IP*Qi

(3)Pvl Q,

(4)lPvlft

	(5)6	из (1) и(2);
	I6)P	из(1)и(3);
	(7)gvl2		из (1) и(4);
	(8)М />		из(1) и (4);
	0)0*1 б		ш(2)и(3);
	(10)/Vl?		из(2)и(3);
	(11)1р		из (2) и (4);
	(12)1 Q		из (3) и (4);
S':	(13)Pv0		нз(1)н(7);
	{U)PvQ		ш(1)и(8);
	(15)Pv£?		иа(1)н(%
	(16)Л-6		its (1) и(10);
	(17)5		из {1)ч СП);
	(18)?		из (I) и(12);
	(19)2		из (2) и (6);
	(20)	li v e ИЗ(2) и(7);
	(21) liV fi		из (2) и(8);
	(22) 1 PvQ		ia (2) и (9);
	(23)1 Л/g		и*(2) и (10),
	(24)1?	?	нз (2) и (12);
	(25)		из(3) ч (5);
	1,26)Л / '$		да(3)н(7);
	(27) /v l Q из (3) и(8);
	(28)Л/1 Q		ю р )и (9);
	(29)Л/1 g		из (3)и(10);
	(30)	1е	Ю(3)и(11);

95

(3:)1Р	из(4)и(5);
(32)1 с	из(4)н(6);
(33) 1 Pvle И (4)и [7);
(34)1/Vli?	m(4)и(8);
<35)1M g	из(4)*(9*
(36)1л/1е из(4)и (10);
(37)2	из(5) и(7);
(38)2	из(5) и(9);
(39)0	из(5)и(12).

юнктов. Напричец (7), (8), (9j и(10)-тавтологии. Так как тавтология всегда истинна, то, если вычеркиваем тавтологию из невыполнимого множества дизъюнкта», оставшееся множепяо все еще допхснп бы-а невыполнимо. Следовательно, тавтология есть не относящийся *делу дизъюнкт н не должна порождать:». Если же она порождаете*, то (за исключением очень немногих случае») ее следует вычеркнуть. Далее днагюнты Р, Q, 1 Р, 1 Q порождаются неоднократно, Также имеются другие повторяющие^ дизъюнкты (см. (13) - (16), (20) - (23), (26) - (29) н(33) - (36)). На самом аеле. Чтобы получить доказа­ тельство ana S, нужно породить дигьк>нкты (5), (12) н (35). Для сокращенияизбыточное* рассмотримстратегию вычеркивания.

§5. Сграшяя вычеркивания

Дизъюнкт D называйся подбитойк-томD* (или D поглощает й*), сспи D является некоторой частьюдапюнкта £>*. При этом D*

называется каддшыонктэмдля D.

Пример. Пусть D=P, D*=PvQ, Ясно, что D поддитьюнкт для дизионт £>*,а А*- наддизъюккгдляD.

96

Стратегах вычеркивания зависит от того, как вычеркиваются тавтологии и наддизъюнкты Стратегия вычеркивания будет полной, если ее исполыпв&ть вместе с методам насыщения уровней следую­ щим образом; сперяа выписываются дизъюнкты tfvi'V .. v.V"1) по порядку; затем вычисляются резольвент сравнением каждого щвъюнкта D|G(i4vSlv...vS"’1) с дизьганктом Д,б5и, стоищна после D, Когда резольвента вычислена, она записываете» в конце спискгц кактолько порождаете», еслиона нетавтология и не поглоща­ ется каким-шбудь дизъюнктом и.> описка. В противном случае она вьяеркиваьтся. Очевидно, что при этой не выписывается повторно

к примеру и? §4 и получимследующийсписок: S0. (1)А'Й

в )? 'Л й

(4>iivi &

s'.-	(¾ е	из ЦП1(2),
	<б)р	® (1) »Р).
	(7) ■?	из(2)кi№.
	(8)18	из(3)1К4),

& □ из (5) и (8).

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

Ясно, что необходимые вычисления не уменьшаются, а увели­ чиваются. Чтойм использовать стратегию вычеркивания, нужно уметь решать, является ли полученный дизъюнкт тавтологией или является лиодиниздшьюнктов пядяиаьюиктом другого.

Метод резолюций, как ужеуквано, позволает автоматизировать

люции может порождать иного .ишних и ненужные дизъюкктов на­ ряду с шитезными. Хстл можно использовать стратегию еычеркива-

нив, чтобы выбросить некоторые из эти* ненужных и бесполезных дизъюнкгоа после того, пак о т порождены. На ИХ порождение уже

нужны большиересурсы машинного временидля того, чтобы опреде­ лить, чтоэтидитьюнктыДействительнолишние и ненужные. Поэтому дм получения 5ффеиивных процедурследует недопускать порожде­ ния большого числа бесполезных дизъюнктов. Имеются различные подходы куменьшениювычислений, среди них: методсемантической

Рассмотрим лох-резолюцию.

Xopouiesвдвойнехорошо, ш хороша.

КальпмрГркаи

§6. Лок-реюлшцня

Иде» лок-резолюииисостеэт, по существу, к использовании ин­

дексов для упорадаяенияхитер вдизъюнктахиз данного множеств

лнзькжкгов. Иными словами, он» вкяючаег введение индексов для

каждого вхождения литеры в S некоторым испым чис.тпм; разные

вхождения одной н той же литеры могут быть индексированы

по-разному. После этого отрезать (удалить) разрешается только лите­

ры с наименьшим индексом в каждом нз

дизъюнктов. Jlirrcpu

в реэольвегах наследуют свои индексы из посылок

Если дагкра

в резольвенте можетунаследоватьболее одного индекса, го ейсгааиг-

сив соответствиенаименьшийиндекс.

Рассмотрим следующиедвадизъюнкта:

pvfiipve.

Введеминдексы,ИУгорыебудем писалслеваситу отлитеры:

о ь ^ й

T

a x

я .1 к » е

ми

ен

нд

еь кш с

е

I ч

ье

м

и

н

д

к

а

к,Р

о т р

еР.з Ва

т

ь;

i|

Р

' /

«

2

р

а з

р

е ш

а

е

т е

Таким образом, примени правило резолюции к дизъюнктам (1) и(2) по iPи jl Р получаем следуюшяйдизъюнкт:

JImepi -Q и ,Q одна и та же. Так как 2<4. то Q получает ннлскс2, поэтомуполучаем

(4) iff.

и являете! лок-рвзельеентой дизъюнктов (1)

Дизъюнкт

(4)

и (2). О

н

ш

а

ч

ечто

те

си был

милот-еры,

вд

м

н

е

г

р

ъ (2)к былиш

индексирок т е ­

ваныи

е

,

н

а

п

р

и

,

т а

к :

(^/IfVsQ,

то литерой в дипкппгк

(2'),

которую разрешено

отрезать, была

бы TQ Однако к iP a yQ нельзя применить правшто резолюиин. Пгагому нв существует лок-реэольвенты дизъюнктов (1) и (2), Пол аон-резотцмй понимается иосяедоамельное получение лок-резольвеиг из данного множества дизъюнктов и вновь получае-

Расснотрим множествоS дшъюниов, которое введенов § 4:

PvQ.

Pv'lQ,

1 PvQ. i? v ie .

Проведем следующую индексацию:

(1) A	jg
(2)^410,
(4)»'?vjle.
Из дизыошп-ов		(1)-(4) можно получил только одну
лок-резольвеягу( 5	)	s l P
а издизъюнктов (1)-(5) толькодвелок-резолыекта:
(6Ы2		из(1) иfi),
(7),1б		и*(2)11(¾.

99

Применяяпрюма резолюции кдизъюнктам(6) и(7), имеем

т .

Таким образом, получаем выводпустогодюыонкгаО. Отметим, что были порождены всего три лок-ре5ольвекгы.

При использовании обычней (неограниченной) революции ДО полу­

чения □ была	порождены 34 рездльвекта. Результативность
лок-резолюцяи не зависит оттого, как проиндексировать литеры в S,
Введеме рассматриваемом примереиндексы иначе, например, тах:
(1) A J2
(2)A .1&
(3),1
(4 )rlf4 l0
Из(1)н(3) получим:
0)«&
Аналогичнополучаем;
(6) гд ч 'д		и5(1>и(4>,
W tfv .lQ		и(Я«(3),
(K),1Q		из(2) и(4),
(¢)	О	из(5) и (8).

Можнодоюзать следующую теоремуо полнотелок-резолющш.

Теорема 3.7. Пусть S - множество аетыонктов, в котором каждая лгара индексирована целым числом. Если S противоречиво (невыполнимо), то имеетсялок-выводпустогодизъюнкта□ изS.

АкиреИБмый

§7. Метод резолюций для хорнпвеких дизъюнктов

Вобщем случае методрезолюцийтребуетбольших вычислений. Если дизъюнкты имоютспециальный вна, являюк* так называемыми хориовекимидизъюнктами, то вычисления упрощаются.

100