Содержание к диссертации
Введение 1
Глава 1. Пример разработки прикладных логических теорий 8
ІД Посі.шоїжа задачи 9
-
Предназначение рцзрабоышюп іеорнн , 11
-
ПрОбіСЧгі форЧііДЬНОІО IiptUCMIl Н'НПН 11
1.1 Сгр.\кт\ pa теории . . 1<">
їй Ofk \ ЛуЛгнис предетшппшоп теории . 21
1.С Проірлччная реализация 27
1.7 Обзор б.шзкпч раби і . . 29
18 Рез>дылш , ... 32
Глииа 2. Проблема синтаксической однозначности и разложимости 31
2 1 Непрерывная выборка информации . . . . Зі
2 2 Ііосіаноика проб іеми раио/кимоии . ... Н)
2 3 Приводимые теории . . 19
2 1 Разло/кнмые теории . 'Л
2 о Рез)лі>іаш ... GJ
Глава 3. Практические попросы разложимости GC
3 1 Конечно аксиоматизируемые теории ... . 67
3 2 Приведение к нредпкаїач 69
3 3 ChJJL'VOilChOt'OOOI.UlieHIie 71
З 1 Реі\тьтатьі . . 79
Заключение 80
Литература
Введение к работе
В настоящее время су щост вус і значительны; і пи і ер ее к методам и средствам декларативного представления знаний, коюрый. в частности, связан с недавно озвученной концепцией "Semantic Web" [l]-[lj и широко раснросіраненньїм понятием формальной онюлоши [5j-[7j. Ре-зулыаюм >іою являеісм разрабоїка и применение новыч компьютерных языков для формальної о представления знаний [G2, СЗ]. а ык-же сисіем поддержки логическою вывода. Каждый из новых языков сооївек iiijei пекоюрому подмножесшу лотки первою порядка, однако исходя in практики специалисты ничіілп осознавать необходимость использования данной лоппш целиком для работы с теми задачами, коюрьіееіали амуальны а последнее время. Среди них можно выделит поиск в обьемныч слабо сірумурированньїх хранилищах информации и шшчрапшо пмероюнных исючников данных.
В рачках данных задач декларашвные описания применяюн'я как іермпнолопіческие базы знаний, н коюрыч описаны іерминьї вмесче с заданной дли них аксиома і пческой осман шкой. Декларашвные іер-минолоїические базі)! знаний обычно прпняю рассчаїрнваїь с двух ючек зрения: как ірафьі счзязноеіп іерминов и как наборы лої ических уїверждений При лом ши])Око используемся понято связи юрминов по вхождению в одно (или близкие в определенной меірнке) высказывания.
Связи между іерминамн в задаче поиска даюі возможшх п> пере- формулировать (усиліпь/ослабпіь) запрос із завиеимосіи оі репльи-юв ею исполнения [S]. Аналопічно лому із задаче шпеї раніш свяш влішкл на ючносіь посіроенною оіобрсикення между двумя описаннями данных [9, 10] При лом аксиомы, заданные в деклараіпвном описании, непоередсіїзенио определяют піп связей между іермипамії [11, 12]. Для решения конкреіной задачи мої) г применяіься различные сіраіеіии. использующие разные іипьі связей в завиеимосіи or сиіуашш.
В данной рабоїе деклараишные описания знаний рассмаїриваюі-ся как (элементарные) іеории в лої икс первого порядка. Естественно, данное рассмоірснне не являсіся оригинальным п оно не може і бьпь гаковым в принципе, начиная с юіо времени, как был введен формальный аппараї логики.
С ючкії зрения связей ісрминов но вхождению для заданной іеории можно расечаїршшь различные компоненты сия шостії на множество сшнаїурньїх символов, используемых в записи предложений теории. Еегеспзенным образом оозішкаеі вопрос: являюіся ли компонешы связное їй одинаковыми для двух лоїпчески эквивалентных іеорий в одной и юй же сшншуре? В целом, ответ являсіся отрицаїельньїм и причина лому - синтаксическая су і ь нашею подхода. На практи-ке ото означает, что могут сущесівовать два множества предложений, коюрые семаншчески з-квивалентны. но синтаксически преде и» юны по-разному. Возможно ли німівестп теорию (аксиомы іеории) к ыко- му виду, по коюрому однозначно определяю!ся Компот1!!!!)! ПЇЯЗШК ПІ еш шпуры іеории? Данный вопрос предеіавляеі расширенную постановку проблемы разложимосіи, коюрая была сформулирована в 2003 і оду в связи с изучением формальных онюлоіпи (см. исходную формулировку в [13] и носіановку в главе 1 8). Суіь проблемы заключл-еіся в юм, как опрсделиіь, предеіавима ли произвольная заданная іеория в лоїике первою порядка и виде объединения двух (или более) icopiifi, имеющих непересекающиеся сіпнаїурьь
Вопрос разложимосіи и.мееі важное значение для формализации знании, поскольку разложимосіь означает возможность разбить формальное описание инісресующеП нредмепюи обласні на част, каждая из коюрых исиоль'зусі свои оїдельньїй алфавш, При попроешш формальною описания некоюі)ой нредмепюи облает часю оказываешь чіо данные, полученные оі экеперюв (или, например, извлеченные авюмашчески из ісксюв). предсіавляюі собой некоюрый набор фактов, которые необходимо структурировать, чтобы получить и ї них адекватную формальную модель. В частности, может бьпь интересно, существуют ли част знания, которые независимы друг оі друїа Эю в і очное і и шоівеісів}Єг вопросу разложимосіи. если рассматривать формальное описание нредмепюи облает как лої ическуго іеоршо (скажем, в некоюром іюдмножесіве лоїики пе])вою порядка) [35. 5G. 61].
В данной рабоїе решена проблема разложичосл и для произвольных элемсшарпых іеорий. Кроме тою. доказана однозначность разложения сшнгиірьі її самой теории (срочностью до формул чиеіою равенства) в случае ею существования. Таким образом, ласюяшая рабо і а }сіанавливаеі связь между подходом к рассмоіреншо синіаксической связанности іермшюії сючки зрения трафов и с точки зрения формул лоїики.
Цель работы исследование возможности декомпозиции (разложения) формальных описаний в логике первою порядка на компоненты с непересекающимися алфавитами; изучение вопроса синтаксической однозначности при использовании элементарных теорий в логике первою порядка как средства формальною представления знаний.
В результаїе рабоїьі авюром был сформулирован кршерий разло-жимосіи. доказана однозначность разложения іеорип на. перазіожн-мые компонент с точностью до формул чиє юю равенсіва. пока за но приведение іеории к іакому виду, по котрому однозначно определяется ее разложение.
Методы исследования: меюды логическою программирования и дедуктивных систем, аппарат математической логики и теории моделей.
Научная новизна
Разумы а і ы, подученные и рабоїс. являюіся новыми и сооівеіеів\-ют тенденции времени в част связанных с ними информационных задач. В часі носі и. до нас і он і цей рабо і ы несмелой an и я по решению проблемы разложимости в теории с дизъюнктными сш натурами не всіречались is публикациях. Но было показано ранее, чю ісория в лотке первою порядка определяв і компопешы связноспі сш шпуры однозначным образом. Также не была исследована взаимосвязь лих вопросов с современными носыновками задач информационною поиска и тисі рации НСЮЧІШК0В данных.
Практическая ценность
Полеченные резульїаі ы имеют ценное п. для задач поиска и иніе-і ранни данных с использованием декларативных баз шанпй. декомпозиции логических программ, распределенною исполнения лоїических операции, таких как проверка на непротиворечивость, над деклараї явными базами знаний большою обьема. Кроме юю, факім. показанные в работе, иредпавлнют интерес в связи с исследованием проб ими релшиштоипи в лої нке и философии.
Апробация работы
Резульгаш работы докладывались в рамках следующих научных всіреч: Infonnatik-200G - немецкой конференции но информаїике (і Дрезден, Германия), русско-немецком симпозиуме но бпоинформатке в 20051 оду {і. Билефельд, Гс])мания), семинаре СОМО (і. Да])мппаді.
Германия, 2005 г.). международной конференции по биоинформаїике BGRS'200G (Новосибирск. 200G і.), конференции "Технолоіпи Маї'Ік-рософі в информатике и проіраммированиим(Новосибпрк: 20UG і од). Международной Научной Сіуденческоп Конфеі)енции в 20031 оду (Новосибирск), а также иа семинарах и Инсіиіуіе сиеіом информаїики СО РАН. Пнииіуіе маїемаїики СО РАН, Пнеппуіе цию юі пи и іе-неіикн СО РАН.
По іемо дисссріашш опубликовано 10 начатых рабо і.
Структура и объем работы
Днсіеріацнонная рабоїа сосі ом і из введення, іреч глав и списка литературы. Объем диссертации - 89 сіраниц. Список литера іуры содержит G3 наименования. Рабоїа включает S рисунков.
Содержание работы
В первой главе описан оиьи создания авюром прикладной лоїп-ческой іеории в обласні биоїшформаїики.
Пока іьшаец-н. как іакие іеорнп мої у і возникнуіь иа пракіике при розрабоїке конкрепшх проіраммньїх приложений. Последоваїе.іьно изложены все основные шаіи от тсореіпческой рабо і ы до реализации в качесіве іі])0іі)а\і\шою продукт.
Данная глава прояеннеї с>іь подхода авю]їа. исходя иі пракіиче-ских соображений, и предлаїаеі досіаючио примеров для освоєння последующих глав.
Во второй главе изложены основные резулыаш рабоїьі Ашором сформулирован кршерий разложимосш дли прои вольной олеменіарнои і сорті, доказана однозначноеп. разложения сш на-іурьі в ди шонкпюе объединение, оівечающее разложению юорші. и однозначносіь разложения самой іеоріш с і очной ыо до формул чи-сюю равенства.
В третьей главе раесмаїриваюіси п])акшческие вопросы раио-жи.мосіи.
Рассмотіїен случай конечно аксиоматизируемых іеорий. введено попите веса сисісмьі аксиом, проблема разложимосш сведена к нахождению сие іемьі аксиом минимальною веса.
Изучены сіандаршьіе преобразования, іакие как сведение к преди-катоїі сіинаїуре искулемпзация. Усіановлено, чю пе])вое преобр.ізо-ванпс со\])аняеі сііойсіво разложимосш Для вюрою преобразования показано, то. хогя оно и не сохраняет ратюжимосчь. все равно свойство разложимости исходной теории может быть распознано после ею применения. Оба преобразования определяются формулами исчисления ИреДИКаЮ» И ІірИВОДЯІ К 60ЛСЄ ПрОСЮМу ВИДУ ПреДЛОЖеНШ'І 1С0-
