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

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

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

ИВАНОВ Дмитрий Анатольевич

^ДК 007.51:681.3.06

ПРЕДСТАВЛЕНИЕ ЗНАНИИ И ПОДДЕРЖКА РАССУВДЕНИЯ С ИСПОЛЬЗОВАНИЕМ ОГРАНИЧЕНИИ

Специальность 05.13.11 "Математическое и программное обеспечение вычислительных машин, комплексов, сетей и систем"

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

Москва 1993

/

Работа выполнена в Московском авиационном институте.

Научный руководитель: доктор технический наук,

профессор Райков Л.Г.

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

профессор Федоров В.В.

кандидат фгаико-математичеоких наук, начальник отдела Сухов C.B.

Ведущая организация: Научно-иоследовательский вычислительный

центр МГУ имени М.В.Ломонооова.

Защита ооотоитоя "/ " 1993г. в

чаоов

на ваоедании специализированного Совета К 063.18.09 в Московском авиациошюм институте по адресу: 12Б871, Москва, ГСП, Волоколамское шоссе, 4.

С диссертацией можно ознакомиться в библиотеке института.

Автореферат разослан

Ученый секретарь Совета к.ф.-м.н., доцент '-п^-^/У Ы.В.Ротанина

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

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

Преодолеть эти недостатки, повысить эффективность обработки можно, подразумевая альтернативную интерпретации логических связок, применяя неполную дедуктивную систему, пользуясь дополнительным формализмом (формализмами), что приводит к гибридной оиотеме представления знаний (СТО). Каковы варианты для выбора дополнительного формализма? !

В настоящее время все большее признание получает объектно-ориентированный (00-) подход. Несмотря на естественность самого понятия объекта, обычные методы обращения с ним: посылка сообщений, полиморфные функции и т.п. — носят процедурный характер. Поэтому традиционная 00-парадигма неприемлема для СТО, где-описательные средства должны быть, по возможности, декларативнымиК изъянам фреймового метода ПЗ можно отнести отсутствие понятия согласованности и семантическую неадекватность механизма демонов. Это обуславливает применение более изощренного подхода, например, основанного на ограничениях (conatraint-baaed).

Чтобы претендовать на практическую значимость, модель предметной облаоти((ПО), должна синтезироваться как согласованное описание. Она формируется исходя из специГикации начальных требований, желаемых свойств,, поведения и т.п. Ввиду постепенности, инкрементальнооти процесса ее построения особую важность приобретает задача идентификации противоречий на более ранних этапах. Это обязывает ориентироваться на систему прямого вывода и компонент поддержки расоуждений (reason maintenance eyatem), который бы фиксировал каждый шаг вывода и обеспечивал бы объяснение для производных фактов и выходных значений.

Поли и задачи. Основными задачами диссертации являются разработка гибридного формализма ПЗ, выразительные средства которого охватывают логический и 00-языки, обеспечение тесного

взаимодействия обоих концепция в рамках единого процесса выво-да/вычиолений на частичной модели. Целевая архитектура СТО должна включать модуль поддержки раооуждений (ЫПР), обеопочивающий представление завиоимоотей между посылками и следствиями, между явно' введенными значениями и результатами вычислений, что необходимо для выдачи объяснения и идентификации источников возникающих противоречий. Программная реализация должна предоставлять1 пользователю возможность выдвижения оуждений на языке, 0ли8ком по мощности к логико-алгебраическим спецификациям, обладать мобильностью, предусматривать расширение СИЗ за счет подключения других средств представления и обработки информации: СУБД, машинная графика, ППП и др.

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

Научная новизна работы заключается в следующем.

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

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

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

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

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

- Разработана методология описания и решения задач, носящая инкрементальный, интерпретационный характер.

Практическая ценность. Предложенные принципы организации

А

СГ13 и тооротичоокио pflзyльт(lл^ гюплощони п оиотомо Alteas, pon-, лиаовашюй под MS-DOS на IBM PC, доведенной до уровня исследовательского прототипа. Основанная на фреймах ранняя версия системы для ЭВМ типа VAX передана в Отраслевой фонд алгоритмов и программ.

Отдельный интерес может вызвать базовый инструмент Ybisp — система программирования на ОО-расширекии языка Коммон Лисп, поддерживающая небезызвестный стандарт Common LISP Object Syatem (CLOS), которая также написана автором. Она внедрена в учебный процосо факультета "Прикладная матоматико" МАИ и Лицо» информационных технологий при МГУ.

Апробация работы. Основные положения и результаты работы докладывалиоь и обоухдались на семинарах "Искусственный интеллект" под руководством профессора Л.Г.Райкова (МАИ, 1987~92гг.), Межвузовской конференции "Математическое обеспечение систем искусственного интеллекта" (Москва, 1987), Всесоюзной конференции "Интеллектуальные системы" (Туапсе, 1991).

Публикации. По тематике диосертации опубликованы 4 печатные работы, нэ очитая нескольких отчетов по НИР кафедры 802.

Структура и объем работа. Диссертация состоит из введения, пяти глав, заключения, опиока литератур«, содержащего 105 наименований, и трех приложений. Машинописных страниц основного текота — 181, рисунков — 16, таблиц — 4, объем приложений — 46 страниц.

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

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

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

ки на Епепший мир, путем опецифшации впешней семантики.

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

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

Во-вторых, комбинаторный взрыв, со-НР-полнота проблемы вывода в логике выакааываний, полуразрешимооть ЛПП означают отсутствие гарантии вавершения для значительной чаоти операций СТО.

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

1) применение более слабой логики, которая имела бы аффективную процедуру вывода, ориентированную на семантические методы;

2) интерпретация над большим числом истинностных значений;

3) комбинация о дополнительными формаливмами;

А) обеспечение согласованности оодержимого БЗ, а вначит, использование прямого вывода. 5) встроенная и аффективная реализация МНР.

За последнее десятилетие ОО-подход и идеологически близкий к нему фреймовый метод ПЗ (41 валились в такое декларативное и инференциально мощное уточнение, как парадигма ограничений. При воей привлекательности последней в качеотве дополнительного формализма, интеграция во о логическими средствами должна ооу-щ9отвлятьая в рамках существенно гибридной (essentially hybrid) и сбалансированной СТО. Это подразумевает

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

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

- реализацию всякого влияния, оказываемого представляющей конструкцией одного под$ормалтама на внания, предоставленные средствами другого, согласно общей семантике.

О учетом сказанного, в конце главы уточняется постановка

б

задачи дисоертации: отрогая спецификация упомянутых формализмов ПЗ и теоретическое наследование их свойств, выработка принципов их объединения друг о другом и о МПР в рамках гибридной архитектуры СТО и программная реализация на базе Лисп-системы.

Во второй главе формально описан логический компонент. Фундамент его дедуктивной сиотемы составляет пропозициональная логика PCL. Синтаксически ее язык Lp совпадает о языком классической логики высказываний. Алфавит языка разделен на две составляющие: фиксированную часть, куда входят логические связки и вспомогательные символы, и нелогическую чаоть, зависящую от приложения, — счетное множество Р пропозициональных переменных. Традиционно определяются правильно построенные формулы.

Дедуктивная система PCL описывается как система естественного вывода, которая не содержит логических аксиом. В PCL от-оутотвует и правило предположения, или выдвижения гипотез, — отправными точками всех доказательств являются факты и гипотезы, . которые явно вводятся в БЗ пользователем и трактуются в качестве нелогических вкоиом. Для каждого логического символа имеется более одного правила введения и устранения. Правила довольно просты и напоминают способ интерпретации формул, что демонстрирует, к примеру, следующее

Определение 1 (Правила вывода для л).

<^n> <j) -i(a л р) (ABl) -а £ Р (лКг) а ft Р-

(л!)

JLJ3 ал р

(плЕ1) М3?. Р (плЕг) а Q

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

Необходимость семантической характеристики дедуктивной системы, функционирующей в условиях неполной и противоречивой информации, обусловила использование четырехзначной интерпретации связок, которая предложена Н.Белнапом. Каждая формула отмечается одним из элементов множества истинностных значений В - {t, Г, и, к), где t — только истина, f — только ложь, и

— неопределенность (без уточнения причины), к — противоречие.

Далее определяется частичная интерпретация (ЧИ) как отображение Lp-* Ш, которое однозначно раоширяет приписывание истинностных значений пропозициональным символам на весь язык. Со-монтичоскоо следование в логике POL характеризуется такими свойотвами, как сохранение иотшпюоти (вывод никогда не приводит ипо от истины к оо отоутотпию) и "иолокнооти" (шиод ко приводит нас от отсутствия лхи к лжи). Результаты изучения PCL пмрпоилиоь и слодуицих утворждониях.

Теорема 2. Дедуктивная система PCL корректна. ■ Теорема 3. Дедуктивная система PCL неполна. ■ Том не менее, показано, что дедуктивная оистема PCL не слабее, чем метод единичных резолюций (т.е. механизм вывода языка Пролог), что привело к следующему.

Следствие 4. Дедуктивная система PCL полна в классе хор-новоких предложений. ■

Другая часть главы поовящена логике CL — упорядоченно-сортному (УС-) бескванторному языку с равенством. Иерархия сортов вводится как верхняя лолурешетка (S, á) о наибольшим элементом Т. Нелогическая чаоть алфавита языка представлена сигнатурой.

Определение 5. УС-сигнатура — вто пятерка <S,d,F,P,X>, где (S, d) — иерархия сортов, F, Р, X — семейства множеств функциональных, предикатных символов и символов переменных соответственно, индексированное элементами и последовательностями элементов из S. □

Сиитакоио языка CL фиксируется определениями УС-терма и УС-формулы, которые вводятся с условием, Что сорт терма должен быть не больше (в смысле частичного порядка á) сорта соответствующего аргументного места функционального или предикатного символа.

Четырехзначную семантику для логики CL вводит следующее , Определение б. Логичеокая ситуация есть тройка <В,<р,ф>,

где

D = U De — универоум, являющийоя объединением непустых носите-лей (или областей интерпретации) сортов. Замыканием носителя сорта s называется его расширение D^^ De и (о) несобственным элементом <о, который предотавляет неопределенное вначение и являетоя общим для всех сортов.

ф: y<w<e>-» [Dw-> Del — отображение, ведающее интерпретацию

Ü

функциональных символов; ф: Рш-» В] — отображение, задающее интерпретацию предикатных символов, (Б = Ю «...« Б , * = в,.. .в ).

' * и. в ' 1 п' □

1 п

Упорядоченно-оортная частичная интерпретация (УСЧИ), зависящая от логической ситуации и оценки переменных (8 € Э) одновременно, позволяет вычислить значения термов и определить истинностные значения не только атомарных, но и составных формул. Отличив интерпретации переменной от индивидной конотанты в том, что ей мокет сопоставляться неопределенное значение ш, а индивидной константе УСЧИ приписывает собственный элемент универсума Б.

Дедуктивную систему СЬ составляют те же правила вывода, что н для логики РСЬ. Так СЬ не имеет кванторов, ее язык легко вводится к Ьр, УСЧИ преобразуется в ЧИ. Это позволило перенести результаты о корректности и полноте для пропозициональной логики на чистую логику СЬ. "Дедуктивная ниша", вызванная отсутствием в ОЬ первопорядковых правил вывода, заполняется инференци-альными средствами другого формализма — сиотемы ограничений. Общие требования, которым должны удовлетворять эти средотва, отражены в принципах построения УС-сигнатуры и УСЧИ.

В третьей главе описывается МНР, основанный на логике и иопользущий предположения. Формально он включает

- множество узлов и, сопоставленных предложениям БЗ; с каждым узлом связаны две литеры: положительная и отрицательная;

- множество клауз С, которте играют роль двунаправленных обоснований (подтверждений) и представляют зависимости между посылками н следствиями;

- множество предположений А с (К | N € Ш и СтК | N € и), т.е. литер, соответствующих фактам, которые явно введены в БЗ;

- множество контекстов 2 с каждый ив которых является набором предположений, представляет альтернативную точку зрения на ПО.

Основная задача ЫПР — вычисление рааыетки, приписывания каждой литере булевой комбинации предположений в дивьшктивной нормальной форме. Точнее, метка литеры - ото неоократимый буле-вый многочлен над переменными-предположениями из А. Доказано, что множество меток, частично упорядоченное по отношению включения, является конечной дистрибутивной решеткой о псевдодополнениями и поевдоразноотями (£Н,«,+,-,*,0,1). Время выполнения операций в етой решетке оказалось полиномиальным в сравнении о

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

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

Другая обязанность ШР — идентификация противоречий. Это доотигмотии »(^кшнакоииом миток контрарных литер. Если произведение отлично от О, то кавдое из слагаемых есть негодный дизь-и1кт (nogood) — носоимоотимый набор предположений. Каждый контекот, который содержит такой набор, является заведомо противоречивым.

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

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

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

Итогом главы служит инкрементальный алгоритм нахождения согласованной и обоснованной разметки, вступающий в работу при изменении множества узлов U или множества клауа-обоонований С. В конце намечен подход для представления в обработки немонотонных зависимостей, приводится временная сложность процедур! разметки. Она полиномиальна ори наличии только монотонных овязок, но в общем случае проблема является ЫР-полной.

В четвертой главе изложена парадигаа ограничений и как отдельный формализм, и как единый подход к реализации СТО.

Определение 7. Ограничение еоть декларативное утверждение

ю

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

Система ограничений (СО) трактуется как множество ячеек и множоотво отношений между ними. Задача процосооро ограничений — найти приписывание вначений ячейкам, выполняющее данные эт-иошения. Наиболее эффективным алгоритмом разрешения 00 являегол локальное распространение ограничений (ЛРО): как только получает значение часть ячеек неудовлетворенного ограничения, достаточная для применения одного из его методов, так ораву данный метод вызывается, определяя значение ранее неизвестной ячейки. Эти новые значения, в свою очередь, могут привести к дальнейпим вычислениям, посредством соседних ограничений.

После анализа сущеотвупянх реализаций СО, которые, как правило, охватывают математические зависимости, автору удалось не только интегрировать ограничения о логикой, во и реализовать дедуктивный вывод как ЛРО. О этой целью всем формулам, представленным в БЗ, а воем их подформулам ставятся в соответствие булевы ячейки. Значения их выбираются из специальной математической конструкции, бирешетки меток. Еирешетка — это множество, обладающее двумя частичными порядками < и с, двумя наборами решеточных операций, а также операцией отрицания 1.

Определение 8. Еирешеткой меток (И,л,у,п,и,л) называется бирешетка, в которой (1)

(И)

(111)

(17)

Введенный во второй главе набор истинностных значений Ш формируют бирепетку (рио.1), о учетом обозначений: i = <0,1>, t = <1,0>, u = <0,0>, к= <1,1>. Над бирешеткой меток определяется многозначная интерпретация (Ш) J: Lp-» M.

Определение 9. ЫИ J' есть расширение интерпретации J: J = J' Va € Lp: Jlal в J' la|. □

« =di & = «VV • xf xic m'

операции n и и задаются на D^ покомпонентно: <xt,xf> п <yt,yf> =df <xt«yt, if«y£>, <xt,x£> и <7t,7t> =di <xt+yt, xf+yf>;

операции л и v задаются так:

<lt.x£> A <yt,yf> =di <xt-yt, Xf+yf>, <!t.if> V <yt,yf> =¿1 <xt+yt, Xf.yf>; операция отрицания определяется так:

с

к

f

t

u

<

Рио.I. Наименьшая нетривиальная бирешетка Ш.

Функциональный подход рассматривает дедукцию как процесс перехода от МИ, представляющей начальное информационное состояние, к ее расширению, более информативному состоянию. Соглаоуя вычисление дедуктивного вамыкания о принципами приписывания истинностных вначений составным формулам в ЧИ, удалось сформировать клаосы булевых ограничений Not, And, Or, Imp, которые соответствует логическим овявкам, и определить их метода, которые обеспечивают выполнение логических соотношений.

На булевы ячейки, сопоставленные явно внесенным в БЗ фактам, налагаются ограничения оообого вида — булевы предположения двух видов:

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

- предположения-акаиош, ооответотвупцие формулам, которые предотавляют фоновые факты, незыблемые ваконы ПО, нотинноот] которое ве подлежит оомнению и которые, о точки арония пользователя, не должны быть вовлечены в противоречие.

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

Разработанный алгоритм BOOL-PROPAGATE по булевой СО, : которую транолируютоя формулы Lp, и начальной МИ J позволяв найти ее расширение J' (J с J'), служащее решением. Комбинаци. МИ J о контекотом £ € S определяет контекстуальную интерпрета цив I(J,C): Lp-» В. То, что вывод в системе РСЬ сводится к рао проотранению булевых ограничений, подтверждает следующая

Теорема 10. Пусть Г — непротиворечивое множество гипотез а — формула Lp. Тогда

(1) Г »- а «-* I(J',£)|a| = t, где J' — решение булевой СО выработанное BOOL-PROPAGATE, £ — неведомо противоречивы контекст, состоящий из всех предположений — гипотез Г.

(11) Время, затрачиваемое для определения Гю, составляет 0(та«п), где п = |Р| — общее число пропозициональных символов, т = |Г|. ■

Во второй чаоти главы иа ооновв языка логики ОЬ конструируется интересующее нас внутреннее отроение БЗ.

Определение 11. Упорядоченно-оортноя система ограничений (УССО), ассоциированная о БЗ Г, еоть шестерка

СБ (Г) =<и (Ви(Г), ВС(Г), ВА(Г), БЩГ), 80(Г), БА(Г)), где ви(Г) — мнокеотво булевых ячеек,

ВС(Г) — множество экземпляров булевых ограничений, ВА(Г) — множество булевых предположений, эи(Г) — множество оортных ячеек,

БС(Г) = РС(Г) и РС(Г) и ЕОЬС(Г) — множество экземпляров функциональных, предикатных ограничений и ограничений равенства, г!(Г) — множество присваивающих предположений. □ Сортные ячейки оопоотавляются воем термам и подтермам формул, входящих в Г, кроме индивидных конотант. Значение ячейки, ассоциированной о термом 7 сорта в, еоть пара

«1, 2> = «1, (1 € 2 € М (г^, М),

т.е. собственное вначение <1 плюс поддержка а, причем вь служит обоснованием предиката 7 = 1, указывает на источник происхождения или опоооб вычисления (1. выражает поддержку "факта" V ^ й, еоли УССО может обеспечить какую-нибудь информацию, чему г не должен быть равен. Классы функциональных и предикатных ограничений оопоотавляются символам УС-сигнатури и подразделяются на встроенные и вторичные. Первым придается фиксированная интерпретация. Вторые определяются через через композицию других и огорационно сводятся, в конечном итоге, к первым, но их начальная интерпретация может быть недоопределенной и уточняться в ходе разрешения и/или заполнения БЗ.

Присваивающие предположения служат более компактным представлением формул вида (у = с), где о — константа, и, подобно булевым предположениям, делятся на предположения-гипотезы и предположения-аксиомы.

Каждое ограничение, экземпляр встроенного клаооа, имеет внутренний флажок, который находится в одном иа трех состояний:

- удовлетворено;

- неудовлетворено, ибо значения связанных ячеек, вычисленные черев ооооднио ограничения, не выполняют условия теста;

- удовлетворенность невыяонена.

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

Определение 12. Решение УССО еоть пара <%, J>, где X — оценка переменных, приписывание собственных значений, J — МИ, формирующая их поддержки, а

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

Наконец, уточняются понятия выводимой формулы и вычислимого терма, даетоя определение гибридной дедукции, осуществляемо! процессором ограничений, которое окончательно специ^ицируеч отоооб вывода/вычислений в СПЗ.

В пятой главе описаны программная реализация гибридной СТС ARCOS (Automated Reasoning Constraint Objeot System), см, рис.2, и язык ограничений ЛОКОН, который вобрал в себя выразительные преимущества логического и ОО-подходов.

Rio.2. Архитектура системы ARCOS.

Необходимость масштабной символьной и нетрадиционной логической обработки, наличие естественной привязки типа к объект] привели к выбору явыка Лион в качеотве базового инструмента. Фактически им стала сиотема XLlsp (последняя версия 2.0), i которой воплощено около 3/4 стандарта Коммон Лион и ег< ОО-расширения 0L0S.

На рио.З изображена верхняя полурешетка встроенных тишн системы XLlsp. Заглавными буквами напечатаны имена тех, которые сопоставлены классы. Классы PATH, FIN и тип logical, выделенные курсивом, относятся только к сиотеме ARCOS.

Yblsp полностью обеспечивает наследование, оонованное нг построении описка предшествования — тотально упорядоченногс

множества, состоящего из класса и всех его надклассов.

FUNCTION ,1.

compiled-func t ion

SYMBOL LIST VECTOR NUMBER string-ctiar ,

I /

NULL CONS STRING INTEGER FLOAT hash-tablo

blgnum fixnum

stream

keyword

logioal PATH PIN

Еио.З. Иерархия встроенных типов YLiop/ARCOS.

Метасистема, включающая основные метаклассы STANDARD-CLASS, BUILT-IN-CLASS и STRUOTURE-OLASS, изображена на рио.4. (Для иллюстрации приведен один встроенные класс number и один структурный класс structure, а имена метаклассов вписаны за-ЬлавЙ&ли буквами.)- •

' ' t

STANDARD-CLASS

X

. х х

BUILT-IN-CLASS STRUCTURE-CLASS

-- atandard-obiect

- number

structure

COHSTRAIim-OLASS

- aonstralnedr-objaot

Рис.4. Иерархия метаобьектов УЫвр/АЯССБ.

0тношо1шя: «—1ш^опо9-оГ, <-1о-а (оиЬс1аз0-оГ).

Язык ЛОКОН синтаксически являотоя расширенном Коммон Лиона. Концептуально он максимально приближен к логическому языку ОЬ. Роль продопродолошшх, бопоша сортоп играют ПОТрООШШО и структурные типы Кошюн Лиспа. Наращивание иерархии оортов посредством определения новых классов отвечает теоретико-решеточной интерпретации: различным сортом оопоотавляются различные носители, а точным верхним и точным нижним граням (если они существуют) — объединения и пересечения носителей соответственно.

Формирующие сигнатуру символы подразделяются по двум при; накам. Во-первшс, вто естественное раабиепие па индиви,щшв ш ременные, конотанты, функциональные и предикатные символ! Во-вторых, они делятся на так называемые бисимволы (встроенш или первичные), вводимые через примитивы базового языка, и к< символы (вторичные), определяемые средствами самого ЛОКОНа.

Индивидными константами служат традиционные печатные npej ставления объектов данных, символы, упомянутые в фор defconstant Коммой Лиопа, а также ооылки на именованные екаемг ляры, называемые кообъектами. Роль билереманных играют дотаю чоскио переменные Коммон Лиспа, объявлешше в deivar. Коиерс менные вводятся формой defcovar, например:

(deicovar GV rtype number :default О.

:documentation "Напряжение заземления").

Определение биЕункций осуществляется макросом defblfur например:

(defbliun (POW number) ((base number) (log number)) "Бифункии: возведение в отепень и логарифм" (pow (base log) (expt base log)) ; главная бифункция (log (pow base) ; второотеп. бифункция

(If (plusp pow) (log роя base) unbound-value)) (base ; обычный параметр

(If (zerop log) unbound-value (expt pow (/ log)))))

Данная форма вводит в оигнатуру два функциональных оимво ла: pow и log. Последующие их вхождения в термы реализуюто экземплярами единственного встроенного клаооа ограничения pow Приведенное описание еоть результат разрешения функциональноп отношения относительно каждой из трех переменных pow, log i base. Вся спецификация напоминает одновременно формы flat (дл. бифункций) и let (для параметров) Коммон Лиспа. Для частично! бифункции метод вычисления может вырабатывать неопределенно« значение Лисп-конотанты unbound-value, а для для параметра -отсутствовать вообще, подразумевая, что опособ его вычисленш неизвестен.

Определение бипредиката осуществляется макрооом defblpred, который выглядит аналогично, но допускает единственный метод, возвращающий значение nil или не-nll.

Термы и формулы ЛОКОНа отроятся, как в языке CL, о поправкой на Лисп-синтаксис. Для облегчения записи вароаорвировань дно пропопиционолышо конотанты :t (иотина) и :i (ложь), при-

надлежащие типу logloal.

Вое формулы заключаются во внешние скобки #1 1 и внооятол в БЗ двумя способами. Первый способ — описание классов объектов о ограничениями, или коклаосов, например:

(defcoolass ТЕРМИНАЛ ()

((i :type number :documentation "Сила тока") (г .-type number documentation "Напряженно"))

О

:documentation "Отвод элемента электрической цепи")

(defcoolass РЕЗИСТОР () ((tl :type терминал) (t2 :type терминал) (г :type number îlnltarg :r

:documentation "Омическое сопротивление")) (Cailom Кирхгоф «[= ftl 1] (- Ct2 1])])) (Ом #[= (- ttl т] It2 vJ) (• tr] Ctl 11)])))

Определение кокласоа включает

- список имен прямых надкласоов;

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

- список классовых ограничений — формул, представляющих зависимости между слотами (или их частями), которым должен удовлетворять каждый экземпляр и которые, в то же время, представляют устройство для вычисления неизвестных компонентов; каждое из ограничений может быть поименовано, иметь документацию и квали&псатор :arloo или :hypothesis.

Все коклаосы, являются подклассами constrained-object. Именованный кообъект, экземпляр кокласоа РЕЗИСТОР о сопротивлением 4200 (ом), можно создать вазовом

(coobjeot г13 резистор :г 4200.0)

В формулах ссылки на копеременные, кообьекта и их части делаются при помощи путей, например: [gr], [г13], tr13 t1 il. Последнее ооотавное имя обеспечивает краткую нотацию для доступа к слоту.

Другой опособ введения формул в БЗ — посредством отдельных суждений, о помощью tell и axiom, которые активизируют процесс прямого вывода, например:

(axiom #[= tgv] [г13 t2 тП)

(tell »[imp (< (pow [r13 tl 1] 2) 36.3) [исправен]])

К числу косимволов оигнатуры относятся кофункции и копр дикаты, вводимые формами defcofun и defcopred.

(defcofun (R-ПАРАЛ number) ((г резиотор) (у резистор))

"Сопротивление двух параллельно соединенных резисторов"

(#t= (/ 1 Сг-парал]) (+ (/ 1 [х г]) (/ 1 [у г]))]))

(defcopred ПОСЛЕДОВАТЕЛЬНО <(х резиотор) (у резиотор).

&аих (г-total number))

(#t= Ir-total] (+ tx г] [у г))] #t1П [последовательно]

(= (- (X ti v) (y t2 v]) (• ir-total] tx ti 11))]

(defcopred ПУТЕШЕСТВИЕ (&key кто транспорт откуда куда))

Обе формы включает список .параметров (с типами), котор могут подразделяться на обязательные, ключевые (&кеу) и вспом< гательные (&аих), а также необязательный опиоок клаооовых orpi ничений, аналогичный указываемому в defcoclass. Ключевые арг; менты допустимо вадавать в произвольном порядке, как при вызо] функций Коммон Лиспа. Пример небезызвестного путешествия:

(tell *[путешеотвие :откуда 'Санкт-Петербург :куда 'Мооква :кто 'Радищев :трансшорт 'карета]).

Аппарат контекстов сиотемы ARCOS, наряду о идентификации противоречий, обеспечивает модульность БЗ. Контекот формирует* из предположений, сопоставляемых суждениям и клаооовым ограи чениям. Контекоты именуются и чаотично упорядочиваются по отн< шению достижимости, причем наибольшим элементом служит множа с во всех аксиом.

Все операции СПЗ выполняются в рамках фиксированного koi текота, либо текущего, как в случае

(tell #(последовательно (г13] [г14]]),

либо явно заданного посредством ключевого аргумента :contex например:

(tell *[= [г13 ti 7] 5.9] :context решение1)

Запрос и отображение результатов вывода/вычислений осуюе< твляютоя формой ask, которая воспринимает как формулы, так термы ЛОКОНа:

(ask (г-пврал [г13] (г151))

Операции над контекстами предусматривают создан

(defcontext), установку текущего (eet-context), разубеждение, т.е. удалопио предположения (forget), визуализацию противоречивых (show-nogoods) и всех предположений (shcw-aa) контекота.

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

1) Выбор базовых концепций, описание функций и предикатов.

2) Введение и/или переопределение классов объектов.

3) Порождение вкземпляров, моделирующих реалии ПО.

4) Выдвижение суждений относительно свойств объектов.

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

Указанные шаги синтеза (1-4) и анализа (5) могут повторяться, до тех пор пока полученные результаты не будут удовлетворять изначально заданным или сформированным по ходу требованиям. Процесс приводит к окончательной согласованной БЗ и излагается, в целом, на примере решения классической буквенно-цифровой головоломки SEHD + MORE = MONEY.

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

Приложение А содержит доказательства утверждений, приведенных в главах 2-4.

Приложение В дает раввернутую характеристику базовому инструменту программной реализации — интерпретатору Ylisp.

Наконец, в приложении В ошсываетоя синтаксис языка ограничений ЛОКОН в расширенной нормальной форме Бакуса.

ОСНОВНЫЕ РЕЗУЛЬТАТЫ ДИССЕРТАЦИИ

1. Разработана дедуктивная сиотема пропозициональной PCL и упорядоченно-сортной CL логик с четырехзначной семантикой, обеспечивающей адекватную трактовку неполной и противоречивой информации, представленной в БЗ; иооледованы формальные свойства этих логик.

2. С целью аффективной обработки предположений, сопоставленных явно введенным в БЗ фактам, формально иооледованы решетка и бирешетка меток — булевых многочленов, служащих для nupn-жония подцоржки выведенных формул в вычисленных значений термов.

3. Разработаны щмнципн объединения логических конструкций с ОО-средствами, представления их в виде системы булевых и упо-рядоченно-оортных ограничений. Воплощение этих принципов приво-

дит к оуцвотвенно гибридной и обаланоированной СТО.

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

5. Разработан декларативный язык описания ограничен ЛОКОН, включающий развитые средства структуризации понятий. Е преимущества проявляются на классе задач о небольшим чиол

■ независимо выбираемых- параметров и большим количеством вавио моотей: относительно простых математических в/или сложных лог ческих. Описана методология решения, которая носит интерпрет ционный характер, основана на постепенном заполнении БЗ и ра решении противоречий.

6. Программно реализованы СПЗ ARCOS и процессор язы ограничений ЛОКОН на базе YLisp — интерпретатора ОО-расширен языка K0M40H Лисп (CLOS). Общий объем исходных текстов — око 25 тыс. строк на языке Си и 10 тыс. строк на Коммон Лиспе.

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

1. Головачев А.Г., Иванов Д.А. Имитационный синтез концептуал ных схемв САПР. - U., МАИ, Деп. в ВИНИТИ 11.07.) N4527-B89, 58о.

2. Иванов Д.А. Логика времени при моделировании эволюции сноп мы. //В сб.: Методы прикладной математики в иооледовани. технических сиотем и математическое обеспечение ЭВМ. - м МАИ, Деп. в ВИНИТИ 15.01.88 N342-B88, о.201-208.

3. Иванов Д.А. О немонотонной выводимости в пропозиционалъга теориях. //В об.: Математическое обеспечение сиотем автом; •газированного проектирования. - М., МИЛ, 1989, о.22-30.

4. Иванов Д.А., Сигунов В.Р. Си-Лиоп-реаливация интерпретато] фреймового языка представления внаний. // Алгоритмы и пр< гракмы, В1ГГИЦ, 1991, N3, о.50. Рег.ном. 50910000079.

Факультет "Прикладная математика". Автор: 7\ м / f

тел. (095) 1 BU-4084, фвКО 1BQ-8077, JS¿/lCU)lt/£l

B-maili 1тппотг0кв04. malnet. malc. eu (y