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

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

МАРТЬЯНОВ ВЛАДИМИР ИВАНОВИЧ

РГ 5 ОД

о

ЛОГИКО-ЭВРИСТИЧЕСКИЕ МЕТОДЫ ПОИСКА РАЦИОНАЛЬНЫХ РЕШЕНИЙ ПРИКЛАДНЫХ И ТЕОРЕТИЧЕСКИХ ЗАДАЧ -.....

05.13.16 - применение вычислительной техники, математического моделирования и математических методов в научных исследованиях

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

Автореферат

Иркутск - 1996

Работа выполнена в Иркутском вычислительном центре СО РАН

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

на заседании Диссертационного Совета Д 063.32.04 по защитам диссертаций на соискание ученой степени доктора наук в Иркутском государственном университете по адресу:

6С4003, г.Иркутск, бул.Гагарина, 20.

С диссертацией можно ознакомиться в библиотеке Иркутского государственного университета (бул.Гагарина, 24)

Автореферат разослан "2£" 1996 г

профессор Егорычев Г.П.

доктор физико-математических наук, профессор Пинус А,Г.

доктор технических наук, профессор Тятюшкин А.И.

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

Москва

Защита состоится оо^й-Я года в "/У^ас.

час.

Ученый секретарь Диссертационного Совета, доцент

Н.Б.Бельтюков

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

Аетхальность_темыисследований. В настоящее время широко известно важное значение логических методов для применения вычислительной техники в научных исследованиях^ и решении практически значимых задач. Наиболее известными в этом направлении являются применения•логических методов в практике создания языков программирования, экспертных систем и решении комбинаторных проблем большой сложности.

Универсальность языка логики к универсальность средств решения (вывод), сформулированных на языке логики задач, определяют принципиальное значение логики для решения "плохих" проблем и создания мобильных технологий проектирования-программного обеспечения для различных предметных областей. Понимание универсальности языка логики для математики породило в начале XX века логицизм (Б.Рассел, Д.Гильберт и др.) -направление, пытавшееся уложить всю математику в рамки логики. В настоящее время происходит как бы возрождение логицизма, но не для достижения целей собственно математики, а для приложений з различных областях техники и сферах жизни.

Расширение сфера влияния логики происходит за счет широкого применения экспертных систем (от систем советов домохозяйке до систем поддержки принятия политических решений), которые, как правило, содержат блок вывода. Кроме того, появление коммерческих интегрированных систем логического программирования (типа Турбо-Пролог) включило довольно широкий круг программистов в число людей, использующих логику (хотя и в утилитарной форме). Логические методы успешно применяются для решения комбинаторных проблем большой сложности (подкласс №-полных задач).что позволило решать практически важные задачи теории расписаний. Например, состав-

л ять расписания электричек для Бельгии, расписания полетов и обслуживания техники для компании "йофтгаяза".

Если широко смотреть на данную работу, то ее основу со-стзляют три взаимосвязанных направления:

I) построение формализма более адекватно отражающего способы доказательства теорем содержательной математики, чем классические логические исчисления*

2} программная реализация построенных методов для решения теоретических и прикладных задач*

3) построение и доказательство существования алгоритмов решения массовых алгоритмических проблем.

Первое направление своим истоком имеет исследования по логике. Построение языка логических исчислений, начатое Дж". Булем, было завершено Г.Фреге. Большая выразительная сила созданного языка исчисления предикатов была подтверждена рядом исследователей - Дж.Пеано (система аксиом арифметики), Е.Цермело (система аксиом теории множеств) и др.

Д.Гильберту и его школе принадлежит создание основного (в современном понимании) логического исчисления, а именно. . исчислел.ад предикатов первого порядка. Это исчисление содержит не только формальный логический язык, но также фактически, задаваемую правилами вывода, полуразрешзющую алгоритмическую процедуру (Д.Гильберт, ВДккерман [9], Д.Гильберт П.Бернайс 110]), которая-принципиально обеспечивает установление выводимости для любого доказуемого утверждения (во не проявляет признаков положительного или отрицательного ответа на этот вопрос для остальных утверждений). Это наиболее наглядно связывает первое и третье направления диссертации. Отметим. что широко известные методы автоматического' доказательства теорем (АДТ): метод резолюций, обратный метод Мас-лова, алгоритм очевидности, используют гсолурззрешакицие про-

цедуры, идущие от соответствующих логических исчислений [14, 25, 361.

Нетрудно видеть, что на языке логик достаточно высоких порядков можно записать любые математические утверждения. Однако это можно сделать уже на языке исчисления предикатов первого порядка, что составляет содержание известного тезиса Гильберта [38].

Тезис Гильберта становится более ясным, если использовать язык многосортного исчисления предикатов для многоосновных моделей. Построение многосортного исчисления -предикатов начато А.Шмидтом, а первые наиболее яркие приложения получены А.И.Мальцевым [19]. Формализм алгебраических систем и расширение многосортного исчисления предикатов с помощью типовых условий для кванторов использовался в работах академика В.М.Матросова и С.Н.Васильева по синтезу теорем о динамических свойствах нелинейных систем [3-7, 26 - 28, 56]. В работах В.М.Матросова и С.Н.Васильева, видимо, впервые были получены на ЭВМ содержательные теоремы (сравнимые с публикуемыми в математических журналах).

Появление вычислительной техники позволило перевести вопрос реализации систем логического вывода и эвристических троцедур проверки истиности (или их комбинации) в практичес-сую плоскость (второе направление работ диссертации). Начало 5ыло положено классической работой А.Ньюэлла, Дж.Шоу и Г. Саймона [53] по созданию эвристической программы для доказательства теорем исчисления высказываний. Дальнейшее продви-кение связано с открытием Дк.Робинсоном принципа резолюции 36], разработкой С.Ю.Масловым обратного метода [25], рабо-•ами по созданию формального языка для записи математических ■еорий и алгоритма очевидности [ 12 ]. Интенсификация иссле-[ований в данной области связана с появлением языков логи-еского программирования С 18, 42 ] и экспертных систем.

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

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

1. Программная система "1огик-теоретик",1957г., авторы: А.Ньюзлл, Дж.Шоу и Г.Саймон. Доказательство теорем исчисления высказываний [53].

2. Программные системы "Программа I, II, III", i960, автор: Ван Хао. АДТ исчисления предикатов [57].

3. Обратный метод, 1964, автор С.Ю.Маслов. АДТ исчисления предикатов [25].

4. Программная система "А.ЛПЕВ-ЛОМИ-2", 1965, авторы: Н.А.Шанин, С.Ю.Маслов, Г.В.Давыдов и др. АДТ исчисления высказываний [41, 42].

5. Метод резолюций, 1965, автор: Дж.Робинсон. АДТ исчисления предикатов [36].

6. Программная система "Доказатель Бойера-Мура" и идеи реализации метода резолюций, 1972, авторы: Р.Бойер, Дж.Мур. АДТ исчисления предикатов [50].

7. Алгоритм очевидности и программная система САД, 1972, авторы: В.М.Глушков, Ю.В.Капитонова, А.А.Летичевский и др. АДТ исчисления предикатов [ II 1.

8.Программная система "Язык логического программиро- • вания ПРОЛОГ1', 1973, авторы: А.Колмероэ и др. Язык программирования с решателем задач, описанных хорновскими дизъюнктами [;47].

9. Программная система "Доказатель теорем Техасского университета", 1974,. авторы: В.Бледсоу, П.Брюэлл. и др. АДТ исчисления предикатов [44, 45].

10. Доклад Р.Ковальского на Конгрессе 1Г1Р, 1974. Обоснование логического программирования [50].

11. Программная система : Эдинбургский пролог, 1977, автор: Д.Уоррен. Язык программирования с решателем задач, описанных хорновскими дизъюнктами, [ 58 ].

12. Метод сравнения и программная система синтеза теорем, 1978, авторы: С.Н.Васильев, В.М.Матросов и др. Синтез теорем о динамических свойствах нелинейных систем [26 - 28].

13. Японский национальный проект. ЭВМ 5-го поколения, 1979,авторы: Т.Мото-ока и др. Системы обработки информации, заключенной в накопленных знаниях, I 49 1.

14. Программные системы:- AURA " к LMA, 1982, авторы: Л.Воз, Э.Ласк и др. АДТ исчисления предикатов и решение прикладных задач, I 52, 59 ].

15. Проект развития систем логического вывода МККР, 1984, авторы: К.Раф и др. АДТ исчисления предикатов

[ 54 ] .

16. Семантическое программирование, 1985, авторы:

С.С.Гончаров, Д.И.Свириденко. Концепция программирования, основанная на формульном описании вычислимых функций [13].

17. Метод удовлетворения ограничениям в логическом программировании и система решения прикладных задач, 1989, авторы: П.ван Хентенрюс и др. Методы ориентированные на решение комбинаторных проблем большой сложности 148). Решение практически важных задач теории -расписаний большой размерности.

2§ль_работы. Разработка формализма для моделирования математического-мышления, построение логических исчислений, ориентированнных на создание' систем автоматического доказательства " теорем, проведение исследований по определению свойств построенных логических исчислений (полнота, область-конструктивной работы, корректность и др.).

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

Построение и доказательство существования алгоритмов решения массовых алгоритмических проблем.

Метода_исследований. Б работе используются методы математической логики, дискретной нетеыатики, теоретической кибернетики, теории моделей и математической теории логи ческого вывода.

" 0§Х55§€^овизна.г Все основные результаты диссертации, ямшггся новыми и опубликованы в работах автора. В диссертации предлагается новый метод автоматического доказательства теорем ( метод инвариантных преобразований ), отличающийся по своим свойствам {сложность, область конструктивной работы и пр.) от других методов.

Приведены программные реализации метода инвариантных

преобразований (система АВТОДОТ) и логико-эвристических методов (системы КАРАТ1, КАРАТ2, АВТОР), успешно решающие прикладные и теоретические задачи.

Для двух массовых алгоритмических проблем проведены исследования их разрешимости.

Праететеская_и_теоретотеская_ценность. Методы автоматического доказательства теорем предназначаются для проверки истинности тех или иных классов формул исчисления предикатов, причем эти метода ориентированы на реализацию на ЭВМ (в этом их отличие от классических логических исчислений). Сразу же .отметим, что "универсального" метода-АДТ (проверяющего истинность любых формул исчисления предикатов) нет, так как данная массовая алгоритмическая проблема неразрешима. В силу этого нужен целый спектр методов , имеющих какие-либо преимущества для тех или иных целей.

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

. Программная релизация метода (система АВТОДОТ) успешно опробована на решении ряда теоретических и прикладных задач, что подтверждается актом сдачи программной системы межведомственной комиссии и актами внедрения от в/ч 01168 и в/ч 19161.

Программные реализации логико-эвристических методов (системы КАРАТ! и КАРАТ2) ориентированы на решения задач распознавания ситуаций в условиях неполной информации и для организации взаимодействия должностных лиц в условиях жестких временных ограничений. Успешная работа данных систем подтверждена справкой от в/ч 01168.

• Программная реализация логико-эвристических методов

система АВТОР для проектирования расписаний вузов успешно работает в Иркутском техническом университете, что подтверждено актом об передаче в опытную эксплуотацию.

Апробация .работы. Результаты диссертации излагались на . \ТШ Международном конгрессе по 'логике, философии к методологии науки (Москва, август, 1987), на ряде Всесоюзных конференций по алгебре (1971-1990г.г.на всех Всесоюзных и медународных конференциях по прикладной логике (Новосибирск, 1985-1992 г.г., Иркутск, 1995г.). на vil и Ш Всесоюзных конференциях "Проблемы теоретической кибернетики" (Иркутск, 1985; Горький, 1988), семгаарах отделов Ш СО,АН СССР 11975 -90 г.г.), Ш РАН (1981-94 г.г.)Г ВЦ АН Арм.ССР (1987 г.). ЛОШ АН СССР (1980-1986 г.г.), семинарах МГУ(1982-1989г.г. ), кафедры алгебры, логики и кибернетики ИГУ (1972-1995 г.г.), на семинарах КрВЦ СО РАН (1977-1995 г.г.).

Публикации. Основные результаты диссертации опубликованы, в работах tl-15l, список которых приводится в конце автореферата.

С1ЩК1ХВ§_и_°£ьем_работы. Диссертация разбита на два тома Первый том состоит из введения и первой главы. Второй том.- -состоит из второй и третьей глав, заключения и списка литература. Введение разбито на 4 параграфа, первая глава -на 5, вторая глава - на 3, ' третья - на 4:'Объем работы' -,293 страницы. Список литературы содержит 181 наименование.

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

Во введении приведена краткая характеристика направлений работ, которым посвящена диссертация..Приведены . необхо-

даже сведения из математической логики. -

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

Теорана 1.1-1.6, дающие достаточные (а иногда и необходимые) условия корректности различных типов преобразований-формул МШ1, ножно разделить на две группы.

. Теоре.ча первой группы утверждают, что преобразование (того кяк иного типа)л соответствующее .формуле а , истиной ла классе ыоделе к. и удовлетворяющей некоторым синтаксическим условиям, корректно (инвариантно) на классе моделей к. К этой группе относятся теоремы 1.1. 1.5. 1.6_-Ко второй группе относятся теоремы, утзерждающие, что достаточны!» условней корректности (инвариантности) преобразования, соответствующего формуле л , является истинность

на .классе моделей к некоторой формулы л*, получаемой из формула л конструктивно.

Вопросы корректности преобразований рассматривались такие А.Б.Машщводой [20-24]. Н.Яансалмаа [29-33].

В теореме 1.7. доказывается общезначимость % - канонических формул, являющиеся заключительными формулами для Евводов МШТ.

В конце параграфа доказывается полнота я конструктивность формального логического вывода, построенного на основе ЫШ1, ла классе так называемых ар - формул. Этот класс формул значительно вире згорвовс'ккх дизъюнктов. Полученные результата указывают на возможность создания на основе НЖП интерпретаторов для языков логического программирования [18] . белее•заразительных, чем ПРОЛОГ. Вопросы конструктивности

выводов, построенных на основе ЫЙП, рассматривались также А.Б.Николенко [34].

В параграфе §1.3. рассматривается вопросы:

- использование схем доказательств в ЖП:(индукция и метод от противного)*

- тактики вывода.

Индукция, используемая как схема доказательств в ШШ, описанная в §1.3, является существенным развитием так называемой структурной индукции [46]. Интересно отметить, что -данный тип индукции корректен без проверки кстинпости основания индукции, что, вообще говоря, дает некоторые преимущества при решении вопросов управления выводом (¡тогда бывает весь?.:г непросто выбрать основание индукции: начать с нуля, единицы, простого -члена к пр. ). Порождение индукционного предположения ь его пржеиевиа соответствует идеологии МШ1, т.е. выполняется преобразованиями формул.

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

Значительное место в §1.3. отведено построению тактик вывода. Основное отличие предлагаемого подхода от традиционных (например, стратегий метода резолюций [39]) в том, что планирование ведется на уровне применения исходных посылок завода,- аьне каких-тс промежуточных (неизвестных зара-коэ) объектов.

Первый-, раздел параграфа §1.4. посвящен эвристическому алгорктму распознавания ситуаций, являющемуся (с точки зрения логики) одним из методов прямого вывода для некоторого специального класса формул. Приведены оценки сложности алг.о-

ритма по количеству шагов и занимаемой зоне памяти.

Второй раздел параграфа §1.4. посзясен гзатематкчесасой постановке задачи проектирования расписаний и описанию алгоритма работа с очень болызжш формудаак, которые задают условия задачи (входные данные). Для данного алгоритма доказана теорема о полноте и корректности. Э$йективвость алгоритма во многом обеспечивается использованием глубокого возврата гбез полного восстановлена среды точки возврата. В параграфе §3.4. данный алгоритм будет называться глобальный' и будет включаться после локального алгоритма проецирования, который существенно "сжимает" дапше с которыми з дальпе^аем надо _ работать. В оток же разделе ироведегш сравнелке с •методом ¿'довлетворенлл огрзднзвяш* ( П. зан лелтенртсс, [48]).

Пятый параграф первой глазу посзлцэн вопроса»* алгогтсг-мическов разреиныостн теорий, Вопросу алгоритмической рэзрэ-шткосгя Гильберт сччтал ояпьяи я» основных Еопросои математики [93, а А.Н.1:нллгез - традт'ц^о-'ккчк для алгебры. Следу--

ответить, что еягср-глг я«-хсккв вопроса (а игрока» ]

трздиююнги -г дт« иатс.';.-ч .и.-я гг.-: . г: чес.':огс зтро1; КЗ]. 1л -лЛо,- Л'-..- ■■

[351 и др. , 1л, оП л

Вначале парзгрг:"- лкс л-р.лл л:: ;л'рл булевых алгсор (6'.."..; Н - л

ГЯ'Э ч- -- ослад.--: • :; л ллоо'лнл: ^;. ^ •

тоз, ' - - пгнглл' ,(■; лллл'нил, а - гвтсл'орфкл' о. а. Исходили резу^гз; ■ 'лллзсь теорем-з Й.Л.Ерио вз о

разраиикост»! злсь-лллслл; р-м б.-з. з с;-" лгурс;

. ' > (15).

. Во этороз нллп параграфа рассмэтпявглптся расмнрешшз теории целых чисел. Ачгоритнмлсшсс ••<„-Л{,>сн теории целых к

натуральных чисел привлекли внимание логиков сразу же после построения логических языков (т.е. создания необходимого формализма). Это, в частности, произошло из-за известной программы обоснования математики Гильберта, где формальной теории арифметики отводилось весьма значительное место.

Теорема 1.16 усиливает известную теорему о разрешимости универсальной теории целых чисел в сигнатуре < +, | >, где I - отношение делимости.

Второй параграф второй главы посвящен описанию системы АДТ АВТОДОТ, реализующей МИН. В начале параграфа рас-' смотрены входной язык и архитектура системы АВТОДОТ. Входной язык системы ВЯЗ строится на основе языка исчисления щ>гдк-катов первой степени, описание ВЯЗ дано в форме Бзкуса- Нау-эра, опредены нотации операций к отношений прздаютных областей,, метакоманд. В том же параграфе описаны функции основных подсистем и их взаимодействие. Приведены основные технические решения, принятые для внутреннего представления формул исчисления предикатов.

Параграф 2.3. лосвящен описанию основных компонент программных систем решения прикладных задач КАРАН, КАРАТ2 и АВТОР. В этом параграфе' обсуждаются:

- блоки вывода*

- основные интерфейсы«

- блок обеспечения гибридности (средства включения в комплекс КАРАТ! расчетных модулей, решающих базовые задачи предметной области).

В конце параграфа описаны алгоритмы, " реализующие тактики вывода в системе АВТОДОТ и программном комплексе ' КАРАТ2. Первый вариант работы тактики вывода соответствует выполнению логической программы в'ПРОЛОГЕ [I. 8] . Далее описываются способы реализации более гибких тактик;

Второй параграф третьей главы посвящен приложениям системы АДТ АВТОДОГ. Приводятся данные о машинных экспериментах по доказательству теорегл разлзгау^ разделов математики: исчисления высказываний, алгебры, теории категорий, теории дедекиндовых сечений, теории ¡.гаожеств.

Второй раздел параграфа яосглгцея описанию применения системы АВТОДОТ для реиения задач планирования организационно-технических мероприятий на АС« иерархической структуры.

В третьем параграфе рассиатрнзгятсл программные комплексы КАРАН и КАРАТ2, ориентированные на рэизнке задач поддержки-принятия реиеннй (ППР). Современные-системы ППР вюшо-чают компоненты, ориентированные на задачи:

-распознавание ситуаций при использовании пороговых коэффициентов, ограничений и ус«тозий на данные, приоритетов и степеней достоверности по источникам информации;

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

Концепция программного комплекса КАРАТ1 для решения задачи распознования ситуаций основывается на следующих положениях.

Текущая обстановка { ситуация ) описывается вектором [ л . А .... А ]

12 п

где каждый показатель -4 имеет некоторую предметную

интерпретацию. При использовании пороговых коэффициентов показатели имеют фиксированное множество значений, которые имеют ясно выраженную предметную семантику ( например, показатель "К1У" имеет значения { "проводятся", "не проводятся"}). Если предположить, что каждый показатель может принимать любое значения мз множества допустимых-,; • то получаем пространство ситуаций. Пространство ситуаций разбито на ке-

которое множество классов ситуаций (кластеры).Каждому классу ситуаций соответствует диагностика,- предписывающая те или иные действия. Основные задачи блока распознавания ситуаций и его схема следующие. Задачи:

т формирование данных о ситуации с учетом множества источников информации, имеющих приоритеты и степени достоверности по показателям;

- использование пороговых коэффициентов, ограничений и условий на данные;

-автоматизированное формирование классов ситуаций на основе экспертной информации, обучающих примеров;

-распознавание ситуаций в" условиях неполной информации и объяснение решения.

При организации взаимодействия ЛИР (жц принимающих решения) важное значение имеет динамическое планирование информационных обменов с учетом приоритета постугошших задач^ с учетом нормативов времени обработки информации, резака работы иерархической системы, логики движения порций информации (в зависимости от тыга ^формации и адресатов). Коля учитывать также, что обмен информацией осуществляется в сети ЭВМ, имеющей определенные стандарты оформления посланий, за-' данную конфигурацию и т.д., то-данная задача- имеет'самостоятельное значение. В глава-3 она называется задачей планирования информационных потоков з иерархической системе и решается программным комплексом КАРАТ2, описанным в конце параграфа 3.3. Здесь кс приведена математическая постановка этой задачи на языке исчисления предикатов.'

В четвертом параграфе третьей главы описывается программный комплекс АВТОР проектироваим? расписаний вузов. Приведена схема решения данной задачи и два ее основных этапа:

эвристичесюй и логический (хотя стоит отметить, что и логический этап на самом деле использует эвристические алгоритмы, описанные в §1.4). Приведена структура комплекса АВТОР и его основное характеристики, как автоматизированного рабочего места диспетчера вуза.

Основные результаты диссертации могут быть сформулирована следующим образом: . ~

1) Разработан формализм для моделирования математического мышления, построено логическое исчисление,ориентированное на создание систем автоматического доказательства теорем, проведены исследований по определению свойств построенного, логического исчисления (полнота, область конструктивной работы, корректность и др.);

2) Программная система АВТОДОТ, реализующая построенное' логическое исчисление, успешно опробована на решении теоретических и прикладных задач.

3) Создан программный комплекс КАРАН для решения задач распознавания ситуаций в условиях неполной и нечеткой информации.

4) Создан программный комплекс КАРАТ2 для решения задач организации взаимодействия должностных лиц в условиях жестких временных ограничений.

5) Создан програггмный комплекс АВТОР проектирования расписаний занятий вузов.

6) Программная система ■ АВТОДОГ сдана --мэзкведзмотвекной -комиссии, внедрена, в в/ч 19161, в/ч 01168. Программные комплексы КАРАН и КАРАТ2 внедрены в в/ч 01168. Программный комплекс АВТОР 'проектирования расписаний вузов передан в опытную эксплуатацию в Иркутский государственный технический университет.

7) Исследован вопрос.разрешимости двух массовых алгори-

тмических проблем. "

Автор благодарен ¡А.И.Кокорипуj за приветна вкуса к самостоятельной работе, за постановки задач и постоянную -под--держку в любых начинаниях.

Автор благодарен Э.Б.Белякову, Й.В.Вяткину, Ю.Н.Гаврн-кову, В.Й.Машничу, А.Б.Нюсоленко, С.Б.Нкколенко, В.Г.Петрову, К.Н. Соловьавко, А.А.Харкееву, Н.Ш Яковлеву за активное-участие в шголненш плановых тем и реализации проектов программных систем АВТОДОТ, КАРАН, КАРАТЕ, АВТОР.

Автор благодарен Б.В.Окунцову, С.Г.Александрову, В.В. Сухорутчевко.Т.Л.Чекинову, 0.Я.Трубицыну» А ЛЬ Казакову, А.К.Ванькову» В.Д.Михайленко за полезное сотрудничество.

Автор благодарев С.Н.Васильеву за стимулирующую роль в написании диссертации к ценные замечания.

Автор благодарен А.К.&рлову за ценные замечания» способствовавшие улучазвш работы.

ПШШШШ ПО ТЕМЕ ДЙССЕРТАШЖ

1. Александров С.Г.,Яартьяков В.й. Применение систел: АЛТ для решения задач сетевого планирования // Интеллектуализация программных средств. Сб. тр./ Под редакцией -О.Г.Дивакова,- Новосибирск: Наука, 1991.- С. 160-168.

2. Беляков Э.Б.,Мартьянов В.И. Универсальные теории целых чисел к расшфеввая гипотеза бяиззеш» // Алгебра к логика. - 1983.- V} Г. - С.2-6-34.

3. Манцивода A.B., Мартьянов Б,К. Об инвариантных преобразованиях формул // Вычислительные система: Прикладная логика. Сб.научи.тр. / Под.ред. Ерыова КЗ.Л. -Новосибирск: Ш СО АН СССР, Г9В6,- C.I56-I6I.

4. Мартьянов В.И. О теории абелевых групп с предикатами, выделяющими подгруппы, и операциями эндоморфизмов // Алгебра и логика.- 1975.-N5.-С.536-542.

5. Мартьянов В.'И. Универсальные расширенные теории целых чисел // Алгебра к логика.- 1977.-№5.-С.588-602.

6. Мартьянов В.И. Неразрешимость теории абелевых групп с автоморфизмом II Математ. заметки.- М.: Наука, 1978.-Т.23. вып.4.-С.515-520.

7. Мартьянов В.И. Доказательство теорем на ЭВМ // Алгебраические вопросы алгебраических систем и ЭВМ.

'Сб.научн.тр. / Под.ред. Ко Корина" А.И.- Иркутск: ИГУ, 1979.- С.III-127.

8. Мартьянов В.И. Неразрешимость теории булевых алгебр с автоморфизмом // Сиб.мат.журн.- 1982.- Т.23.,№3.-

С.147-154.

. 9. Мартьянов В.И. О методах задания и частичного построения теории на ЭВМ // Кибернетика.- 1982,- ff€.-C.I02-II0.

10.Мартьянов В.И. Задание и частичное-построение теории на ЭВМ // Разработка пакетов прикладных программ / Отв.ред. Матросов В.М. ,Дива.ков О.Г.- Новосибирск: Наука, 1982.-С.5-22.

П.Мартьянов В.И. Об инвариантных преобразованиях формул // Матем. заметки.- М.: Наука, 1984.- Т.36, вып.4.-С.571-583.

12-Мартьянов В.И. Применение логики для решения задач ре-

■ ального времени // Вычислительные системы: Логика и семантическое программирование. Сб.научн.тр. / Под ред. Ершова Ю.Л., Гончарова С.С.- Новосибирск: ИМ СО РАН,

1992. в.146.- С.170-174.

13.Мартьянов В.И., Николенко А.Б. Об интерпретации логических программ // Вычислительные системы: Прикладная логика. Сб.научн.тр. / Прд ред. Ершова Ю.Л., Гончарова С.С Новосибирск: ИМ СО АН СССР. 1987. в.122.- С.38-46.

14.Мартьянов В.И., Харыеев A.A., Яковлев Н.П. Реализация схем доказательств в методе инвариантных преобразований // Кибернетика,- 1988.- N3.- С.79-83.

15.Мартьянов В.Й., Сухорутченко В.В., Окунцов В.В. Планирование информационных потоков в иерархических системах//- Прикладные системы, Москва. 1992.. С. 76-90. .

СПИСОК ЛИТЕРАТУРЫ

1. Борщев В.Б. ПРОЛОГ - основные идеи и конструкции // Прикладная информатика : Сб. научн. тр. / Под ред. Савинкова В.М. - М. : Финансы и статистика, 1986.-Вып.2(11).-С.49-76. !

2. Бублик В.В. Обобщенная структурная индукция // Кибернетика.- 1977. - №3.-С.22-31. ' .

3- Васильев C.R.- Метод сравнения в анализе-систем. // i-iv. Дифференциальные уравнения. 1981,17* №9. С-. 1562-1573; . 1981.17, №11, С. 1945-1954; 1982. I8,Jf2, G.192-205, 1982, 18, №6, С.938-947.

4". Васильев С.К., Каратуев В.Г., • Матросов В.'М.и др\" Пакет ■прикладных программ вывода"теорем метода векторных функц ций Ляпунова // Пакеты прикладных программМетоды и раз работки.- Новосибирск: Наука, I98I.-C.II9-I32.'

5. Васильев С.Н. Вывод теорем на основе решения логических уравнений в исчислении предикатов // Всесоюз. конф.

- "Искусственный интеллект и распознавание образов", 1984.-С.24-27.

6. Васильев C.B., Матросов В.М. Принцип сравнения в матема-^ тической теории систем// V Казахстан, межвуз. конф. по математике и механике, Алма-Ата, 1974.-С.34-36.

7. Васильев С.Н., Жерлов А.К. и др. О логических средствах системы планирования вычислений "ПАСАД"// Алгоритмы -Ташкент: Ж АН Уз.ССР, 1988.-Вып.66.-С.97-112.

,8. Воронков.A.A., Дегтярев АД. Автоматическое доказательство теорем. I. // Кибернетика,- 1986.-(ГС.-С.27-33.

•'9. Гильберт Д., Аккерман В. Основы теоретической логики.-М.: ИЛ, 1947.-194с.

10. Гильбзрт' Ц., Бернайс П. Основания математики: Логические исчисления и формализация арифметики.- М. : Наука, IS83

.-384с.

11. Глу.шков В.М., Ю.В.Капитонова, А.А.Летичевский и

. др. К построению практического формального языка для записи математических теорий.- Кибернетика.-1972,N5, С. 19-28.

12. Глушков В.М. Система автоматического доказательства (САД) // Автоматизация обработки математических текстов. Сб.тр. / Отв.ред. Капитонова Ю.В. - Киев: ИК АН УССР, 1980. -С.3-30.

13. Гончаров С.С., Свириденко Д.И. 2 - программирование // Вычислительные ситемы: Логико-математические аспекты M(33 Сб. научн. тр. / Под ред. Косарева Ю.Г., Гончарова С.С.Новосибирск: ИМ СО АН СССР, 1985, в.107.-С.3-29.

14. Дегтярев А.И., Лялецкий A.B. Логический вывод в системе-автоматизации-доказательств // Математические основы

систем искусственного интеллекта / Отв.ред. Капитонова Ю. В. - Киев: ИК АН УССР, 1982, C.3-I6.

15. Ершов Ю.Л. Разрешимость элементарной теории дистрибутивных структур с относительными дополнениями и теории фильтров // Алгебра и логика. -1964.- №3.-С.17-38.

16. Ко корни А.И., Козлов ГЛ. Элементарная теория абелевых групп без кручения, с предикатом выделяющим подгруппу // Алгебра и логика.- 1969.- Г.8.- ИЗ.-С.320-334.

17. Криницкий H.A. Равносильные преобразования логических схем // Автореферат канд. диссертации.- МГУ.-1959.

18. Логическое программирование.// Сб. статей/ под ред. 'В'.Н. Агафонова.- М.:Мир, 1988, 368с.

19. Мальцев АЛ1. Модальные соответствия // Изв. АН СССР.-сер. матем.- 1959.- Т.23,-№3.- С.313-336.

2Ü. Манцквода A.B. О р - преобразования формул // VII Всесоюзная конф. по мат. логики. Тезисы докл.- Новосибирск: ИМ СО АН СССР, 1984.- С.97.

21. Манцивода A.B. О преобразованиях, соответствующих определениям // VII Всесоюзная конф. "Проблемы теоретической кибернетики". Тезисы докл.- Иркутск: МГУ 1935,- 128-129.

22. Манцивода A.B. О представимых преобразованиях У/ Всесоюзн. конф. по прикладной логике. Гезисы дозсл.-Ровосибирск: ИМ СО АН СССР. 1985.- С.136-138.

23. Манцивода A.B. .06 инвариантности С -преобразований // Алгебраические системы. Алгоритмические вопросы и ЭВМ Сб.научн.тр. / Под.ред. Кокорина А.И. - Иркутск: ИГУ, 1986.-С.63-68.

24. Манцивода A.B. О строгой вложимости П IV Всесоюзная

конференция "Применение методов математической логики". Тезисы докл.- Таллин, Г986. С.104-106.

25. Маслов С.Ю. Обратный метод установления выводимости в классическом исчислении предикатов // ДАН СССР.- 1964.-вып.I.- С.17-20.

26. Матросов В.М., Васильев С.Н. Принцип сравнения для вывода теорем математической теории систем// Тр. IV Международ. об!Гнздин. конф. по искусств, интеллекту. - Тбилиси.- М.: ВИНИТИ.- 1975.-С.166-175.

17. Матросов В.М., Васильев С.Н. Принцип сравнения для автоматического вывода теорем. 1,11 // Изв.АН СССР.-сер.Техн.кибернетика.- Г978,- Ш,- С.60-69, Р.- С.40-49.

}8. Матросов В.М., Васильев С.Н. и др. Алгоритмы вывода теорем векторных функций Ляпунова.- Новосибирск: Наука, 1981.- 271с.

19. Нансалмаа Н. Представление нормальными преобразованиями содержательных доказательств // VI Всесоюзная конф.по матем.логике. Тезисы докладов Тбилиси: ТГУ, 1982.- С.131.

¡0. Нансалмаа Н. О - преобразованиях формул // VII Всесоюзн.юонф. "Проблемы теоретической кибернетики". Тез.докл.- Иркутск: ИГУ, 1985.- С.145-147.

Я. Нансалмаа Н. О корректных преобразованиях формул // Алгебраические вопросы и ЭВМ.Сб.научн.тр. / Под ред. Кокорина А.И.- Иркутск. ИГУ, 1986.- С.92-96.

12. Нансалмаа Н. О преобразованиях формул в к-значных логиках // Применение методов математической логики.Тезисы докл.- Таллин: ИК АН ЭССР, 1986.- С.129-130

3. Нансалмаа П. О применении правила заключения в неформальных математических доказательствах //

Кибернетика.- 1986.-№4.- С.90-92.

34. Николенко А.Б. О конструктивности преобразований формул // Всесоюзн.конф. по прикладной логике. Тезисы докл., Новосибирск: ИМ СО АН СССР, 1985.- С.116.

35. Подловченко Р.И. Моделирование программ схемами и построение систем преобразований схем // Кибернетика.-1982.- т.- С.88-96.

36. Робинсон Дж. Машинно-ориентированная логика, основанная на принципе резолюций // Кибернетический сборник, новая серия / Сб.перев.под ред. Лупанова О.Б.- М.: Мир, 1970.- вып.7.- С.194-218.

37. Слободской A.M., Фридман Э.И. О теориях абелевых групп с предикатом выделяющим подгруппу // Алгебра и логика.-1975.- Т.14.- Н5,- С.572-575.

38. Справочная книга по математической логике, ч.1.- М.: Наука, 1982.- 392с.

39. Чень., Ли Р. Математическая логика и автоматическое доказательство теорем.- М.: Наука, 1983.- 352с.

40. Шанин Н.А, Давыдов Г.Л., Маслов-С.Ю. и др. Алгоритмы машинного поиска естественного логического вывода в исчислении высказываний.- Л.: Наука, 1966,- 39с.

41. Шанин Н.А, Давыдов Г.Л., Маслов С.Ю. и др. Алгоритмы машинного поиска естественного логического вывода в исчислении высказываний.- М..Л.: Наука, 1965,- 40с.

42. Язык Пролог в пятом поколении ЭВМ// Сб. статей/ под ред Н.И.Ильинского.-М.:Мир,1988 , 504с.

43. Янов Ю.И. О логических схемах алгоритмов // Проблемы кибернетики / Под ред. Ляпунова A.A.- М.: Изд-во физ.-мат. лит-ры, 1958.- вып.I.- С.75-127.

44. Bledcoe I.W.. Bruell ?. A man-machine theorem -proving System.- Artificial Intelligence, 19T4, vol.-5. p.51-72.

45. Bledcoe *.». won resulution theurem proving // Ai til. Intelligence. 1977, vol.9, p.1-35.

46. Burstaii R.ffi. Proving properties o£ Programs by Structural Induction 11 Computer Journal, 1969, vol.12. №1; p.T2-77.

47. Colmerauer A., P.Kanoui, R.Pasero. Un systeme de communication ho/nme-machine en irancais; rapport de

- rechercheCRI 72-18, Group-Intelligence Artificielle, Universite Aix - Marseille II.

48. Hentenryck van P. Constraint Satisiation in logic Programming// The MIT Press, Cambridge, 1989.

49. International Conference on Fifth Generation Computer Systems: Proc./Int. Conf.. Tokyo, 1979/Amsterdam a.o.: North Holland, 1981.

50. Kowalski R. Predicate logic as programming language// In: Information Processing'74

(HIP Congress 74), 1974. p.569-574.].

51. Kowalsky R. logic programming // Proc.IFIP 83, 1983.-p.133-145.

52 ." lusk I,"W.McCune, R.Overbeek. Logic'Machine Architecture: kernel functions// Lecture Motes in Computer Science, v. 138, 1982.!.

53. Nevell A., Shaw J., Simon H. Empirical Explorations oí the Logic Theory Machine.- Proc. West Joint Computer Conf.- 1957. vol.15, p.52-67.

54. Raph K. The Marksraf Karl Refutation Procedure//

Memo SEKI-MK-84-01, University Kaiserslautern, 1984.

55. Rosser J.B. Extensions of some theorems of Gogel and Church // J.Symbol.Logic, 1936. 1. p.87.

56. Vassilyev S.M. Machine synthesis ol mathematical theorems. - J. logic Programming, 1990, v.9, № 2-3, pp.235-266.

57. Wang H. Towards mechanical mathematics // IBM J.Res. and Develop.- 1960.- 4,- p.2-22.

58. Warren D. Implementing Prolog - compiling predicate logic programs// D.A.I. Research Report N39, 40. Edinburgh: Uviversity oi Edinburgh, 19Î7.

59. Wos L. Solving open questions with an automated theorem pruving program// Lecture Notes in Computer Science.

v. 138, 1982.