Конгруэнции на термах и унификация тема автореферата и диссертации по математике, 01.01.09 ВАК РФ

г О

| ,1

российская академия наук вычислительный центр

На правах рукопйси

Гавриленко Юрий Вячеславович

. конгруэнции на термах и унификация

Специальность 01.01.09 — магматическая кибернетика

автореферат

диссертации на соискание ученой степени кандидата физико-математических наук

москва - 1991

Работа выполнена ■ Вычислительном центре Российской Академии наук

Научный руководитель! кандидат физико-1

ских

наук старший научны) сотрудник Николай Макарович Нагорный

Ведущая организация! Институт системного анализа РАН,

на заседании специализированного совета К. 002.12.01 при Вычислительном центре РАН по адресу! 117967, Москва, ГСЛ-1, уп. Вавилова, 40.

С диссертацией можно познакомиться • библиотеке Математического института им. В.А. екпоеа РАН

Официальные оппоненты: доктор физико-математических наук Владимир Борисович Бореев

доктор физико-математических наук Александр Яковлевич Диковский

Зашита состоится *

Ученый секретарь специализированного совета К.ооа.эа.01 при вц ран,

доктор физико-математических наук

К.В. Рудаков

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

АКТУАЛЬНОСТЬ ТЕМЫ.

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

Метод решения уравнений в термах - унификация - был найден Э. Постом и Ж. Эрбраном уже на раннем этапе развития математической логики. Однако интенсивное изучение приемов унификации и их широкое применение началось лишь после знаменитой работы Дж. Робинсона [1], положившей начало машинному алгоритму автоматичес- • кого поиска доказательств теорем. - принципу резолюций, стержнем которого стала унификация.

Усилия исследователей в этом направлении привели к созданию теории унификации или точнее теории уравнений в термах - новой математической дисциплины, использующей методы алгебры и логики. Исчерпывающий обзор основных достижений й ретроспективный анализ , истории развития этой теории представлен в ста-, ье Й. Зикмана [2].

Теория уравнений в термах - яркий пример успешного взаимодействия информатики и математики, в итоге которого математика обогатилась постановками новых глубоких теоретических проблем, родившихся в недрах прикладных исследований, а информатика получила точные методы их решения. Применения методов унификации в инфор> тике многообразны и зачастую неожиданны: экспертные и диагностические системы, машинное зрение, компьютерная алгебра, автоматический поиск вывода формул, математическая лингвистика, проектирование трансляторов, обучающие системы - вот далеко не

полный перечень дисциплин, где приложения унификации оказались плодотворны. Глубоки и интересны "внутриматематические" применения унификации, например, в теории доказательств [3].

Но главное поле этих приложений, постоянно рождающее новые неисследованные проблемы, - это, конечно, логическое программирование, прогресс которого прямо зависит, от совершенствования стратегий "поиска по образцу" и алгоритмов унификации.

Теория уравнений в термах с полным основанием считается фундаментальным разделом теоретической информатики, во многом определяющим ее современное развитие.

ЦЕПИ РАБОТЫ.

Задача унификации в исчислениях равенств заключается в следующем. Фиксируем n = < Var, Con, Га, « ) - произвольную алгебраическую сигнатуру, содержащую счетное множество переменных, множество констант, множество функциональных символов и символ равенства. Совокупность тт(П) термов рассматриваемой сигнатуры задается обычными индуктивными правилами:

1. Если t - переменная или константа, то teTn(ft).

2. Если feFn - функциональный символ валентности п>0, tx, t2,..., tneTm(n), то f(t1( t2,... ,tn) сТш(П).

Термы графически представимы конечными деревьями, вершины которых помечены переменными или константами сигнатуры, а внутренние вершины - функциональными символами. Размеченные сходным образом бесконечные деревья, содержащие конечное число различных поддеревьев, также рассматриваются в теории унификации и называ- ' ются регулярными деревьями.

Пусть Е - произвольное исчисление равенств, т.е. совокупность аксиом, каждая из которых имеет вид Vxx—xm(p=q), где

p,qeTm(n), а x1(___,11, - полный список переменных, входящих в р

и q. Два терма t и s связаны в Е отношением эквивалентности =g, если формула t=s выводима из аксиом Е в логике первого порядка с равенством. Если Г - конечная система уравнений в термах: '

г « { tL - Si | isisn, tLl s± £ Tm(íí) }, то финитная (т.е. имеющая конечную оОласть определения) подстановка а: Уаг -» Ти(П) называется унификатором (т. е. решением) Г, если otL =г ctsí для всех lsisn.

Унификатор о называется самым общим унификатором Г (в другой терминологии - наиболее общим унификатором), если <т <Е ó' для любого ее унификатора а' (т.е. если существует такая подстановка X, что a't =в kot для всех teTm(n)).

Основные вопросы, связанные с унификацией в Е, таковы:

1) всякая пи система уравнений г имеет унификатор ?

2) всегда пи разрешимая система уравьзний имеет самый общий унификатор ?

3) как устроено многообразие самых общих унификаторов г (т.е. как они связаны друг с другом ) ?

4) какие системы уравнений в термах Е-эквивалентны, т. ё. имеют одни и те же решения ?

Если для исчисления Е отношение совпадает с графическим равенством термов, то задача унификации для % называется классической.

Группа французских математиков, возглавляемая создателем языка ПРОЛОГ Д.-Копмероэ, исследовала обобщение классической задачи на случат алгебры регулярных деревьев R(F) [4 -7]. При таком обобщении решение системы уравнений в термах Г ищется не в свободной алгебре конечных термов ти(П), а среди регулярных деревьев, т.е. унификаторами г яогяотся отображения о: Уаг - R(F),

приравнивающие все пары термов из Г. В более общем случае и сама система г тоже может состоять из равенств регулярных деревьев.

Такое "нестандартное" определение унифицируемости помимо своей математической естественности мотивируется уже тем, что все ' практические версии языка ПРОЛОГ используют не оригинальный алгоритм унификации [1], а- лишь его "урезанный" вариант (без проверок вхождения переменных), реализующий (некорректное) понятие унифицируемости, близко напоминающее унификацию в >|1) (см. [1*, 8]).

Исследования группы Колмероэ увенчались разработкой нового языка логического программирования ПРОПОГ-т, основанного на унификации в бесконечных регулярных деревьях [7].

Однако унификацию в регулярных деревьях вряд ли можно признать вполне удовлетворительной хотя бы потому, что уравнения и х=1 (£(х)), интуитивно воспринимаемые как безусловно •различные, оказываются эквивалентными в алгебре так как

имеют одно и то же (единственное) бесконечное решение: х = f(í(f( ...£(...)...))).

Одна из побудительных причин настоящего исследования заключалась в стремлении модифицировать унификацию так, чтобы появилась возможность семантически разграничивать уравнения, подобные х=£(х) и х=£ (£(х)) . (Другая причина состояла в стремлении обобщить унификацию на случай бесконечных систем уравнений в термах.

Между тем, осуществить поставленные щ л средствами,- .уже имевшимися в арсенале теории унификации, оказалось невозможным, поскольку все хорошо известные методы решения систем уравнений в термах, изпоженные, например, в работах [1, 9 - 12), существенно опирались на конечность рассматриваемых систем и непосредственно не обобщались на бесконечный случай.

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

что само понятие унифицируемости нуждается в радикальном измене-нии. Именно, вместо унифицирующих действий (выбора, подстановки и последующего графического сравнения получившихся термов)•следует рассматривать конгруэнции на термах - отношения эквивалентности между термами, удовлетворяющие ряду естественных дополнительных Условий, которые по существу ако оматизируют важнейшие свойства унификации.

Кроме таких конгруэнций-модепей бескон жых систем уравнений в термах п диссертаци исследованы и обычные унификаторы-подстановки (естественно, нефинитные, для которых также пришлось-создать нов'ый математический аппарат [4*.- б*]).

Был выделен и иследован важный в приложениях подкласс самых общих решений систем уравнений в термах - главные решения, удовлетворяющие свойству идемпотентности [2*, з*].

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

1) исследовать конгруэнции на тепмах в качестве-алгебраических моделей-унификаторов ■ для Систем уравнений в термах,

2) изучить свойства решений произвольных - как конечных, так и зсконечных - систем уравнений в термах,

3) описать строение главных решений произвольной системы уравнений в термах.

НАУЧНАЯ ' НОВИЗНА.

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

генетически связано с понятием упрощаемого и когерентного бинарного отношения, вскользь упоминаемого в работе [4]. Заметим также, что употребление термина "конгруэнция" в диссертации не вполне соответствует апгебраической традиций (см., например, [14]). Частный случай утверждения з.ю.14 для конечных систем уравнений в термах установлен в-[13] и независимо автором в работе [2*].

ТЕОРЕТИЧЕСКАЯ И ПРАКТИЧЕСКАЯ ЦЕННОСТЬ.

Результаты диссертации могут быть использованы в исследованиях по погическому программированию. Наиболее перспективным представляется применение унификации бесконечных систем уравнений в термах к проблемам -теории неограниченно продопжающихся логических вычислений [12].

■АПРОБАЦИЯ РАБОТЫ И ПУБЛИКАЦИИ.

Отдельные части исследования докладывались -в 1988 г. на Всесоюзном семинаре "Семиотические аспекты формализации интеллекту. апьной деятельности. Боржоми-88" [1*] и на Второй всесоюзной конференции "Прикладная логика" [2*]. В 1991 г. результаты диссертации были доложены на Вторых математических чтениях памяти М. Суслина [4*]. •

Отдельные результаты диссертации излагались в 1989 г. на семинаре по математической логике кафедры математической логики МГУ. В полном виде доказательства всех результатов диссертации были заслушаны в 1988 - 1992 гг. на семинаре "Математическая логика й информатика" (Вычислительный центр РАН, Москва).

По теме диссертации автором опубликовано б работ [1*.- 6*]. Основные результаты изложены в [3*], [5*] и [6*].

СТРУКТУРА И ОБЪЕМ РАБОТЫ.

Диссертация состоит из введения, трех глав, .заключения, списка литературы (24 наименования) и приложения, включающего индекс ключевых слов и обозначений. Диссертация содержит'' 147 страниц основного текста и 7 страниц приложений.

СОДЕРЖАНИЕ РАБОТЫ

Основные результаты исследования сосредоточены в заключительной третьей главе диссертации. В двух первых главах, которые носят в основном технический характер, развиТ"; новый математический аппарат, созданный специально для исследования конгру-лнций на термах, неограниченных подстановок и bec энечных систем уравнений в термах.

Теперь изложим по порядку .основное содержание всех глав диссертации. '■

В первой главе диссертации разработаны математические методы исследования неограниченных подстановок. В первом разделе главы введены понятия диаграммы терма, внутреннего и внешнего узла т.ерма, описывающие графическую структуру терма. В следующем разделе йсследуется семейство sub(n) всех неогрании,5нных подстановок вида a:Var -» Тш(П). Определены множества, характеризующие произвольные подстановки! Don((j), Ii..(<j), Rng(o) - области задания, изменения и значений подстановки а. Установлен ряд новых теоретико-множественных соотношений' для областей композиции подстановок. Третий раздел.главы посвящен новому важному для теории унификации бесконечных систем уравнений понятию квазиперестановки.

• Пусть X - подстановка в сигнатуре П. Подстановку фсвиЬ(П) будем называть квазиперестановкой для X', если выполняются следующие требования:

1) ftRng(X) : Var - Var,

2) отображение $ инъективно на области Rng(Á). Важнейшее свойство квазиперестановок - их "квазиоЬратимость":

Если для подстановок о и X справедливо равенство о - $*Х, где $ - некоторая квазиперестановка_ дляХ, то существует н -квазиперестановка для а такая, что Л - н'о.

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

. Пусть о,Л - произвольные подстановки сигнатуры п. Будем говорить, что подстановка.о мажорирует X (X меньше а, А<а), если существует подстановка eesub(U) такая, что а = е»А. Аналогично определяется отношение неравенства между термами: t<s « Эге8иЬ(П).в - rt (t,seTn(n)). Получен следующий результат:

Пусть сигнатура п содержит по крайней мере один функционапь- ' ный символ валентности большей 1, тогда для любых подстановок X,aesub(а) справедлива эквивалентность:

X ¿ о - \/teTm(Cl) .Xt й ot. Исследована связь неравенства Xso подстановок Л и а со всевозможными неравенствами их ограничений на конечные подмножества Wcvar:-Пу ть X и а - любые подстановки в произвольной сигнатуре п,.

а последовательность множеств И0,н1гн2,... с Var удовлетворяет • * '

условию: для любых двух х¡,x¡evar существует такое натуральное azoj sго xj,x2ewm. Тогда, если при каждом níO справедливо неравенство X IWn s о Мп* то isa.

Во второй главе введено основное понятие диссертации -

понятие конгруэнции на термах. Бинарное отношение эквивалентности между термами - мы называем конгруэнцией, если для функциональных символов f,geFii(n) валентности пиши для произвольных термов t1(s1(...,tn,sneTB(n) выполняются.следующие условия:

1) t¡~3 J,..., t„~snt4=2> í(tj,...,ta) ~ f(Sj,...,Sn),

2) если f(t1,...,tn)~g(s1,...,sa), то n - ш и f=g,

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

Если o:vаг -» Tm(n) - произвольная подстановка в сигнатурё п, то бинарное отношение между термами, задаваемое условием

. t в - at = as ( t,seTa(íl) ), является конгруэнцией, которая будет называться конгруэнциейf порожденной подстановкой о.

Ограничение конгруэнции - на множество переменных W с var является конгруэнцией и определяется следующими свойствами:

1) если Var(t) си, rot~IW з - (t~s) Л (Var(s).^W),

2) если (Var(t) и Var (в)) n я, то t - !И s - t = а.

Во втором разделе описан способ явного задания конгруэнций -с помощью согласованных отображений. В следующем разделе по аналогии с областями Dora и im подстановок введены множества переменных, сходным образом характеризующие произвольную конгруэнцию. Так, например, область задания конгруэнции - определяется условием xeDom(-) - 3teTa(n). t+x Л x-t, а область значений -'условием х«1п(~) - 3yeVar3teTa(n).y#tAy-tAxeVar(t).

Доказано, что из конечности области задания любой конгруэнции следует конечность ее области значений. Исследованы свойства ограниченных конгруэнций (имеющих конечную область задания).

В последнем разделе изучено отношение неравенства между кон-груэнциями. В частности, установлено, что если т - произвольная,

а о - идемпотентная подстановка, то неравенство между подстановками айт эквивалентно неравенству конгруэнций s ~т.

первых двух разделах заключительной третьей главы диссертации исследованы свойства отношения зависимости термов в произвольной конгруэнции -:

t >-* в - ЭТеТ»(П) (t-T Л (в - подтерм Т) Л в*Т ).

Терм t непосредственно зависит от в в если t >•* в и не существует такого терма q, что t >* q и q >•* s.

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

В третьем разделе этой главы определены понятия фундированно-сти терма и переменной: терм t фундирован относительно >* , еспи конечна любая убывающая последовательность термов вида: t >•* tx t2 >-*...>* tn >-*... . Изучена связь свойства фундированности с понятиями ограниченной и предельной разложимости термов, определяемыми в том же разделе.

В следующих разделах (4 и 5) исследовано важнейшее свойство фундированности конгруэнций. Конгруэнция - называется фундированной, еспи не существует бесконечно убывающих цепочек зависимостей термов вида t0 >■* ta >■* t2 >•* ... .

Один из основных результатов диссертации представлен теоремой о порождении фундированной конгруэнции идемпотентной подстановкой:

Пусть — произвольная фундированная конгруэнция в сиги туре п, и на множестве ее нулевых переменных Var0(~) определено некоторое отображение t:Var0(~) -> Var, при всех x,ytVar0(~) удовлетворяющее условиям: а) х ~ fx, Ь) х ~ у - фх = fy. Тогда существует (и притом единственна) подстановка теЗиЬ(П),

обладающая следующими свойствами: 1) а2 = а (а - идемпотент) ,

2) ~ совпадает с (~ - , 3) ох = для всех хеУаг0(~).

В шестом разделе введена группа автоморфизмов конгруэнции: и-Аи<:(~) => { пеРога | УхеУаг.х-ях }.

Установлено, что все идемпотенты, порождающие какую-нибудь конгруэнцию, подобны относительно этой группы :

Если идемпотенты ог, о2 порождают одну и ту же конгруэнцию то найдется автоморфизм тгеи-АиЬ (~) , для которого выполняются следующие условия: 1) и'1 - и ; 2) <т2 » °а1°тт = я"1»'а1 /

3) при всех хеУаг справедливо соотношение х - пх. Определены также другие группы автоморфизмов конгруэнций и

изучены их алгебраические свойства (разделы б и 7).

Восьмой раздел посвящен исследованию строения произвольных конгруэнций. Установлено, что всякая конгруэнция разбивается на фундированную и нефундированную части, зная которые можно восстановить исходную конгруэнцию. Точная формулировка основного результата (теорема з.8.и) воспроизводится ниже.

' Разработанная в предыдущих разделах диссертации теория конгруэнций применена к теории унификации конечных и бесконечных систем уравнений в термах (разделы 9 и Ю последней главы). .

Введено понятие модели системы уравнений 2 - так в диссертации названы конгруэнции в которых эквиваленты термы каждого разенства системы: для любого равенства системы е.

Системы уравнений, имеющие модель, названы квазиуинфицируемыми.

Доказано, что всякая квазиуйифицируемая система £ обладает минимальной моделью -1, удовлетворяющей неравенству 5 - для любой другой модели -.

Исследована связь между решениями-подстановками и моделями систем уравнений в термах. Так, например, показано, что подста-

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

I Таким образом, обычная проблема унифицируемости произвольной системы уравнений в термах сведена к вопросу о возможности порождения ее моделей подстановками.

Доказано, что произвольная система уравнений унифицируема в том и только в том случае, когда она имеет фундированную модель.

Для самых обших решений произвольной унифицируемой системы уравнений в термах Е получен следующий результат:

Если т, т' -самые общие решения £, то найдется такая квазиперестановка для т что т' » г.

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

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

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

Г - конечная подсистема 2 Ьг(х) <, ых (под высотой переменной х в системе г понимается наибольшая длина начинающихся с X убывающих цепочек зависимостей переменных в минимальной модели I).

Следующие результаты яопяатся центральными в диссертации:

а). Утверждение, характеризующее свойство отношений зависимости между термами:

Теорема 3.4.7. В произвольной конгруэнции каждый терм непосредственно зависит лишь от конечного числа попарно неконгруэнтных термов.

б). Теорема о строении фундированных конгруэнции:

Теорема 3.5.6. 1. Каждая фундированная конгруэнция порождается некоторым идемпотентом.

2 . Ограниченная фундированная конгруэнция порождается ограниченным идемпотентом.

в). Результат о разложении произвольной конгруэнции:

Теорема 3.8.11. Для любой конгруэнции ~ существуют такие множества переменных V и к, что выполняются следующие условия:

1) -IV - наибольшая фундированная часть

2) V ПК с Уаг, (~) ;

3) для любого множества переменных и, содержащего и, и произвольного идемпотента а, порождающего конгруэнцию - IV, справедливо равенство: - « [~ Ю]° .

г). Критерий унифицируемости систем уравнений:

Теорема з.ю.з. 1. Произвольная квазиунифицируемая система уравнений в термах унифицируема в том и только в том случае, когда она фундированна.

2. Произвольная система уравнений унифицируема тогда и только, тогда, когда она имеет фундированную модель. ■

д). Результат о строении'множества главных решений унифицируемых систем уравнений в термаЯ:

Теорема з.ю.17. Если 2 - унифицируемая система уравнений а-термах, а о¡,р2е!(Ъ) - ее произвольные главные решения, то най-

дется такой нулевой автоморфизм этой системы леАиЬ0(£), что справедливы следующие равенства:

1) тг'1 » Я, 2) о2 ' 1Г~1°01°П = л~1°о1.

ЗАКЛЮЧЕНИЕ

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

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

Исследована морфология произвольных конгруэнции на термах (теоремы о выделении фундированной части).

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

Исследован класс главных решений систем уравнений в термах.

С помощью введенных групп симметрии систем уравнений в термах описано строение многообразия самых обших и гпавних решений произвольной системы уравнений. Изучено строение групп симметрий систем уравнений в термах. Исследовано понятие эквивалентности систем уравнений в термах. Установлены критерии унифицируемости бесконечных систем уравнений в термах .

ЛИТЕРАТУРА

1. Robinson J. A. A Machine Oriented Logic Based on the Resolution Principle // J. of the ACM. - 1965, v. 12, Ко. 1, - p. 23

- 41.

Имеется русский перевод:

Робинсон Дж. Машинно-ориентированная логика, основанная на принципе резолюций // Кибернетический сборник (Новая серия), 7 -М.: Мир, 1970. - С. 194 - 218.

2. Siekraann J. Н. Unification Theory // J. Symbolic Computation. - 1989, V.7, No. 3S4. - p. 207 - 274.

3. Pudlak P. On a Unification Problem related to Kreisel's Conjecture // Commentationes Mathematicae Universitatis Carolinae. - 1988, v. 29, No. 3. - p. 551 - 556.

4. Courcelle B. Fundamental Properties of Infinite Trees // Theoretical Computer Sei. - 1983, v. 25, No. 1. - p. 95 - 163.

5. Common H., Lescanne P. Equational Problems and Disunification // J. Symbolic Computation. - 1989, v.7, No. 3S4. - p. 371

- 425. ' -

6. Colmerauer A. Equations and Inequations on Infinite Trees // Proc. Int. Conf. of FGCS 1984. ICOT. - Tokio. - 1984",

- p. 85 - 99.

7. Colmerauer A. An Introduction to PROLOG-III // Comms. of the ACM. - 1990, v. 33, No. 7.

8. The Occur Check. Net Talk // Logic Programming. Newsletter of the Association for Logic Programming. - 1993, v. 6, No. 2. -p. 14 - 19.

9. Martelli A., Montanari U. An Efficient Unification Algorithm // ACM Transactions on Programming Languages and Systems.' - 1979, v. 4, No. 2. - p. 258 - 282.

10. Paterson M., Wegman M. Linear Unification // J. of Computer and System Sciences. - 1978, v. 16, No. 2 - p. 158 - 167.

11. Venturini-Zilli M. Complexity of the Unification Algorithm for First Order Expressions // Calcolo. - 1975, v. 12, No. 4. - p. 361 - 371.

12. Lloyd J. W. Foundations of Logic Programming, 2nd ed. -Springer-Verlag, Berlin, New York, London. - 1987. - XII+212 pp.

13. Lassez J. L., Mäher M. J., Marriott K. G. Unification Revisited // Lecture notes in Computer Sei. - 1988, v. 306. - p. 67 - 113.

14. Кон П. Универсальная алгебра. - M. : Мир, 1968. - 352 с.

15. Plotkin G. D. A note on Inductive Generalization /./ Machine Intelligence' 5. B. Meitzer, D. Michie Eds. - University Press. Edinburgh. - 1969. - p. 153 - 163.

16. Plotkin G. D. A Futher Note on Inductive Generalization // Machine Intelligence' 6. B. Meitzer, D. " Michie Eds. University Press. Edinburgh. - 1971. - p. 101 - 124.

17. Plotkin G. D. Building-in Equational Theories // Machine Intelligence' 7. B. Meitzer, D. Michie Eds. - University Press. Edinburgh. - 1972. - p. 73 - 90.

18. Eder E. Properties of Substitutions and Unifications // J. Symbolic Computation. - 1985, v.l, No. 1 - p. 31 - 46.

РАБОТЫ АВТОРА ПО ТЕМЕ ДИССЕРТАЦИИ

1*. Гаврипенко Ю. В. Унификация в ПРОЛОГЕ: машинные эксперименты // Семиотические аспекты формапизации интеплектуапьной деятельности. Всесоюзная школа-семинар "Боржоми - 88". Тезисы докладов и сообщений.- Москва, 1988. - С. 35 - 39.

2*. Гаврипенко Ю. В. Группы автоморфизмов систем уравнений в термах // Прикладная логика. Вторая всесоюзная конференция. Тезисы докладов. - Новосибирск, 1988. - С. 38.

3*. Гаврипенко Ю. В. Главные решения и группы автоморфизмов систем уравнений в термах // Доклады АН СССР. - 1989, т. 309, N 3. - С. 524 - 528.

4*. Гаврипенко Ю. В. О строении фундированных конгруэнций на термах // Вторые математические чтения памяти М. Суслина. Тезисы докладов. - Саратов, 1991. - С. 31.

5*. Гаврипенко Ю. В. Конгруэнции на термах и свойства отношений зависимости между переменными // Доклады Академии Наук. -

1992, Т. 323, N 3. - С. 389-393.

6*. Гаврипенко Ю. В. Строение фундированных конгруэнций и унификация бесконечных систем уравнений в термах // Доклады Академии Наук. - 1993, т. 329, N 2. - С. 128 - 131.

МОСКОВСКИЙ ИНСТИТУТ СТАЛИ И СПЛАВОВ

Заказ Л Объем / О Тираж /с"с Типография ШСиС, ул.Ордаоыикидзе, 8/9