Содержание к диссертации
Введение
1 Дескриптивные логики и табличный алгоритм вывода 15
1.1 Современные подходы к обработке знаний 15
1.2 Структура дескриптивных языков 18
1.3 Блок терминологии 23
1.4 Блок утверждений 25
1.5 Табличный алгоритм 27
2 Исчисление именующих ограничений 35
2.1 Общая схема 35
2.2 Основные определения 39
2.3 Система логического вывода 46
2.4 Корреляция с дескриптивной логикой 56
2.5 Корректность и полнота исчисления 60
2.6 Расширение исчисления 79
2.7 Революционный вывод в дескриптивной логике 81
3 Язык CLP и обобщенный подход к логическому программированию 83
3.1 Язык CLP(K) 83
3.2 Дескриптивные термы, как обобщение эрбрановых термов . 92
3.3 Амальгама, как обобщение унификации 94
3.4 Корректность обобщенного подхода 100
Заключение 103
Литература
- Структура дескриптивных языков
- Система логического вывода
- Расширение исчисления
- Дескриптивные термы, как обобщение эрбрановых термов
Введение к работе
Актуальность проблемы
В настоящее время ведется большое количество исследований, связанных с представлением и обработкой знаний, основную потребность в которых диктует развитие глобальной информационной среды Интернет. С развитием Интернета стало очевидно, что данная распределенная среда является мощным независимо-наполняемым банком знаний человечества. Проблемой сегодняшнего Интернета является неэффективная система поиска и обработки информации, которая функционирует на основе контекстного поиска данных. В сегодняшнем Интернете компьютер играет роль хранителя и передатчика информации, который предоставляет лишь достаточно примитивные средства поиска, оставляя интеллектуальную, системную и классификационную работу пользователю-человеку. При том объеме данных, которые сегодня накопились в мировой информационной среде, эта проблема становится ключевой. Для ее решения во главе с создателем мировой информационной паутины Т. Бернерсом Ли развивается концепция Интернета нового поколения — Semantic Web [19], где представление знаний должно реализоваться на основе логического формализма. На роль такого рода формализмов выбраны дескриптивные логики [17][32], обеспечивающие компромисс между выразительностью и эффективностью работы. Это означает, что с
теоретической точки зрения дескриптивные логики являются весьма простыми формализмами, поскольку они должны успешно работать в распределенной среде в реальном времени. Поэтому на них нельзя возлагать задачи сложного манипулирования системами знаний, например, реализацию таких метазадач, как развитие баз знаний, взаимодействие с внешним миром и т.д. Для таких внешних задач нужны иные формализмы. Ряд ведущих специалистов в области представления и обработки знаний (Я. Хоррокс, А. Сатлер, А. Леви, X. Боли и другие) в качестве основного претендента на эту роль рассматривают логическое программирование. С появлением еще одного формализма возникает и проблема взаимодействия «базового» формализма дескриптивных логик и «внешнего» формализма логического программирования [47]. Поэтому задача создания действительно эффективного механизма представления и обработки знаний, в основе которого лежит интеграция данных подходов, является актуальной.
Еще одной актуальной задачей является развитие систем выводов для дескриптивных логик. В настоящее время для этой цели используются табличные алгоритмы [48], имеющие переборную природу, что приводит к неэффективности в случае больших баз знаний (например, больших онтологии в области медицины или биологии), хотя здесь имеется ряд существенных достижений, например — системы Fact [27] и Racer [26]. Весьма интересным представляется подход, связанный с использованием большого опыта, накопленного в сфере автоматического доказательства теорем, в первую очередь, революционного тина. Ряд вычислительных экспериментов показывает, что даже универсальные
системы автоматического доказательства резолюционного типа, в частности, система Vampire [46], разработанная А. Воронковым, демонстрируют результаты, близкие узкоспециализированным решателям, основанным на табличных алгоритмах [49]. Поэтому разработка специализированных систем вывода, основанных на принципе резолюций, также имеет значительный потенциал.
Цели и задачи исследования
Диссертационная работа посвящена разработке логических основ работы со знаниями в распределенных информационных средах на основе интеграции дескриптивных логик и системы логического программирования.
Цель работы — создание интегрального логического формализма, реализующего эффективные механизмы представления и обработки знаний. В работе развивается формализм, который в качестве ядра содержит способ представления знаний, семантически подобный дескриптивной логике ALC, использует логический вывод резолюционного типа, и который обладает ключевыми свойствами корректности и полноты. Данный формализм объединяет преимущества дескриптивной логики и логического программирования. С практической точки зрения формализм ориентирован на использование в различных Web-сервисах, имеющих отношение к обработке знаний в контексте развития Интернета нового поколения — Semantic Web.
Для достижения этой цели решались задачи:
Разработка способа представления знаний на основе дескриптивных термов.
Разработка системы вывода дескриптивных термов на основе метода резолюций.
Обоснование корректности и полноты системы вывода.
Исследование свойств разработанного исчисления.
Разработка модели языка, реализующего интегральный подход к обработке знаний, который объединяет дескриптивный формализм с некоторой версией логического программирования в ограничениях.
Методы исследования. Основные методы, на которые опирается данная работа, принадлежат теории доказательств, теории вычислимости и теории моделей. Разработка исчисления именующих ограничений выполнена на идеях, заложенных в семантическом программировании. Система логического вывода в исчислении основана на принципе резолюций. Разработка обобщенного подхода к логическому программированию базируется на логике предикатов.
Научная новизна
В диссертационной работе рассмотрен новый подход [11] [39] к объединению средств логического программирования и дескриптивной логики, основной идеей которого является разделение этих двух уровней за счет перевода дескриптивного формализма на уровень термов. Данный интеграционный подход базируется на исчислении именующих
ограничений, разработка которого выполнена в работе. В этом обобщении дескриптивной логики заключается основное отличие от других гибридных подходов к обработке знаний (например, языков DLP [25], Carin [35], Dat-alogDL [40], AL-log [23]). Основными элементами исчисления именующих ограничений являются дескриптивные термы. Понятие дескриптивного терма вводится впервые, оно основано па идеях, заложенных в теории информационных ресурсов [12][7] и семантическом программировании [24][37].
В работе впервые вводится резолюционная система вывода для дескриптивных логик и термов.
Также впервые интеграция дескриптивных логик и логического программирования проведена таким образом, что получивишйся язык логического программирования в ограничениях является логическим обобщением чистого Пролога, дескриптивные термы являются естественным обобщением эрбрановых термов, а операция амальгамы, введенная на дескриптивных термах, является обобщением унификации.
Научная и практическая значимость работы
Работа ориентирована на решение актуальных проблем, возникающих сегодня в развитии глобальных сервисов обработки знаний.
Из-за бурного и неконтролируемого наполнения информационными ресурсами глобальная информационная среда постепенно превращается в собрание разрозненной и неупорядоченной информации, а контекстный поиск информации часто не позволяет получить доступ к действительно нужным данным.
Поэтому проблемы представления и обработки знаний находятся в фокусе внимания многих исследовательских групп, в частности, консорциума W3C. На данный момент устоявшихся технологий нет.
В работе предлагается новый подход к логической обработке знаний, который основан на комбинации средств дескриптивной логики и логического программирования. Данный подход может быть полезен как при разработке вариаций глобальной системы хранения и обработки знаний, так и при разработке отдельных сервисов.
В основном существующие формализмы представления знаний базируются на дескриптивных логиках. Однако дескриптивные логики, хоть и являются изящным и полезным средством для работы со знаниями, но не обладают достаточной гибкостью и больше сфокусированы на общую манипуляцию знаниями (например, решение задач классификации в базах знаний). В отличие от дескриптивных логик, логическое программирование хорошо настроено на явную обработку объектов, включая их процедурную обработку. Поэтому идея объединения дескриптивных логик и логического программирования может иметь серьезное практическое значение.
Также является востребованной разработка новых систем вывода для дескриптивных логик, т.к. табличные алгоритмы являются недостаточно эффективными в больших предметных областях. Система вывода, которая разработана в рамках работы, позволяет внедрить в дескриптивные логики резолюционную систему вывода, обладающую свойством полноты. Принцип резолюции хорошо изучен, и существует целый спектр разнообразных стратегий и оптимизаций, которые могут быть использованы и в дескриптивном случае.
10 На защиту выносятся:
Исчисление именующих ограничений: техника представления знаний на основе дескриптивных термов и резолюционная система вывода.
Доказательство полноты и корректности системы вывода исчисления именующих ограничений.
Построение модели языка, реализующего комбинированный подход к обработке знаний.
Теоретическое обоснование обобщенного подхода к логическому программированию.
Структура и объем диссертации
Диссертация состоит из введения, трех глав, заключения и списка использованной литературы.
В первой главе работы приводится обзор подходов к обработке знаний и рассматривается семейство дескриптивных логик, в том числе метод логического вывода — табличный алгоритм. В параграфе 1.1 выполняется обзор современных подходов к обработке знаний, В параграфе 1.2 рассматривается словарь дескриптивных логик, базовая логика и структура её расширения, понятие базы знаний. В параграфе 1.3 рассматривается структура терминологических описаний в базе знаний. В параграфе 1.4 рассматривается структура утверждений в базе знаний. В параграфе 1.5 дается описание системы вывода в дескриптивных логиках и формулируются её основные свойства.
Во второй главе вводится и исследуется исчисление именующих ограничений — выполняется построение языка и формулируется резолюциошіая система логического вывода с обоснованием свойства полноты. В параграфе 2.1 рассматривается общая схема построения исчисления NCC. В параграфе 2.2 вводится понятие дескриптивного терма, который берет свое начало в теории информационных ресурсов и является основным элементом языка, на котором построено исчисление. В параграфе 2.3 вводится резолюционная система логического вывода, состоящая из восьми правил синтаксической обработки дескриптивных термов. В параграфе 2.4 рассматривается корреляция дескриптивных термов и концептов дескриптивной логики. В параграфе 2.5, рассмотрена корректность правил вывода и выполняется обоснование свойства полноты исчисления NCC. В параграфе 2.6 рассматривается, как исчисление может быть расширено для решения большего класса задач. В параграфе 2.7 на основе правил логического вывода NCC выполняется построение базы резолюционной системы вывода для дескриптивной логики ALC.
В третьей главе на концептуальном уровне выполняется построение модели языка, реализующего комбинацию подходов логического программирования и исчисления именующих ограничений к обработке знаний. Разрабатывается теория обобщенного подхода к логическому программированию, построенная на основе исчисления NCC. В параграфе
рассмотрена модель языка логического программирования в ограничениях CLP(K). Показаны примеры решения логических задач, аспекты взаимодействия различных логических стилей. В параграфе
рассматриваются дескриптивные термы как обобщение термов
логического программирования. В параграфе 3.3 рассматривается операция амальгамы дескриптивных термов как обобщенный механизм унификации. В параграфе 3.4 приводится обоснование корректности обобщенного подхода к логическому программированию.
Основные результаты диссертации опубликованы в следующих работах:
Манцивода А.В., Липовченко В.А. Применение логического программирования к обработке знаний // Вестник Бурятского университета. Серия 13. Математика и информатика. - Улан-Удэ: Изд-во Бурят, ун-та, 2006. - Вып. 2, - С.50-57.
Mantsivoda A., Lipovchenko V., Malykh A. Logic Programming in Knowledge Domains // Lecture Notes in Computer Science. - Berlin: Springer, 2006. - P. 451-452.
Mantsivoda A., Lipovchenko V., Malykh A. Logic Programming in Knowledge Domains (Full version) // Известия ИГУ. Серия математика. T.l. - Иркутск: Издательство Иркутского ун-та, 2007. - С.188-204.
Липовченко В.А. Обобщенный подход к логическому программированию // Материалы VII школы-семинара «Мат. моделирование и информационные технологии» - Иркутск: Изд-во ИДСТУ СО РАН, 2005. - С.20-21.
Липовченко В.А., Манцивода А.В. Комбинированный подход к
обработке знаний // Труды всероссийской конф. «Телематика-2006». - С.-Пб., 2006. - С.59-61.
6. Липовченко В.А. Полнота исчисления именующих ограничений // Материалы Молодежной научно-практической конференции «Информационные технологии». - Иркутск, 2006. - С.12-14.
Апробация результатов
Основные результаты работы представлялись на Международной конференции по логическому программированию (Сиэтл, США, 2006), Всероссийской научно-практической конференции «Телематика» (Санкт-Петербург, 2006); VII школе-семинаре «Математическое моделирование и информационные технологии» (Иркутск, 2005); Молодёжной научно-практической конференции в рамках недели информационных технологий в г.Иркутске (Иркутск, 2006); семинарах кафедры информационных систем Иркутского государственного университета (2003 -2007гг.).
Личный вклад автора состоит:
В совместной с научным руководителем разработке исчисления именующих ограничений;
В самостоятельном обосновании полноты и корректности исчисления именующих ограничений;
В совместной с научным руководителем разработке модели языка, реализующего комбинированный подход к обработке знаний;
4. В самостоятельной разработке обобщенного подхода к логическому программированию с выполнением обоснования корректности.
Благодарности
Автор благодарит научного руководителя проф. А.В. Манциводу за неоценимую помощь при написании диссертации, а также команду аспирантов и студентов Иркутского госуниверситета за ценную помощь при апробации исчисления именующих ограничений и обобщенного подхода к логическому программированию.
Структура дескриптивных языков
Дескриптивными логиками [17] называется семейство формализмов, ориентированных на представление и обработку знаний (KR-формализмов). В данных формализмах знания о прикладной области (о мире) представляются с помощью определения отношений между понятиями (эти знания называют терминологией). Далее, используя эти понятия, определяются свойства объектов в домене (эти знания называют описанием мира).
Дескриптивные логики являются распространенным инструментом, на котором базируются системы описаний знаний. Доказательством этому служит то, что дескриптивные логики занимают ключевую позицию как система формализации знаний в концепции Интернета нового поколения — Semantic Web.
Дескриптивные логики эквивалентны небольшим фрагментам логики первого порядка и представляют собой компромисс между выразительностью и алгоритмической эффективностью.
Словарь дескриптивных логик состоит из концептов (понятий) и ролей (отношений). Концепты обозначают множества индивидуальных имен, роли обозначают бинарные отношения между индивидуальными именами.
Элементарными описаниями концептов являются атомарные концепты и атомарные роли. Сложные описания концептов могут быть построены из атомарных концептов индуктивно с помощью конструкторов. В абстрактной записи будем использовать буквы А и В для обозначения атомарных концептов, R - для обозначения атомарных ролей, буквы С и D - для сложных описаний. Языки различных дескриптивных логик (будем называть их дескриптивными языками) отличаются между собой наборами используемых конструкторов. Язык AL (Atributive Language) был представлен в работе [48] в 1991 году как минимальный язык, который представляет практический интерес. Другие дескриптивные языки являются расширением языка AL.
Описание концептов в AL может быть выполнено с помощью: атомарного концепта А, универсального концепта Т, нижнего концепта І-, атомарного отрицания - А, пересечения концептов С П D, ограничения значения V72.C, ограниченного квантора существования 3R.T. Заметим, в AL отрицание может быть применено только к атомарным концептам, и только универсальный концепт может быть в области действия квантора существования (за ролью R). Приведем пример, который может быть выражен в AL. Предположим, что Person и Female — атомарные концепты, тогда Person П Female и Person П - Female являются AL-концептами, описывающими интуитивно персоны женского пола и персоны не женского пола, соответственно. Если предположим, что hasChild является ролью, то можно сформировать концепты Person П 3hasChild.T и Person П VhasChild.Female, обозначающие, соответственно, персоны, которые имеют детей и персоны, все дети которых женского иола. Используя нижний концепт в Person П VhasChild.J-, можно описать те персоны, которые не имеют детей.
Чтобы формально определить семантику AL-концептов, рассмотрим интерпретацию /, которая состоит из непустого множества А7 (область интерпретации) и функции интерпретации, которая назначает каждому атомарному концепту Л множество А1 С Д7 и каждой атомарной роли R бинарное отношение R1 С Д7 х Д7. Функция интерпретации расширяется на описание любых концептов с помощью следующего индуктивного определения: Т7 = Д7 ±7 = 0 Ы)1 = д7\л7 {CUD)1 = 0 01 {MR.C)1 = {а є Д7У6.(а, Ь) Є R1 -+ b Є С1} (ЗЯ.Т)7 = {аєД73&.(а,6)єЯ7} Будем говорить, что два концепта эквивалентны (записывается С = D), если С1 = D1 для любой интерпретации /. Рассмотрим другие языки AL-семейства, которые получаются добавлением новых конструкторов и поэтому являются более выразительными.
Расширением языка AL любым подмножеством данных конструкторов получается отдельный дескриптивный язык. Каждый такой язык именуется как AL[U][E][N][C], где отдельные буквы в названии соответствуют присутствию соответствующего конструктора в языке. Например, язык ALEN — есть расширение языка AL конструкторами полного квантора существования и количественными ограничениями.
С семантической точки зрения не все данные языки различны. Семантически справедливы эквивалентности С U D = —(—«С П - D) и 3R.C = -iV.ft.-iC. Следовательно, объединение и квантор существования можно выразить, используя отрицание произвольного концепта. С другой стороны, с помощью объединения концептов и полного квантора существования, возможно выразить отрицание концептов. Поэтому считается, что объединение и полный квантор существования доступны в каждом языке, который содержит отрицание и наоборот.
Семантика концептов определяет дескриптивные языки как фрагмент логики предикатов первого порядка. Интерпретация / назначает каждому атомарному концепту и роли унарное и бинарное отношение над А1, соответственно, поэтому атомарные концепты и роли могут быть рассмотрены как унарные и бинарные предикаты.
Система логического вывода
Система логического вывода NCC, определяемая в данном параграфе, ориентирована на решение задачи проверки непротиворечивости множества именующих ограничений. Первым делом определим правила исчисления именующих ограничений, на которых базируется система. Система вывода в NCC базируется на принципе резолюций, однако модификации табличных алгоритмов также могут применяться для обработки дескриптивных термов. Принцип резолюций применим в системах обработки знаний. Это подтверждает известная система автоматического доказательства Vampire [46], которая успешно решает сложные классификационные задачи в реальных онтологиях [49].
Покажем сходство правила Res с принципом резолюций, которое достаточно очевидно. Для упрощения предположим, чтоіі, t2,t атомарные концепты. Т.к. семантика дескриптивных термов определяется аналогично семантике концептов в дескриптивных логиках, то, пользуясь способом отображения дескриптивных языков в фрагменты логики первого порядка, переведем посылку данного правила в эквивалентную формулу: (фх) V ti(ix)) Л ( с(гх) V t2(ix)) Л t(ix). (2.1) Используя дизъюнкты-посылки (c(ix) \ft\{ix)) и ( с{гх) Vt\(ix)), найдем бинарную резольвенту t\{ix) V t2(ix), которая эквивалентна логическому заключению правила Res, также переведенному в формулу. Чтобы показать сходство Any с принципом резолюций, рассмотрим несколько модифицированное правило вывода Any . ix:\ (p:c;fr),(p c; 2) ix :: $i; 2 Переведем посылку данного правила в эквивалентную формулу логики первого порядка: (Зу.{р{іх,у) Л с(у)) V ti(ix)) Л (4z.(p(ix, z) - c(z)) V t2(ix)). Предположим, что t\ и І2 атомарные концепты. После сколемизации и преобразования мы получим три дизъюнкта: р(іх, а) V t\{ix), с(а) V t\{ix) и p(x,z) V c(z) V t2(ix), где а - константа, полученная в процессе сколемизации у.
Дважды найдем бинарную резольвенту и получим желаемый результат t\(ix) V t2(ix), который имеет то же самое значение, что и логическое следствие ix :: t\;t2 правила Any . Таким образом видно, что применение правила вывода Any является аналогом нахождения последовательности бинарных резольвент.
Ниже будет показано что, в отличие от полного метода резолюций, который полуразрешим, благодаря «специализации» исчисление NCC является разрешимым. В системе вывода NCC невозможно применение правила резолюции к аксиомам - только к именующим ограничениям. Данное ограничение позволяет в практических задачах значительно уменьшить число шагов вывода. В процессе поиска доказательства аксиомы вводятся с помощью правила Ах. Данное правило может быть применено для любого гх1 Є А и любой аксиомы, определенной над А. В дескриптивных логиках (если терминология циклическая) применение аксиом оказывает значительное влияние на эффективность вывода, так как большое количество аксиом в терминологии приводит к комбинаторному взрыву. Например, ранние реализации табличных алгоритмов применяли все аксиомы к сгенерированным элементам, и это приводило к комбинаторно безнадежной ситуации. Наиболее эффективные реализации DL-решателей используют специальную технику, которая позволяет существенно уточнить необходимость применения аксиом к тем или иным элементам.
Одна из наиболее интересных задач, которая выходит за рамки данной работы, является разработка эффективных стратегий использования аксиом в NCC. Самая простая эвристика, которую можно предложить, заключается в том, чтобы применять правило Ах только к тем аксиомам, которые могут быть тут же вовлечены в применение одного из резолюционных правил Any или Res.
Правило Ата применяется к паре именующих ограничений гх :: t\ и гх :: Ї2 и позволяет объединять в одном именующем ограничении информацию о некотором объекте гх, заданную в конечном множестве именующих ограничений. Основным назначением данного правила является формирование именующих ограничений, к которым на следующем шаге применяются правила Res или Any.
Рассмотрим, например, правило Res. В посылке данного правила ix:: (c;ti), ( с; ), в общем случае может находиться некоторая дополнительная информация о ix, содержащаяся в терме t, но этот терм не фигурирует в логическом заключении, хотя правило Res, где логическое заключение есть ix :: t\;t2,t, также является корректным. Правило сформировано таким образом, чтобы не образовывались длинные описания с повторяющейся информацией. Если в выводе необходимо использовать именующее ограничение ix :: t\\t2,t, его можно получить предварительно с помощью правила Ата из ix :: (c;t\), ( с; ), і и ix::t\;t2. Заметим, что результат применения Ата будет ix :: (с; ti), ( с; Міі г и он не соответствует точно ix :: h;t2,t. Однако все правила преобразования настроены таким образом, что используют необходимые данные в дескриптивных термах, и поэтому нет необходимости вводить в систему правило, обратное Ата.
Правило Ех применяется для вынесения значения атрибутов на внешний уровень с целью выполнения дальнейших манипуляций с ними. Логическое заключение данного правила может быть, неформально, описано как «предположим что существует dx, такое что dx :: t».
Расширение исчисления
Рассмотренное исчисление NCC соответствует дескриптивной логике ALC(ALCO). Данная логика, хоть и представляет практический интерес, однако уступает в выразительности логике ALCN, в которой выразимы ограничения на количество объектов, обладающих тем или иным свойством.
Рассмотрим, как исчисление NCC может быть расширено до соответствия логике ALCN. Дополним определение дескриптивных термов семантическим аналогом количественных ограничений в ALCN. Если р Є Attr и г Є М U IX U S U Т$ , тогда р п и р п есть атомарные дескриптивные термы. Семантика данных дескриптивных термов запишется: (р п)1 = {а AJ{6(a, b) Є /} n} (р п)7 = {аєД7{6(а,Ь)є/} п} Система вывода, для данного расширения исчисления NCC, будет представлять собой комбинацию рассмотренного резолюционного подхода и механизма обработки количественных ограничений, который используется в табличном алгоритме На практике, дескриптивная логика ALCN, хотя и является достаточно выразительной, в задачах повышенной сложности является неэффективной, т.к. может приводить к большому перебору. Компромиссом между выразительностью и эффективностью, который можно принять для расширения исчисления NCC, является расширение NCC только до конструкции р 1. Семантика данной конструкции будет, соответственно, следующей: (р І)1 = {а Є А Щі Ь) Є Al l}.
Важно, что такое расширение является выразимым в исчислении NCC и, следовательно, соответсвует возможности эффективного вывода. Также, смысл такого заключения будет рассмотрен в следующей главе и основан на факте, что на базе данного расширения исчисления NCC возможно построение обобщенного подхода к логическому программированию.
В данном параграфе показывается, как на основе идей, заложенных в исчисление NCC, можно построить вывод резолюционного типа для классических дескриптивных логик. Как и в классическом методе резолюций, это исчисление работает с дизъюнктами. Поскольку для дескриптивных формул возможна только неполная конъюнктивная нормальная форма, правила построения которой представлены в параграфе 2.4, то дизъюнкты будут также неполными. Наш резолюционный вывод работает с множествами неполных дизъюнктов, которые представляют собой формулы вида С\ U ... U Сп, где СІ либо атомарные концепты, либо ролевые концепты VR.C или 3R.C, в которых С - формула в неполной конъюнктивной нормальной форме. Терминологические аксиомы также переводятся в множество неполных дизъюнктов. Например, эквивалентность A = \/R.(Bi П А), где А, ВІ - атомарные концепты, переводится в два неполных дизъюнкта - А U VR.(Bi ПВ2)иЛи a#.(-.#i U -,В2).
Пусть А - атомарный концепт, С и D произвольные концепты, R - роль, а, Ь - константы. Резолюционный вывод в дескриптивной логике будет базироваться на следующих аналогах правил вывода NCC: 1. Правило (DLRes). (Ли і)(а) ЫиР2){а) (DiUD2)(a) 2. Правило (DLAny). (ЗД.С1 U А) (а) (УДА U Ар (а) (3/?.(dnC2)UAUA)(a) 3. Правило (DLAx). Axiom{Di U ... U Dk) (Х?іи...иД0(а) 4. Правило (DLEx). {3R.{C1n...r\Ck)UD){a) (3R.{b}uD)(a) 0 ),...,0 ) 5. Правило (DLPerm). WW {a}(6) Множество ограничений CS состоит из аксиом и дизъюнктов. Чтобы доказать выводимость формулы F из CS, строится вывод пустого дизъюнкта L из множества СБиГ(а), где Г - множество неполных дизъюнктов, эквивалентных формуле -iF, а а - новая константа. Правила Ama, Subst, False исчисления NCC не имеют в данном исчислении аналогов, поскольку в случае дизъюнктов являются лишними. Проиллюстрировав возможность резолюционного вывода для дескриптивных логик, мы не углубляемся в изучение данной системы, поскольку это выходит за рамки поставленных перед нами задач. Заметим только, что леммы, относящиеся к системе вывода NCC, также справедливы для данной системы вывода в DL.
Дескриптивные термы, как обобщение эрбрановых термов
Рассмотрим свойства термов эрбранова универсума на основании которых можно утверждать, что данные термы могут рассматриваться как частный случай дескриптивных термов. Термы могут содержать частичную и неполную информацию. Это возможно, когда они не являются основными, и в них встречаются свободные переменные. Во время вычисления количество информации в термах становится больше, и она становится более точной. Это возможно за счет подстановок термов вместо переменных. Если даны два терма эрбранова универсума t\ и , то можно сравнивать и объединять информацию, содержащуюся в них. Сравнение и объединение информации могут быть выполнены благодаря наиболее общему унификатору. Пусть в — MGU{h,t2) — наиболее общий унификатор термов h и t i, тогда: h h, если h = h@, t t\V\ 2, если t — h$ = tiQ. Программы в логическом программировании состоят из предложений, выражающих знания о той задаче, для решения которых программа направлена. В формулировках этих предложений используются термы эрбранова универсума. Рассмотрим, как такие «знания» могут быть сформулированы с помощью дескриптивных термов. Возьмем в качестве домена знаний А эрбранов универсум Н. Терм t считается неполным, если содержит переменные. Можно считать, что неполный терм t описывает множество таких t Є Я, что i! — tMGU(t,t ), что означает t1 = {t Є H,t = tMGU(t,t )}. Терм t, который не содержит переменных, очевидно, описывает множество состоящее из одного терма t = t, т.е. является полным описанием. Далее определим правило представления эрбрановых термов из Н в виде дескриптивных термов. Дескриптивное представление эрбранова терма t обозначим через DT{t). Тогда: 1. если t - константа в виде атома вида /(), то DT(t) = /, ще f Є CN; 2. если t - константа отличная от атома, то DT(t) = t, где t Є М; 3. если t - переменная, то DT(i) = dxt, где dxt Є DX; 4. если t - некоторый терм вида f(h, tn), где / - функтор, h,...tn 94 произвольные термы, то DT(t) = f,argi : DT(ti),... ,argn : DT(tn), где / Є CN, argi,..., argn Є Attr.
He будем забывать, что в логическом программировании каждый функтор определяется с точностью до количества аргументов. Два функтора с одним именем, но разным количеством аргументов — суть два разных функтора. Рассмотрим пример дескриптивного представления. Пусть имеется терм p(Y,f(X),g(X,Z)) . Его дескриптивный аналог, в соответствии с правилом представления, запишется следующим образом: р,агдг : dxY,arg2 : (f,argi : dxx),arg3 : (g,argi : dxx,arg2 : dxz). Здесь dxy,dxxAxz временные имена. Подобно тому, как в процессе вывода могут уточняться переменные Y, X, Z, в обобщенном подходе должны будут выводиться именующие ограничения видачу :: ty. Не следует обращать внимания на громоздкость математического представления дескриптивных термов. В языке программирования дескриптивные термы имеют простую и естественную запись. Далее рассмотрим механизм обобщения операции унификации эрбрановых термов.
Одним из наиболее важных аспектов логического программирования является понятие унификации термов. Приведем некоторые конструктивные определения, связанные с понятием унификации. Данные определения будут полезны в обосновании корректности обобщенного подхода к логическому программированию. Определение 3.3.1 (1Щ, с.80) Подстановка - это конечное мпоэюеетво егіда {s\/v\ ...,sn/vn}, где каждая г;,- - переменная, каждый Si - терм, отличный от V\, все V{ различны. Подстановка, которая не содержит элементов, называется пустой. Определение 3.3.2 ([Ц], с.80) Пусть в = {s\/v\ ... ,sn/vn} -подстановка и t - терм. Тогда W - терм, полученный из t заменой одновременно всех вхождений переменной Vi{\ і п) в t на терм Sj. t9, называется примером t. Определение 3.3.3 ([Ц], с.80) Подстановка 0 называется унификатором для множества термов {t\,...,tk} тогда, и только тогда, когда t\0 — tiQ — ... = t\fi. Множество {t\,...,tk} называется унифицируемым, если для него существует унификатор.
По сути, для унифицируемых термов унификаторов может быть бесконечно много, но наиболее общий унификатор (MGU - Most General Unifier) будет всегда один. Определение 3.3.4 ([Щ, с.80) Унификатор а для некоторого набора термов будет наиболее общим унификатором тогда, и только тогда, когда для каждого унификатора в для этого набора существует такая подстановка X, что 0 = а о X .
Роль унификации — отождествление термов и конкретизация переменных. В языках логического программирования операция унификации является основной операцией логического вывода. По статистике [51], затрата ресурсов на выполнение унификации термов составляет примерно 80% от общих затрат ресурсов на выполнение логического вывода. От эффективности алгоритма унификации сильно зависит скорость выполнения логического вывода. Амальгама - операция, определенная на дескриптивных термах. Рассмотрим особенности выполнения операции амальгамы дескриптивных термов, относительно выполнения операции унификации их эрбрановых аналогов. Пусть ti и t2 - произвольные термы вида f(pi-..pk) и }{Гі...Гк)і соответственно. Транслируем t\ и t i в DT{i\) и DTfo), используя правило представления термов в дескриптивном виде: DT(h) = /, атдх : DT(Pl),..., argk : DT(pk), DT(t2) = /, arg, : DT(n),..., argk : DT(rk). Выполним для DT{t\) и DTfa) операцию амальгамы. По определению, амальгама DT(t\) П DT( ) — есть дескриптивный терм (DT(ti),DT(t2)), который запишется следующим образом: /, argi : DT{p1),..., argk : DT(pk), атд1 : DT(n),..., argk : DT(rk). (3.1) Алгоритм унификации для ti и ti, заключается в попарной унификации аргументов - и гг- с целью вывода подстановок. Из результата амальгамы 3.1 следует: чтобы обобщенный подход имел смысл, т.е. действовал аналогичный механизм вывода подстановок, нужно результат амальгамы дополнить условиями, кардинальности argi 1 для 1 г к. В этом случае каждый argi должен будет иметь не более одного значения. Добавим в 3.1 условия кардинальности, тогда результат должен будет принимать следующий вид: DTitjnDTfo) = ar9l : (DTfa) П DT(n)),.. .,argk : (DT{pk) П DT(rk)).
При выполнении операции амальгамы для каждой пары значений аргументов, а также подаргументов, таким же образом добавляя условия кардинальности, получим механизм вывода подстановок, аналогичный унификации. Данные условия кардинальности выразимы в рамках логики ALCO с помощью конструкции argi dx, где dx Є DX - новая переменная. Модифицированную таким способом операцию амальгамы для дескриптивных термов DT{t\) и DTfa) будем называть LP-амальгамой, и будем обозначать DT(t{) П DT(t2). Рассмотрим ещё одну особенность операции амальгамы. Пусть t\ и 2 - произвольные термы вида f(pi..-Pk) и 0(7 1.. .rfc), соответственно. Унификация данных термов невозможна, т.к. / ф д. Транслируем термы t\ и в DT{t\) и DT{t2): DT{h) = /, ar9l : DT{Pl),..., argk : DT(pk), DT{t2) = g, ar9l : DT(n),..., argk : DT(rk). Операция LP-амальгамы для данных дескриптивных термов может выполнятся, и её результат будет: f,g,ar9l : {UT(h) П DT(n)),...argk : (DT(tk) П DT(rk)). (3.2) Поэтому таким образом определенная амальгама не может служить обобщением унификации. Для решения данной проблемы достаточно далее модифицировать операцию LP-амальгамы следующим способом. В результат LP-амальгамы необходимо добавлять аксиому ( /; д) для различных функторов /ид, которая будет означать, что пересечение соответствующих концептов пустое. Аксиомы данного вида также необходимо добавлять при необходимости к результатам операций амальгамы, которые должны выполняться между значениями аргументов и значениями подаргументов.
