Дедуктивный вывод на знаниях

В. И. Вагин

Основные определения

В дедуктивных моделях представления и обработки знаний решаемая проб­лема записывается в виде утверждений формальной системы, Цель — в виде утверждения, справедливость которого следует установить или опровергнуть на основании аксиом (общих законов) и правил вывода формальной системы. В качестве формальной системы используют исчисление предикатов первого порядка.

В соответствии с правилами, установленными в формальной системе, за­ключительному утверждению — теореме, полученной из начальной системы ут­верждений (аксиом, посылок), приписывается значение ИСТИНА, если каждой посылке, аксиоме также приписано значение ИСТИНА. Формула В является логическим следствием формул F_u F_it..., F_n тогда и только тогда, когда для любой интерпретации, в которой конъюнкция Fi&F₂&... &F_n истинна, форму­ла В также истинна.

Доказательством теоремы называется поиск ответа на вопрос: следует ли логически формула В из заданного множества формул F_lt F₂, —, F_n, что рав­носильно доказательству общезначимости формулы Fi&F₂&... &.F_n-+B или про­тиворечивости (невыполнимости) формулы Fi&F₂&... &F_n&^8. Из практиче­ских соображений удобнее доказывать противоречивость формулы, причем процедура установления невыполнимости формулы Fi&F2&... &F_n& ~] В называ­ется процедурой опровержения.

В логике было доказано, что не существует эффективной разрешающей процедуры для исчисления предикатов первого порядка, позволяющей узнать по данной формуле, является она теоремой или нет [Church, 1936]. Неразре­шимость исчисления предикатов первого порядка не закроет путь для авто­матического доказательства теорем, если воспользоваться ограничением, свя­занным с априорным предположением об общезначимости формулы, которую следует доказать.

Рассматриваемые далее методы поиска доказательств подтверждают, что формула общезначима (т. е. является теоремой), если она на самом деле та­ковой является. Для необщезначимых формул алгоритмы доказательства тео­рем работают бесконечно долго. Принимая во внимание результат А. Черча и А. Тьюринга, это лучшее, что можно ожидать от процедур доказательства теорем.

Краткая история

Стремление найти общую разрешающую процедуру доказательства тео­рем наблюдается у Лейбница, Пеано, в школе Гильберта. Автоматическое до­казательство теорем берет начало от работы [Herbrand, 1930], Процедура вы­вода Зрбрана основывается на его теореме, которая гласит: множество дизъ­юнктов (т. е. букв или их отрицаний, соединенных знаком V) S невыполнимо тогда и только тогда, когда существует конечное невыполнимое множество фундаментальных примеров (т. е. константных случаев) дизъюнктов в S. Та­ким образом, для установления невыполнимости (противоречивости) множегт-

ва дизъюнктов необходимо образовывать множества Si, S₂,..., S_m,... констант­ных случаев дизъюнктов и последовательно проверять их на ложность. Теоре­ма Эрбрана гарантирует, что если исходное множество дизъюнктов 5 невы­полнимо, то данная процедура обнаружит такое т, что S_m ложно.

С помощью эрбрановской процедуры вывода, реализованной на ЭВМ, был доказан ряд простых теорем их логики высказываний, но программа столкну­лась с непреодолимыми трудностями, при доказательстве теорем логики пре­дикатов [Gilmore, 1960J. Основной недостаток процедуры Зрбрана состоит в экспоненциальном росте конечных множеств фундаментальных примеров дизъюнктов Si при увеличении L

Ненамного эффективнее был метод Девиса и Патнема, с помощью кото­рого были доказаны некоторые теоремы из логики предикатов первого поряд­ка, оказавшиеся недоказуемыми у Гил мора [Davis et al., 1960].

Наконец, в 1964—1965 гг. были созданы обратный метод вывода С. Масло-ва [Маслов, 1964j и принцип резолюций Дж. Робинсона [Robinson, 1965].

Обратный метод вывода

В этом методе поиск вывода идет от целевой формулы к аксиомам или постулатам, истинность которых априорно известна. Чтобы определить выво­димость формулы В из посылок F_u F₂,..., F_n, необходимо найти формулы пред­шественники, из которых В может быть выведена одним применением пра­вила вывода. Затем по каждой из получившихся формул-предшественников, 'не являющейся аксиомой исчисления, определяется множество непосредственных формул-предшественников и т. д. вплоть до построения окончательного выво­да. Дерево, возникающее в ходе такого процесса, называется деревом поиска вывода, оно превратится в дерево вывода в тот момент, когда все его «листья» окажутся аксиомами исчисления.

Поясним работу обратного метода на следующем примере. Имеем две схемы вывода:

1. Fx{a, xt)&Ft{xt, a)^Bi{a, xt), i=lX _

2. F₃(y_j<)&F₄(z_jⁱ)&B_l(a, _Xl)^B_s{a, щ), /=1,3.

Априорно истинными считаются следующие предикаты: Fi(a, Xi), Fi(a, Хц), Fi(a, x₄), F₂(x₃, a), F₂(x₄, a), B,{a, xi), F»(yi^l), Fs{yf)_f F*(yS), F₃(y^), fa(t/2²), Р₃(у₃*), Fi(Z2^l), F₄(zi³), F₄(zs⁴) (начальная ситуация). Необходимо получить истинное значение для предиката ^(о, иг).

Обратный вывод идет от.нужного результата. Предположим, что В%(а, иг) является истинным, я определим, нет ли среди априорно истинных п/редикатов предиката 5г(о, и$). Если он находится в этом списке, то вывод заканчивает­ся. В примере это не так. Тогда просматриваются все схемы вывода и в пра­вых частях схем отыскивается предикат вида В₂(а, Uj). В примере такая схема одна. Заменяем в ней всюду / на 3 и анализируем истинность выражения Рг(уз')&р4(2*¹)&Вг(а, xi). Так как это конъюнкция, то истинными должны быть все три предиката, входящих в нее. Но их истинность зависит еще от значе­ния /. Положим i=l. Проверим, используя описание начальной ситуации, ис­тинность предикатов F₃{yz^l), F₄(zz^l), B_t(a, x_t). Видим, что Р₉(у_г^х) не явля­ется истинным, поэтому берем /=2. По той же причине это значение i отвер­гается. При (=3 наблюдается аналогичная картина. При /=4 предикат Р$(у₃*) является истинным. Предикат F₄(zs*) также истинен. Предикат Bi(a, x₄) ло­жен. Определим условия, при которых В\(а, х₄) истинно. Для этого просматри­ваются правые части схем вывода и находятся те схемы, в правых частях ко­торых стоит предикат B_t(a, xi). В примере такая схема одна. Полагаем в ней /=4 и анализируем левую часть схемы: F\{a, x₄)&F₂{xi, а). Из описания на­чальной ситуации видно, что данное выражение является истинным. Вывод окончен.

Если бы на некотором шаге поиска вывода было получено несколько схем вывода с нужными празыми частями, то были бы альтернативные варианты и 90

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

На основе обратного метода вывода были разработаны машинный алго­ритм вывода [Давыдов и др., 1969] и несколько версий алгоритма машинного поиска естественного логического вывода в исчислении высказываний (АЛПЕВ) [Шанин и др., 1965]. Разработка версий систем АЛПЕВ — ЛОМИ и алгоритма вывода на основе обратного метода носила поисковый характер и показала принципиальную возможность машинных доказательств теорем.

Принцип резолюций

Метод резолюции (см. § 1.2) требует, чтобы исходная логическая формула была приведена к специальному виду, называемому пренексной нормальной формой (ПНФ), имеющей вид^ х_г >j₂ х₂...)|_я х_пМ, где)^е {у*Я} (1 < * <«)- М — бескванторная формула (матрица), а префикс есть последовательность кванторов. В свою очередь, М представляется в виде конъюнктивной нормаль­ной формы (КНФ) F,&F>&... &F~. где каждая из F_t, F₂,...,F_n есть дизъюнкция литер (т. е. букв или их отрицаний). Сохраняя противоречивость (общезначи­мость) формулы, в ней можно устранить кванторы существования, используя сколемовские функции. В итоге получим стандартную форму.

Например, для определения стандартной формы формулы

Ч*(2У{Р(*> y)V~[Q(y. z))^-gzR{x, у, г)). преобразуем ее в ПНФ:

. y)&Q(y, *)) Va**(*. y> *)) =

y)ScQ(y, г) V R(x, у, г)).

Матрицу сведем к КНФ:

У)УЩх, у, z))&(Q(y, z)VR(x, у, г))).

Устранимз 2 введением сколемовской функции z=f(x, у). Имеем следующую стандартную форму:

V*W((1 Р(Х, у) У R (х, у, f{x, у))) A (Q (у, f (x, y))\/R (x, у, f(x, у)))).

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

В итоге любая формула может быть представлена множеством дизъюнк­тов, т. е. дизъюнкцией литер. В примере множество дизъюнктов S= ^:={~]P(x,y)\/R(x,y,f(x_ty)), Q(y,f(x,y))\/R(x,y,f(x,y))}. Здесь запятая меж­ду дизъюнктами заменяет знак &. Более подробное изложение сведения любой формулы к множеству дизъюнктов можно найти в [Чень и др., 1983].

Основная идея принципа резолюции заключается в проверке, содержит ли множество дизъюнктов S пустой дизъюнкт (см. § 1.2). Когда дизъюнкт не со­держит никаких литер, то он называется пустым. Так как пустой дизъюнкт не содержит литер, которые могли бы быть истинными при любых интерпретаци­ях, то он всегда ложен. Обозначим его через D. Если S содержит П, то S противоречиво (невыполнимо). Если 5 не содержит П, то следующие шаги заключаются в выводе новых дизъюнктов до тех пор, пока не будет получен □ (что всегда будет иметь место для невыполнимого S). Таким образом, прин­цип резолюций рассматривается как правило вывода, с помощью которого по­рождаются новые дизъюнкты из S.

По существу принцип резолюций является расширением однолитерного правила Девиса и Патнема, идея которого заключается в следующем, В двух дизъюнктах, один из которых состоит из одной литеры, а второй содержит произвольное число литер (в том числе и одну), находится контрарная пара литер (например, Р и ~\Р), которая вычеркивается, и из оставшихся частей дизъюнктов формируется новый дизъюнкт (например, Q из Р и "l^VQb От­метим, что ничего нового по сравнению с известным правилом modus ponens здесь нет, так как, например, ~\P\/Q равносильно P-+Q и из выводимости Р и P-+Q следует выводимость Q.

Дж. Робинсон расширил однолитерное правило Девиса и Патнема на слу­чай произвольных дизъюнктов с любым числом литер. Если в любых двух дизъюнктах Су и С₂ имеется контрарная пара литер, то при вычеркивании ее формируется новый дизъюнкт из оставшихся частей дизъюнктов. Этот вновь сформированный дизъюнкт называется резольвентой дизъюнктов С\ и С%. На­пример, пусть

Тогда резольвента С: Р \/ П F.

Обоснованность получения таким образом резольвент вытекает из теоремы, гласящей, что резольвента С, полученная из двух дизъюнктов С\ и С₂, явля­ется логическим следствием этих дизъюнктов.

Если в процессе вывода новых дизъюнктов получены два однолитерных дизъюнкта, образующих контрарную пару, то резольвентой этих двух дизъ­юнктов будет пустой дизъюнкт П. Таким образом, выводом пустого дизъюнкта □ из множества дизъюнктов S называется конечная последовательность дизъ­юнктов Си С₂,..., Ck, такая, что любой d (l^i^k) является либо дизъюнктом из S, либо резольвентой, полученной принципом резолюций, и Са = П.

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

С_Ж:-\РШ)

то резольвента может быть получена только после применения к новки f(x) вместо х. Имеем

) V

резольвента

C:~\R(f(*))VQ(y)-

Отсюда подстановка 0 называется унификатором для множества выраже­
ний W_u W_{2................} W_h тогда и только тогда, когда 1^,6 = И?₂6—... =В?_А6

(см. § 1.2).

Унификатор <т для множества выражений W\, W₂,..., Wk называется наи­
более общим унификатором (НОУ) тогда и только тогда, когда для каждого
унификатора 6 для этого множества существует такая подстановка X, что 0 =
= <ьА,, где аоХ — композиция подстановок. В свою очередь композиция под­
становок o={ti/x_u t₂jx₂,..., tn/xn) и X<={ui!yi, u₂/y₂,..,,u_m/y_m} есть подста­
новка вида {tiX/xi, t₂X/xi.................. t_nX/x_n, U\ly_u u₂/y₂,.... u_m/y_m], из которой вычер­
киваются все tjX/xj, если tiX==xj, и все щ/yi, такие, что y_L(={x_u x₂,..., х_п).
В примере унификатор {/(*)/*} являлся НОУ.
92

Дж. Робинсон предложил алгоритм унификации, который находил НОУ, если множество выражений W_i} W_2}..., W_k было унифицируемо, и сообщал о неудаче, если это не так.

Если две или более литеры (с одинаковым знаком) дизъюнкта С имеют НОУ о, Со называется фактор-дизъюнктом Например, пусть С= =P(x)VP(f(y))VQ(x). Тогда o={f(y)/x) и Ca = P(f(y))VQ(f(y)) есть фак­тор-дизъюнкт.

В логике предикатов первого порядка резольвента для исходных дизъюнк­тов Ci и С₂ может быть получена одним из четырех способов: 1) из Ci и С₂; 2) из C_t и С₂а\ 3) из da и С₂; 4) из С\а и С₂о.

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

Так, имеем две посылки и заключение: некоторые студенты любят всех преподавателей, ни один из студентов не любит невежд, следовательно, ни один из преподавателей не является невеждой. Докажем это заключение из двух посылок принципом резолюций. Для этого введем следующие предикаты: С(х) — х —студент, Р(х) — х — преподаватель, Н(х) — х —невежда и Г.(х, у) — х любит у. Тогда две посылки на языке логики предикатов первого порядка бу­дут иметь вид

2X(C(x)*Vy(P(y)-*l><x_t у)));

. У))). Заключение будет выражено как у у (Р (у)-+ ~] Н (у)),

На языке дизъюнктов посылки и заключение (его необходимо взять с от­рицанием) будут иметь вид

1) С(а);

2) 7(y)Vi(e. у);

3) ~\С(х)\/-\Н(у)\/-\Цх, у);

4) Р(Ь);

5) Н(Ь).

Докажем, что это множество дизъюнктов невыполнимо. Имеем
(а, у) из 1) и 3); а ■

из 2) и 4); 9 ■

из 6) и 7); и

из (5) и 8).

Указанный вывод представляется деревом вывода (рис 2 2)

Принцип резолюций эффективнее процедуры Эрбрана. Но и он
существенным недостатком, заключающимся в формировании
резольвент большинство из которых оказываютсяЧенужными. Согочи
ные модификации принципа резолюций направлены на нахождение более эф­
фективных стратегий поиска нужных дизъюнктов. Остановимся на тех которые
нашли применение в моделях обработки знаний, в основе которых лежит ис­
числение предикатов первого порядка. которых лежит ис-

Отметим, что основными способами устранения причин «экспоненпияльнп го взрыва», имеющего место при доказательстве теор^м^а^^скоТс^пенн" сложности, являются использование семантики и встраивание Г правила вы вода н алгоритмы унификации специфики конкретной области применения.

Рис. 2.2

да имеется подстановка б, такая, что С^бе

глощенным дизъюнктом. Например, пусть CiP(x) и Ct P{a)\/R{y). Так как б*» {а/*}, то Ci6 = P(a). Тогда Ci6sC₂ и С\ поглощает Сг, т. е. Сг можио без ущерба для вывода удалить из множества дизъюнктов.

Семантическая резолюция

Одной из эффективных модификаций принципа резолюций является семан­тическая резолюция [Slagle, 1967J. В ней используется интерпретация для раз­деления множества дизъюнктов 5 на два класса; Si — непустое множество дизъ­юнктов, которое выполняется (т. е. принимает значение и) этой интерпретаци­ей, 5₂ — непустое множество дизъюнктов, которое не выполняется (т. е. при­нимает значение л) этой интерпретацией; S]LJ52=S. Разрешается резольвиро-вание дизъюнктов, принадлежащих только разным множествам, и запрещается образование резольвент от дизъюнктов, входящих в одно и то же множество. Тем самым сокращается образование ненужных дизъюнктов, так как только резольвированием из разных множеств можно получить пустой дизъюнкт.

Другим способом ограничения количества порождаемых дизъюнктов яв­ляется упорядочение предикатных букв. Если имеется упорядочение предикат­ных букв типа Pi>Pz>... >Ph, то разрешается резольвирование литеры, об­ладающей наибольшим порядком, т. е. Pi.

Определим формально семантическую резолюцию. Пусть / — интерпретация
и Р — упорядочение предикатных букв. Конечное множество дизъюнктов
{Е_и £₂,..., £_г, N), r^l, называется семантическим клашем (clash) относитель­
но Р и / (PI-клашем) тогда и только тогда, когда Ей Е%... Е_г (называемые

электронами) и N (называемое ядром) удовлетворяют следующим условиям: 1) Ей Е₂,...,Е_Г ложны в интерпретации /; 2) при Ri=N для каждого i—

= 1, 2.... г существует резольвента R_t+i, образованная из Rt и Ег, 3) резоль-

вируемая литера в Et является наибольшей предикатной буквой в Et, i— = 1, 2,..., г; 4) Rr+i ложна в интерпретации /; R_T+i называется Р1-резольвен-той, полученной из Р/-клаша {Е_и Ез,...,Е_г, N).

Вывод из множества дизъюнктов 5 называется PI-выводом тогда и только тогда, когда каждый дизъюнкт в выводе является или дизъюнктом из S, или /"/-резольвентой.

Проиллюстрируем семантическую резолюцию на рис. 2.2, задав интерпре­тацию и упорядочение предикатных букв следующим образом:

/ = {-]С(а), ~[Р(Ь), -\H(b), ЦаЬ)},

что значит С (а), Р(Ь), Н{Ь) ложны в этой интерпретации, a L(a, b) истинен и Р>С>//>1. Дерево вывода показано на рис. 2.3. Здесь {Е_и £₂, N} удовлетворяет всем четырем условиям, следовательно, является Р/-клашем, и

— /V-резольвента. Аналогично {£₃, E_ir N} является Р/-клашем и □ — />/-резольвентой.

В семантической резолюции можно использовать любую интерпретацию и любое упорядочение предикатных букв. Семантическая резолюция полна. Тео­рема о полноте семантической резолюции гласит: если Р — упорядочение преди­катных букв в конечном невыполнимом множестве дизъюнктов S, а / — интер­претация множества дизъюнктов 5, то существует Р/-вывод пустого дизъюнкта из S.

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

Дизъюнкт называется положительным, если он не содержит знаков отри­цания, н отрицательным, если каждая его литера содержит знак отрицания.

Положительной гиперрезолюцией называется специальный случай Р/-резо-люции, в которой каждая литера в интерпретации / содержит знак отрицания. Положительной она называется в силу того, что все электроны и Р/-резольвен-ты здесь положительны. Аналогично определяется отрицательная гиперрезолю­ция, у которой каждая литера в интерпретации / не содержит знака отри-надшя.

Стратегия множества поддержки была предложена в [Wos et al., 1965]. Для доказательства того, что формула В логически следует из формул F\, Ftt-./Fn, доказывалась невыполнимость формулы F_l&F2&...&F_n&~\*. Так как посылки Fi&F₂&... &F_n всегда выполнимы (истинны), то естественно запретить резольвирование литер в Fi&F2&...&F_n. Пусть S — невыполнимое множество дизъюнктов и 5j — подмножество из S, такое, что 5—Si выполнимо. Тогда под­множество Si называется множеством поддержки. Резолюция с множеством поддержки — это применение принципа резолюции к паре дизъюнктов, не при­надлежащих одновременно 5—Sj.

Все специальные случаи семантической резолюции полны.

Лок-резолюция

Идея лок-резолюции [Воуег, 1971J состоит в использовании индексов для упорядочения литер в дизъюнктах из множества дизъюнктов 5. Иными слова­ми, она включает индексацию каждого вхождения литеры с S некоторым це* лым числом; разные вхождения одной и той же литеры в S могут быть индек­сированы по-разному. После этого резольвировать разрешается только литеры с наименьшим индексом в каждом из дизъюнктов. Литеры в резольвентах наследуют свои индексы из посылок. Если литера в резольвенте мо­жет унаследовать более одного индекса, то ей ставится в соответствие наимень­ший индекс.

Например, рассмотрим следующие два дизъюнкта: 1) iP\/2R_t 2)з~1 P\ZiR> Целое число, помещенное под литерой слева,— это индекс, поставленный в со­ответствие этой литере. Так как индекс \Р меньше индекса ₂R, то разрешается

резольвировать \Р. Аналогично, так как индекс з~Т* меньше индекса \R, то можно резольвировать _Я'~\Р. Таким образом, резольвируя дизъюнкты 1) и 2) по \Р и 3*1^*. получаем дизъюнкт 3) _sRViR- Так как одна и та же литера R наследует два индекса (2 и 4), то ей ставится в соответствие наименьший ин­декс, т. е. 4) ₂R. Дизъюнкт ₂R называется лок-резольвентой исходных дизъ-♦ юнктов 1) и 2).

Отметим, что если бы литеры в дизъюнкте 2) были индексированы иначе, а именно 2)' ₄~\Р V з^> то резольвируемой литерой в этом дизъюнкте была бы з#- Однако она не резольвируется с литерой из дизъюнкта 1). Поэтому в этом случае не существует лок-резольвенты для дизъюнктов 1) и 2').

Лок-резолюция полна.

Линейная резолюция

Линейная резолюция была независимо предложена в [Loveland, 1968a, б]
и [Luckham, 1968]. Линейным выводом из множества дизъюнктов S называ­
ется последовательность дизъюнктов (Си Сч,...,С_п), в которой верхний дизъ­
юнкт Ci<=S, а каждый член Ci+u (—1, 2.. л—1, является резольвентой дизъ­
юнкта Ci (называемого центральным) и дизъюнкта В; (называемого боковым),
который удовлетворяет одному из двух условий: 1) Bi^S, (=1, 2,.... п —1;
2) Я< является некоторым дизъюнктом Су, предшествующим б выводе дизъюнк­
ту С_;, т. е. /<О". Линейный вывод имеет вид дерева (рис. 2.4).

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

Линейная резолюция может быть усилена введением понятия упорядочен­ного дизъюнкта и использованием информации о резольвированных литерах. Упорядоченным дизъюнктом называется дизъюнкт с определенной последова­тельностью литер. Говорят, что литера Ьг старше литеры Li в упорядоченном дизъюнкте тогда и только тогда, когда L₂ следует за L\ в последовательности, определенной упорядоченным дизъюнктом. Старшая (наибольшая) литера дизъ­юнкта является последней литерой дизъюнкта, а младшая литера — первой.

Если две или более литер (с одинаковыми знаками) упорядоченного дизъ­юнкта С имеют НОУ о*, то упорядоченный дизъюнкт, полученный из последо­вательности Со вычеркиванием любой литеры, идентичной младшей литере, называется упорядоченным фактором дизъюнкта С. Например, для упорядо­ченного дизъюнкта C=P(x)\/Q(x) \/Р(а) имеем а={а/х) и Со— = P(a)\/Q(a)\/P(a). Вычеркивая последнюю литеру, получаем упорядоченный фактор дизъюнкта P(a)\jQ(a).

Другим усилением линейной резолюции является использование информа­ции о резольвированных литерах. Обычно при выполнении резолюции образо­вание резольвент происходит путем удаления резольвированных литер, однако эти литеры несут полезную информацию, которая может быть использована для усиления линейной резолюции. Например, если С_г = Р{х) V Q (^х) V ~1 Ж-^х) и C_S=~]P(a)\J Q (а) —упорядоченные дизъюнкты, то конкатенация С:(а) и С₂(а), где о={а/х}, дает последовательность Р(а)\/ Q{df\/ ~\R(a)\/ "^ P (а) VQ(a).

Теперь вместо удаления Р(а) и ~] Р (а) будем оставлять в резольвенте первую из них, помечать ее (двумя вертикальными чертами) и называть об­рамленной литерой. Если за обрамленной литерой не следует никакая другая литера, то ее будем вычеркивать. Продолжая пример, получаем упорядоченную.резольвенту:

\Р(а)\ VQ

Пусть S = {P\JQ, HPVQ, P\/ ~]Q ~\Р\/ ~\Q). Линейный вывод, ис­пользующий информацию о резольвируемых литерах и понятие упорядоченного дизъюнкта, изображен на рис. 2.5, Видно, что из четырех боковых дизъюнктов три принадлежат S и один Р является центральным. Рассмотрим

Рис. 2.4

Рис. 2.5

подчеркнутую резольвенту, в которую входит литера ~| Р, являющаяся допол­нением к обрамленной литере \Р\. Данное обстоятельство указывает на необ­ходимость использования центрального дизъюнкта Р в качестве бокового. Ре-зольвнруя \P\\J\Q\\j-\PcP, получаем |P|VIQIVI1^I- Так как за этими обрамленными литерами не следует никакой другой литеры, то, вычер­кивая их, получаем пустой дизъюнкт D.

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

Алгоритм линейного вывода, применяющий как понятие упорядоченного дизъюнкта, так и информацию о резольвируемых литерах, называется OL-вы- водом (Огфгео* Linear Deduction). OL-вывод — это по существу то же самое, что в [Loveland, 1968J называется методом элиминации моделей. О/.-вывод является разновидностью линейной резолюции с функцией выбора (SL-вывод) [Kowalskf, 1971J. OL-вывод полон.

Возвращаясь к рис. 2.5, видим, что невозможно построить линейный вы­вод пустого дизъюнкта, если в качестве боковых дизъюнктов брать только дизъюнкты из исходного множества S. Назовем дизъюнкты множества 5 входными дизъюнктами. Тогда резолюция, у которой хотя бы один из двух дизъюнктов является входным, называется входной резолюцией. Входная ре­золюция проста и эффективна, но, как видно из рис. 2.5, не полна. Однако существует специальный класс так называемых хорновских дизъюнктов (см. § 1.2), для которых входная резолюция полна. Дизъюнкт называется хорнов-ским, если он содержит не более одной положительной литеры. Входная резо­люция является логической основой для языка логического программирования Пролог [Clocksin et al., 1981].

Поиск по сайту: