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

Российская Академия Наук Сибирское Отделение Институт систем информатики имени А.П.Ершова

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

ПОНОМАРЁВ Денис Константинович

Синтаксическая однозначность при представлении знаний в логике первого порядка

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

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

Научный руководитель -профессор А.Г.Марчук

Новосибирск 2006

Работа выполнена в Институте систем имени А.П. Ершова СО РАН

информатики

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

Марчук Александр Гурьевич, доктор физико-математических наук

Официальные оппоненты:

Морозов Андрей Сергеевич, доктор физико-математических наук

Витяев Евгений Евгеньевич, кандидат физико-математических наук

Ведущая организация:

Институт автоматики и процессов управления ДВО РАН

Защита состоится 26 декабря 2006 года в 16 часов 00 минут на заседании диссертационного совета К003.032.01 в Институте систем информатики имени А.П. Ершова Сибирского отделения РАН по адресу:

630090, г. Новосибирск, пр. Акад. Лаврентьева, 6.

С диссертацией можно ознакомиться в читальном зале библиотеки ИСИ СО РАН (пр. ак. Лаврентьева, 6).

Автореферат разослан ноября 2006 г.

Ученый секретарь Диссертационного совета, ! 1■ Мурзин Ф.А.

к.ф.-м.н.

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

Актуальность проблемы

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

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

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

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

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

связности сигнатуры теории? Данный вопрос представляет расширенную постановку проблемы разложимости, которая была сформулирована в 2003 году в связи с изучением формальных онтологий. Суть проблемы заключается в том, как определить, представима ли произвольная заданная теория в логике первого порядка в виде объединения двух (или более) теорий, имеющих непересекающиеся сигнатуры.

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

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

Цель работы

- исследование возможности декомпозиции (разложения) формальных описаний в логике первого порядка на компоненты с непересекающимися алфавитами;

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

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

Методы исследования:

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

Научная новизна

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

Практическая ценность

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

Апробация работы

Результаты работы докладывались в рамках следующих научных встреч: Informatik-2006 - немецкой конференции по информатике (г. Дрезден, Германия), русско-немецком симпозиуме по биоинформатике в 2005 году (г. Биле-фельд, Германия), семинаре COMO (г. Дармштадт, Германия, 2005 г.), международной конференции по биоинформатике BGRS'2006 (Новосибирск, 2006 г.), конференции "Технологии Майкрософт в информатике и программировании" (Новосибирск, 2006 г.), Международной Научной Студенческой Конференции в 2003 году (Новосибирск), а также на семинарах в Институте систем информатики СО РАН, Институте математики СО РАН, Институте цитологии и генетики СО РАН.

По теме диссертации опубликовано 10 печатных работ.

Структура и объем работы

Диссертационная работа состоит из введения, трех глав и списка литературы. Объем диссертации - 89 стр. Список литературы содержит 63 наименования. Работа включает 8 рисунков.

Содержание работы

В первой главе описан опыт создания автором прикладной логической теории в области биоинформатики.

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

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

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

Нами было разработано формальное представление анатомии "модельно-го"растения Arabidopsis thaliana в развитии, которое используется для навигации в базе данных экспрессии генов этого растения и анализа взаимосвязей фенотипических аномалий. Само формальное представление является набором предложений логики первого порядка, реализованных программно в виде дедуктивной базы данных в системе Protégé.

Разработки по формальному описанию анатомии в развитии, равно как и сама база данных были выполнены в Институте Цитологии и Генетики СО РАН, внедрены в этом институте и являются частью проекта "Computable Plant"(ИЦиГ СО РАН; Институт Геномики и Биоинформатики, Университет Калифорнии, Ирвайн, США; Отдел Биологии, Технологический Институт Калифорнии, Пасадена, США; <http://computableplant.org>).

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

Среди растений в биологии, как модель, выделен вид Arabidopsis thaliana. Согласно международной исследовательской инициативе, к 2010 году распознанные функции каждого из генов этого растения должны быть интегрированы в генные сети, дополняя и/или корректируя их. Информация о генах Арабидопсиса, накопленная к настоящему времени, должна помочь в систематизированном освоении новой информации о растении и использовании ее для других видов.

Описание функций генов на уровнях РНК, белков, клеток, тканей, а также на уровне органов и всего организма для разных генотипов являются сложными и емкими знаниями. Огромный объем разрозненной информации из публикаций требует объединения и систематизации для того, чтобы понять, что уже известно об экспрессии генов Арабидопсиса и что еще предстоит узнать. В связи с этой задачей в Институте Цитологии и Генетики СО РАН была разработана и постоянно развивается база данных AGNS (Arabidopsis GeneNet Supplementary database), которая является открытым Интернет-ресурсом (http://www.bionet.nsc.ru/agns) и предоставляет доступ к описанию функций известных генов Арабидопсиса на различных уровнях

мРНК, белков, клеток, тканей, а также уровне органов и всего организма в целом, как для дикого, так и для мутантных типов.

Вся информация содержится в двух модулях AGNS: базе данных по экспрессии генов и базе данных по фенотипам растения (смысл данных поясняется в разделе 2 первой главы диссертации). Кроме того, разработаны два контролируемых словаря содержимого базы данных. В дополнение к этому потребовалось разработать формальное описание анатомического строения растения на уровне клеток, тканей и органов в развитии. Следуя популярным терминам в инженерии знаний, для краткости в данной работе мы называем это формальное описание онтологией. Основой для создания онтологии послужили статьи по паттернам экспрессии генов, фенотипам и непосредственно процессам развития растения.

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

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

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

Anatomy _Elementl Developmental __Stagex

Has_Developmental_Stage2(Anatomy_Element x Developmental_Stage) Bef ore2(Developmental_Stage x Developmental_Stage) Occurs_In2(Developmental_Stage x Developmental_Stage)

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

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

Vx3s(Anatomy_Element(x) —» Has_Developmental_Stage(x,s)) (1)

Vs->(Occurs_In(s, s) V Before(s, s))

(2)

Vx, Si,S2~>{Has_Developmental_Stage(x, si)A

Has_Developmental_Stage(x, s2) A Occurs_/n(sj, 52))

(3)

V«!, s2->(Before(sl, s2) A Occurs_/n(si, S2))

(4)

Vsi,S2,S3(J3e/ore(si,s2) A Before(s2,s3) —► Before(slts3)) (5)

VSi, S2t S3(OcClirS_/n(sj} S2) A Occurs_In(s2, S3) —*■ Occurs_/n(Si, S3)) (6)

С точки зрения практической реализации, предложения 1-4 задают ограничения на содержание фактов об индивидуумах, вводимых в онтологию. Предложения 5, б определяют транзитивность отношений Be fore и Occurs _1п и, фактически, задают правила для вывода новых фактов из уже имеющихся.

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

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

о S - стадия развития; найти стадии раньше/позже S.

о А - анатомический элемент, S - его стадия развития; найти элементы, принадлежащие А на стадии S.

о А - анатомический элемент, S - его стадия развития; найти элементы, содержащие А на стадии S.

о А - анатомический элемент; найти анатомические элементы, из которых он развивается.

о А - анатомический элемент; найти анатомические элементы, которые развиваются из А.

о А, В - анатомические элементы; найти стадии, которые претерпевает А, будучи частью В.

о А, В - анатомические элементы; найти стадии, которые претерпевает А, в то время как он содержит В.

о А, В - анатомические элементы; является ли А частью В на некоторой стадии развития В (или А)? (по-другому: является ли А частью В когда-либо?).

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

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

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

2)развитие многих анатомических элементов описывалось в статьях в виде "X обладает следующими свойствами, когда Y находится на стадии S " (например, "LDS2 leaf shows meristematic divisions throughout the mesophyll"), но в то же время подобные описания приводились лишь для некоторых стадий Y.

Это привело к необходимости введения искусственных стадий развития у анатомических элементов.

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

В выборе практической реализации мы руководствовались двумя побуждениями: применить достаточно широко распространенный и достаточно выразительный язык представления онтологий, а также использовать редактор онтологий, обладающий богатыми функциями импорта-экспорта и визуализации. В результате это привело к выбору языка OWL-DL и редактора Protégé (версия 3.1, http://protege.stanford.edu), а сама теория была реализована как дедуктивная база данных в этой системе. Текстовая информация о

развитии растения Arabidopsis thaliana, выделенная из научных статей, была представлена в формальном виде.

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

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

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

В процессе исследований было проведено сравнение разработанной теории с широко известными информационными ресурсами "TAIR"h "Plant Ontology", которые предоставляют таксономии терминов по анатомии и развитию растений (в частности, и модельного растения Arabidopsis thaliana). В частности, была проанализирована связь терминологических систем и структур данных в онтологии, разработанной консорциумом "Plant Ontology", и онтологии, разработанной автором. В результате было доказано, что формальное представление, разработанное автором, превосходит разработку консорциума в возможности использования для анализа экспериментальных данных высокой детализации по времени.

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

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

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

Определение 1 Рассмотрим сигнатуру £ и теорию Т этой сигнатуры. Теория Т - разложимая, если можно подобрать такое дизъюнктное разложение сигнатуры Е = Е1иЕ2, Е1ПЕ2 = 0, Е1 ф 0 ф Е2 и такую систему аксиом теории Б, которая представляется объединением 5 = ¿"1 и в котором в формулах г = 1,2 используются только символы из части Е< сигнатуры Е. Будем далее обозначать разложение теории как Т= <8> 52, а разложение сигнатуры как Е = Е1 Ц Е2.

Для произвольной теории Т можно было бы рассматривать тривиальное разложение, в котором Е1 = 0 или Е2 = 0, а множество формул 51 (соответственно ¿>2) образовано формулами чистого равенства теории 7", предложениями теории не использующими сигнатурных символов. Однако такое разложение малосодержательно, поэтому, согласно введенному определению, далее под разложимой теорией будем понимать такую теорию, которая обладает нетривиальным разложением, в котором Ех ф 0 ф Е2. Если имеются только тривиальные разложения, то теорию будем называть неразложимой.

К примеру, если сигнатура Е состоит только из одного предиката, то любая теория этой сигнатуры Е (даже определенная пустым множеством аксиом) неразложима.

Проблема 1 Рассмотрим теорию Т сигнатуры Е, определенную некоторым множеством замкнутых формул Ф сигнатуры Е. Как исходя из системы аксиом Ф определить разложимость теории Т ?

Проблема 2 Рассмотрим конечно аксиоматизируемую теорию Т сигнатуры Е, определенную некоторым конечным множеством предложений Ф сигнатуры Е. Как исходя из системы аксиом Ф определить разложимость теории Т?

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

Определение 2 Рассмотрим теории ¿>1, ¿>2 дизъюнктных сигнатур Еь Ег; Е! Л Е2 = 0, Е2.

Теория Т сигнатуры Е = Е1Ц Е2 разлагается в произведение теорий Бх, (обозначаем Т = если она получается дедуктивным замыканием всех предложений теории «5>1 (сигнатуры и всех предложений теории $2 (сигнатуры в исчислении предикатов расширенной сигнатуры Е : £1, 1- Т.

При этом теории называем компонентами (разложимости)

теории Т.

Основываясь на интерполяционной теореме Крейга, в работе доказано, что для любой (элементарной) теории Т сигнатуры Е можно однозначно определить дизъюнктное разложение сигнатуры Е = Е1 Ц ... Ц £„, которое с точностью до перестановки сомножителей отвечает любому разложению теории Т=.5>1®.. на неразложимые компоненты разложимости - теории сигнатуры E¿, г = 1,... , п (см. теорему 1 ниже). Также показано, какие шаги необходимо выполнить для того, чтобы привести систему аксиом теории к такому виду, по которому однозначно определяется это разложение.

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

Обсуждение данных проблем следует начать с такого замечания.

Замечание 1 Если теорию Т сигнатуры £ можно определить такой системой аксиом, в которой используются только символы части сигнатуры £' С 2, то такая теория - разложимая. Она разлагается на теорию меньшей сигнатуры и теории символов из дополнения £\£', определенные множествами тождественно истинных предложений.

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

Определение 3 Рассмотрим сигнатуру £ и теорию Т этой сигнатуры. Теория Т - приводимая, если можно подобрать такое подмножество Е' С S сигнатуры £ и такую систему аксиом теории S, в формулах которой используются только символы из части £' сигнатуры £. В этом случае будем говорить точнее, что теория Т приводится к теории Т' меньшей сигнатуры £'.

Если же такое невозможно, и любая система аксиом теории Т использует все сигнатурные символы, то теорию Т называем неприводимой.

Символы сигнатуры £ теории 7~, которые невозможно исключить из любой ее системы аксиом, называем существенными (символами теории

Г).

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

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

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

Замечание 2 Рассмотрим сигнатуру £' и ее расширение £.

Пусть ф игр - предложения меньшей сигнатуры причем в исчислении предикатов большей сигнатуры £ выводима секвенция ф ф. Тогда эта секвенция выводима и в меньшей сигнатуре £'.

Предложение 1 Рассмотрим расширение сигнатуры £' С £ и теорию "Р сигнатуры £' соответственно. Рассмотрим предложение <р сигнатуры £.

Тогда если формула tp следует из теории V, то найдется предложение в теории "Р такое, что в включает только те символы сигнатуры £', которые встречаются в формуле <р и из которого предложение ip следует: Vb-в, в

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

Определение 4 Рассмотрим теорию 7* и предложение теории <р €7*.

Предложение <р назовем приводимым в теории 7", если найдется такое предложение в теории Т, в €7", которое использует строго меньшее число сигнатурных символов формулы (р, и выполнена секвенция 0\- <р. При этом, предложение в назовем сужением формулы <р в теории Т.

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

Замечание 3 Любая неприводимая формула <р теории Т включает только существенные символы теории Т.

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

Предложение 2 Пусть Т - теория сигнатуры Е. Рассмотрим множество существенных символов Е' сигнатуры Е; Е' С Е.

Тогда теорию Т можно определить некоторой системой аксиом сигнатуры Е'. При этом, данная система аксиом в сигнатуре Е' определяет неприводимую теорию Т.

Далее в работе рассматриваются уже неприводимые теории и неприводимые системы аксиом.

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

Предложение 3 Рассмотрим разложение сигнатуры Е = Е1 Ц Ег и теории сигнатур Ех, Ег соответственно. Рассмотрим предложение <р сигнатуры Е.

Тогда если следует из объединения теорий Н V?, то найдутся такие предложения в и ф теорий V и О. соответственно, из которых следует предложение : Т* в, 0.\- ф, в, ф Ь <р, причем, предложение в включает только такие символы сигнатуры Еь которые встречаются в формуле а предложение ф содержит только те символы сигнатуры Ег, которые используются в формуле <р.

Из предложения 3 выводится способ установить разложимость теории Т. Для его описания определим понятие разложимого предложения теории.

Определение 5 Рассмотрим теорию Т и предложение теории <р €7".

Предложение у назовем разложимым в теории 7", если найдутся такие предложения в и ф теории 7", в ЕТ, "ф €7", которые включают символы

1.4

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

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

Замечание 4 Если предложение <р теории Т неприводимо, то фрагменты его разложения в и "ф также являются неприводимыми предложениями теории.

Для теории Т через Т* обозначим теорию чистого равенства, содержащуюся в Т. Она определяется замкнутыми формулами чистого равенства, принадлежащими теории Т. Для произвольной теории «5 через (<5>, 7"#) обозначим теорию 5 вместе с предложениями чистого равенства теории Т.

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

Лемма 1 При любом разложении теории х®^ в произведение теорий сигнатур £1,1)2 соответственно (Пх ф 0 ф И2) каждое неразложимое предложение <р теории Т, включающее сигнатурные символы, выводится либо только из теории (^^Т*), либо только из теории (52,7"*).

Если формула к тому же, неприводима, то она содержится либо в теории сигнатуры £1, либо в теории ,7"*) сигнатуры £2. В

частности, она содержит символы либо только из сигнатуры £ь либо только из сигнатуры £2.

Следствие 1 Рассмотрим произвольное нетривиальное разложение теории Т = ® ... ® Тогда любое неприводимое и неразложимое предложение теории 1р 6 7" принадлежит некоторой теории

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

Следует формализовать полученные результаты с помощью следующего ниже понятия. Приведем его для произвольной системы аксиом Ф некоторой теории сигнатуры £.

Определение 6 Два сигнатурных символа Р, ф € £ называются непосредственно связанными (системой аксиом Ф теории Т), если Р и ф входят в одну аксиому -ф € Ф.

Символы Р, С} называются связанными (системой аксиом Ф), если найдется такая последовательность символов Р — Т\,..., Т, = в которой любая соседняя пара Т», Т<+1 связана непосредственно.

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

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

Определение 7 Две аксиомы (р,ф € Ф назовем непосредственно связанными, если они содержат некоторый общий символ сигнатуры Е.

Аксиомы <£>, ф назовем связанными (системой аксиом Ф) если найдется такая последовательность аксиом из Ф : <р = ф\,—, фч = ф, в которой любая соседняя пара ф¿, связана непосредственно.

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

Применим введенные выше определения 6,7 к максимальной системе неприводимых и неразложимых аксиом Ф(Т) неприводимой теории Т. Определим стандартные компоненты связности сигнатуры Е = Е1 Ц... Ц £„ относительно этой системы аксиом. Построим стандартное разложение теории на компоненты разложимости, отвечающее этому разложению сигнатуры.

По построению каждая аксиома из системы Ф(Т) содержит символы только из какой-то одной дизъюнктной части сигнатуры Е,-. Обозначим для каждого г = 1,..., п через все аксиомы, содержащие символы из Е<. Поскольку теория неприводимая, каждый символ сигнатуры присутствует в некоторой аксиоме из Ф. Значит, - множество аксиом соответствующей компоненты связности системы аксиом. Вместе эти множества аксиом определяют стандартное разложение теории Т^Бх <8>... ® Бп.

Заметим, что аксиомы г = 1,..., п определяют неразложимые теории. Действительно, если бы некоторая система определяла разложимую теорию, то по лемме 1 сигнатура Е,- и система аксиом £4 была бы несвязна. А по построению это компонента связности.

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

Лемма 2 Любые системы неприводимых и неразложимых аксиом Ф неприводимой теории Т определяют одно и то же отношение связности на символах сигнатуры Е теории Т. В частности, они определяют одни и те же компоненты связности Е*, г = 1,..., п сигнатуры Е.

Лемма 3 Пусть Т - неприводимая теория сигнатуры Е, а Е = Е1 Ц ... Ц £п - есть стандартное разложение сигнатуры на компоненты связности.

Рассмотрим произвольное разложение теории на компоненты Т=Т 1® ...<8>Тт. Тогда разложение сигнатуры, отвечающее этому разложению теории, получается из разложения Е = Ех Ц... Ц Еп объединением некоторых компонент Е*.

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

Лемма 4 Пусть теория Т сигнатуры Е = ЕхУЕг разлагается в произведение теорий5х и^г дизъюнктных сигнатур Ех,Е2, ЕхПЕ2 = 0>Ех ф 0 ф Е2. Предположим, что эти теории содержат все формулы чистого равенства теории Т: г = 1,2.

Тогда каждая теория состоит из всех предложений теории Т, которые включают только символы из части сигнатуры Е*, {<р € (р 6 7"}, г = 1,2. В частности, такое разложение определяется по разложению сигнатуры однозначно.

Замечание 5 Утверждение леммы 4 легко обобщается на случай произвольного числа сомножителей в разложении теории.

Теорема 1 Для любой неприводимой теории Т сигнатуры Е однозначно определяется дизъюнктное разложение сигнатуры Е = Ех Ц ... Ц Е„, которое с точностью до перестановки сомножителей отвечает любому разложению теории Т=3х<2).. .®Зп на неразложимые компоненты разложимости Si - теории сигнатуры Е<, г" = 1,...,п. Зафиксируем некоторое такое разложение.

Для произвольного разложения теории на неразложимые компоненты Т = Т, О ... ® Тт имеем п = т и после подходящей перенумерации компонент каждая теория отличается от теории некоторыми предложениями чистого равенства из исходной теории Т : (5;,Т*)=(Т<,Т#).

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

Для произвольного г = 1,..., п обозначим через теорию сигнатуры Е*, порожденную системой аксиом образующей компоненту связности системы Ф. Также обозначим через - теорию вместе с предложениями чистого равенства теории Т. Имеем разложение теории на неразложимые компоненты 7~=«5'х®. .

Рассмотрим произвольное разложение теории на неразложимые компоненты Т—Т\. .®Тт. По лемме 3 сигнатура каждой компоненты Т,- получается объединением некоторых компонент Е^., = 1,...,п стандартного разложения общей сигнатуры.

Дополним каждую теорию формулами чистого равенства: Тогда также имеем Т=Т'х<8>.. .<8>7~'т.

В силу леммы 4 и замечания 5, заключаем, что каждая теория Т'^ образована всеми формулами теории Т, которые включают символы из соответствующей ей сигнатуры Ду. Однако по лемме 3 Д7 получается объединением некоторых Е*, г = 1,2,..., гг.

Для произвольного з рассмотрим произведение теорий сигнатур Е,С Aj. Оно содержится в теории Т, является непротиворечивым и определенным. Применяя замечание 5, получаем, что теория совпадает с этим произведением. В силу неразложимости теории Т7,-, она совпадает с некоторой теорией использующей те же символы сигнатуры.

Этим построено отображение j —► г. Компоненты разложения по

замечанию 5 однозначно определяются используемыми символами сигнатуры - компонентами стандартного разложения Х^. Поэтому это отображение разнозначно. Сюръективность отображения очевидна, так как, в силу разложимости, любой символ сигнатуры должен использоваться некоторой теорией Т'й.

Тем самым теорема 1 доказана.

Из леммы 2 следует, что для определения компонент связности сигнатуры достаточно использовать любую систему (Ах)" аксиом теории, образованную неприводимыми и неразложимыми предложениями. Ее нетрудно получить исходя из неприводимых аксиом (Ах)' теории Т.

Действительно, согласно предложению 2 для теории Т существует система аксиом (Ах)', состоящая из неприводимых предложений. Применим к этой системе следующие преобразования.

Каждую разложимую аксиому V? € (Ах)' заменим на ее фрагменты в, гр, каждый из которых выводится из (Ах)' и для которых в,ф Ь (р. Неразложимые аксиомы не изменяем. Обозначим полученную после преобразования систему аксиом как Т(Ах)'.

По построению система аксиом Т(Ах)' также определяет теорию Т. Будем повторять это преобразование и построим последовательность систем аксиом Т(Ах)\ Т^Лх)',----

Каждая формула содержит лишь конечное число сигнатурных символов, поэтому каждая аксиома (р из (Ах)' может быть последовательно разложена только конечное число раз (оговоримся, что рассматримаемые сигнатуры - конечные). Таким образом, начиная с некоторого п в системе аксиом Ттп(Ах)', тп^ п, будут только неразложимые фрагменты аксиомы (р.

Обозначим через (Ах)" такие предложения <р, каждое из которых встречается во всех членах построенной последовательности кроме, может быть, конечного их числа. Это неразложимые фрагменты аксиом из (Ах)'. По замечанию 4 система (Ах)" состоит из неразложимых и неприводимых предложений теории Т и представляет систему аксиом теории Т.

С учетом леммы 2 система неприводимых и неразложимых аксиом (Ах)" теории Т определяет разложение сигнатуры, а с учетом леммы 3 и самой теории. Вместе с заключительным утверждением леммы 3 это приводит нас к критерию разложимости элементарной теории Т.

Критерий разложимости Теория Т сигнатуры £ является разложимой

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

В третьей главе рассматриваются практические вопросы разложимости.

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

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

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

Определим вес формулы ф как натуральное число

и)(ф) = ЗпрМ = 3*{зирр(ф)).

Замечание 6 Основание степени 3 выбрано так, чтобы для любых натуральных чисел п, т выполнялось неравенство Зп+т > Зп + Зт (в частности, чтобы суммарный вес фрагментов разложения формулы был всегда меньше, чем вес самой формулы).

Определение 8 Весом системы аксиом Ф теории Т назовем сумму весов составляющих ее аксиом:

™(ф) = !>(*>■

Минимальной системой аксиом теории Т будем называть такую систему аксиом Ф, вес которой минимален.

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

Предложение 4 Пусть Ф - есть минимальная система аксиом теории Т. Тогда она образована такими предложениями теории Т, которые являются одновременно неразложимыми и неприводимыми.

В решении проблемы разложимости сигнатуру £ можно предполагать предикатной, включающей только символы предикатов. Для этого в работе используется стандартный способ представления функций х =/(х\%... ,хп) их графиками Р(х1,... ,х„, х)(= 0) и показывается, что свойство разложимости при этом сохраняется.

Более точно, рассматривается преобразование (обозначено в работе как ') теории, соответствующее этому представлению, и для него доказывается следующее предложение.

Предложение 5 Рассмотрим теорий Т сигнатуры £ и преобразование ' формул сигнатуры £ в формулы предикатной сигнатуры £', описанное выше.

Тогда Т разложима тогда и только тогда, когда разложима производная теория Т'.

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

Замечание 7 Если теория Т конечно аксиоматизируема, то она определяется одной формулой ф сигнатуры £. Тогда её скулемовское обогащение в расширенной сигнатуре £* определяется универсальной формулой ф* и скулемовскими предложениями 5. Во всяком случае, ф* Ь Т.

В общем случае теория определяется некоторой системой аксиом Ф. Её скулемовское обогащение Т* определяется соответствующим набором универсальных формул Ф* сигнатуры £* и теорией скулемовского обогащения 5. При этом Ф* I- Т.

Конечно, добавление к теории формул новой сигнатуры £* нарушает разложимость - появляются неразложимые формулы <р*. с символами из обеих сигнатур (исходной и Д = | ф = (3 х)^р(х, ху,.хп), (р- формула сигнатуры £}). Поэтому требуется расширить определение разложимой теории. Используем предикатность сигнатуры £, считая, что функциональные символы появляются только при скулемизации.

Определение 9 Рассмотрим теорию Т предикатной сигнатуры £. Теория Т называется относительно разложимой (разложимой относительно скулемовского обогащения), если можно подобрать дизъюнктное разложение обогащённой сигнатуры £* = Е^ Ц ££ , £ П £1 Ф 0 ^ £ П ££ и такие множества формул , Б'2 соответствующих сигнатур ££, которые содержатся в скулемовском обогащении теории 7~: , ¿>2 СТ* и порождают расширение теории Т: , \гТ. Обозначение: 7~= ® 3'2.

Поясним данное определение. Наша цель - определить разложимость исходной теории Т после скулемовского обогащения. Так как Т С 7"*, мы требуем существования в Т* двух множеств формул , Б'2 дизъюнктных сигнатур, из которых следует сама теория Т (другими словами, она содержится в дедуктивном замыкании этих множеств формул).

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

исходной сигнатуры Е:Е1=ЕПЕ^^0^£ПЕ$ = В частности, этим исключается тот случай, когда одна из компонент может совпадать с Д. То есть, случай, когда, может быть, одно из множеств содержит формулы только с символами из Д, а другое - из Е.

Отметим, что если исходная теория Т не содержит 3-формул, т.е. Д = 0 и Т = Т*, мы приходим к изначальному определению разложимой теории, данному в главе 2 диссертации.

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

Предложение 6 Разложимость теории Т равносильна её относительной разложимости.

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

1. Исследовано применение декларативных описаний в логике первого порядка для задач поиска информации и интеграции источников данных. Разработана и реализована программно логическая теория в области биоинформатики для анализа экспериментальных данных по экспрессии генов и фе-нотипическим аномалиям модельного организма АгаЫс1ор81з 1,ЬаНапа (Ь.).

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

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

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

[1] Ponomaryov D. Semantic Web basics in logical consideration. // Lecture Notes in Informatics: Proc. / Informatik-2006, Dresden, 2006 - Bonn, 2006. - Volume 2 - P.337-344.

[2] Пономарев Д.К. Проблема разложимости при формальном описании знаний. - Новосибирск, 2006 - 21 стр. - (Препр. / СО РАН. Ин-т систем информатики; N135).

[3] Ponomaryov D. On decomposability of elementary theories // Algebra and Model Theory - Novosibirsk State Technical University, 2005 - N 5 - P. 162-169.

[4] Ponomaryov D., Omelianchuk N, Kolchanov N., Mjolsness E., Meyerowitz E. Semantically rich ontology of anatomical structure and development for Arabidopsis thaliana (L.). // Proc. Bioinformatics of Genome Regulation and Structure (BGRS'2006), Novosibirsk - 2006 - P. 227-230.

[5] Mironova V.V., Poplavsky A.S., Ponomaryov D.K., Omelianchuk

N.A. Ontology of Arabidopsis Genenet Supplementary Database(AGNS): Cross references to TAIR ontology. // Proc. Bioinformatics of Genome Regulation and Structure (BGRS'2006), Novosibirsk - 2006 - P. 209-212.

[6] Ponomaryov D., Omelianchuk N, Kolchanov N., Mjolsness EM Meyerowitz E. A program method for inferring relationships between phenotypic abnormalities of Arabidopsis. // Proc. Bioinformatics of Genome Regulation and Structure (BGRS'2006), Novosibirsk - 2006 - P. 231-234.

[7] Ponomaryov D. Lattice semantics for incremental data extraction from declarative knowledge bases. - Новосибирск, 2006 - 13 стр. - (Препр. / CO РАН. Ин-т систем информатики; N134).

[8] Пономарев Д.К. Задача разложимости элементарных теорий и проблема минимизации из аксиом. // Тез. конференции-конкурса "Технологии Microsoft в информатике и программировании", Новосибирск, 22-24 февраля, 2006. - С. 213-215.

[9] Пономарев Д.К. Применение языков описания онтологий для построения Web-ориентированных информационных систем. // Вестник Новосибирского Гос. Ун-та / Информационные технологии - Новосибирск, 2004 - Т.1, Вып.2 - С. 5-20.

[10] Пономарев Д.К. Применение Web-стандартов описания метаданных для представления предметных областей. // Тез. XLI Международной Научной Студенческой Конференции (МНСК), Новосибирск, 14-17 апреля 2003. - С. 39-40.

Пономарев Д.К.

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

Автореферат

Подписано в печать Объем 1,1 уч.-изд.л.

Формат бумаги 60x90 1/16 Заказ №<$57" Тираж 100 экз.

Отпечатано на ризографе "AL Group" 630090, г. Новосибирск, пр. акад. Лаврентьева, 6

Введение

Глава 1. Пример разработки прикладных логических теорий

1,1 Постановка задачи.

12 Предназначение разрабоинноп юории.

13 Проблема формальней о иредсшв к'ння.

1,1 Структура теории.

1о Обсуждение предгтавичшой теории. l.G Программная реализация.

1,7 Обзор близких pa6oi.

1 8 Резулыаш

Глава 2, Проблема синтаксической однозначности и разложимости

2 1 Непрерывная шлборка информации . . . . 31 2 2 Посшнонка проб юмы ра5ло/Кимо(л и . . U)

2 3 Пршюшмые теории.

2 1 Разложимые теории . . . "Л

2 5 Резулыаш . . .G

Глава 3. Практические вопросы разложимости GG

3 1 Конечно аксиоматизируемые теории . . G

3 2 Приведение к преднкаым.

3 3 Скудемонское обогащение.

3 1 Ре платы

В настоящее время существуй значительный ишерес к метола'i и средствам декларативного представления знаний, коюрый. в частности, связан с недавно обученной концепцией "Semantic Web" [lj-[l] и широко раснрос1раненным понятием формальной онюлопш [5]-[7j. Рсчулыаюм )юю являек'я разрабош! и применение новых компьютерных языков для формальною представления знаний [G2, G3], а мк-же сисп'М по,1держки логическою вывода. Каждый и з новых языков cooiBeu iB)ei некоюрому иодмножес1ву лотки первою порядка, однако исходя из практики специалисты начгши осознавать необходимость использования данной лотки целиком для работы с теми задачами, коюрые (чали аыуальны в последнее время. Среди них можно выделил» поиск в объемных слабо струмурированных хранилищах информации и пн им рацию кчероюнных источников данных.

В рамках данных задач декларашвные описания применякнся как 1ерминоло1ические базы знаний, в коюрыч описаны 1ермины вмесче с заданной для них аксиомашческой еемашикой. Декларашвные iep-\1Иноло1 ические базы знаний обычно нриняю рассмаipnnaiь с двух ючек зрения: как i рафы свя зносш юрминов и как наборы ло1 ических упзерждении IIjjii лом широко используемся ионяше связи юрминов по вхождению в одно (или близкие в определенной мефике) высказывания.

Связи между 1ерминами в задаче поиска даю1 возможное п> переформулировать (усилить/ослабить) запрос в зависимости oi рез)лыа-Ш13 ею исполнения [8]. Аналошчно лому в задаче imiei рации связи влинкл на точность иоароешюю отображения меж,1у двумя описаниями данных [9, 10J При лом аксиомы, заданные в декдарашвном описании, непосредственно определяют пш связей между терминами [11, 12]. Для решения копире:ной задачи moi^t применяйся различные cipaieimi. использующие разные пшы связей в зависимости от ситуации.

В данной работе декларативные описания знаний расематривают-ся как (элементарные) теории в лошке первого порядка. Естественно, данное рассмотрение не являемся орипшальным и оно не может бып> 1аковым в принципе, начиная с юю времени, как был введен формальный amiapai дошки.

С ючки зрения связей терминов по вхождению для заданной юории можно рассматривать различные компоненты свя зности на множестве cniHaiypubix символов, используемых в записи иредчожешш теории. Есюспзенным образом возникае1 вопрос: являю1ся ли компоненты связносш одинаковыми для двух лошчески эквивалентных leopini 13 одной и юй же cniiiaiype? В целом, ответ является отрицательным и причина лому - сишаксическая cyib нашею подхода. На практике это означает, что могут сущеснзовать два множества предложений, которые семантически эквивалентны, но синтаксически представ юны по-разному. Возможно ли привести теорию (аксиомы теории) к такому виду, по коюро.му однозначно определяю юя комноиешы связнос in сш шнуры юории? Данный вопрос нредставлне! расширенную постановку проблемы разложимое! и, коюрая была сформулирована в 2003 юду в связи с изучением формальных ошолошй (см. исходную формулировку в [13] и поепшовку в главе 1 8). Суп» проблемы заключайся в юм, как определи хь, иредаавима ли произвольная заданная тория в .юшке первою порядка в виде объединения двух (или более) ieopiii'i, имеющих непересекающиеся сшншуры.

Вопрос разложимое:и имее! важное значение для формализации знаний, поскольку разложимосп» означает возможность разбить формальное описание инюресующей нредмепюй облает на част, каждая из коюрых используе1 свой оиельный алфавш. При построении формальною описания некоюрой предмешой облас!П часю оказы-вае1ся, чю данные, полученные oi экснерюв (или, например, извлеченные авюмашчсски из ickciob), иредсчавляю! собой некоюрый набор фактов, которые необходимо структурировать, чтобы получить и i них адекватную формальную модель. В частности, можег бьпь интересно, существуют ли част знания, которые независимы друг oi дру1а Эю в ЮЧНОС1И cooiBeiciB)er вопросу разложимое!и. если рассматривать с})0]).малыю0 онисанио предмешой облапи как ло[ ическую !ео])ию (скажем, в некоюром иодмножечлве лошки первою порядка) [35. 56. 61].

В данной рабою решена проблема разложимости для произвольных элемешарных теорий. Кроме тою, доказана однозначность разло/ко-ния сш ши)ры и самой хеории (с lo'inocibio до формул чисюю равенства) в случае ею существования. Таким образом, настоящая рабоы )С1анавливае1 связь мел\,1у подходом к paccMoipennio сшпаксической связанное!!! 1ермшюв с точки зрения !рафов и с ючки зрения формул Л01 ики.

Цель работы

- исследование возможности декомпозиции (разложения) формальных описаний 15 логике первою порядка на компоненты с непересекающимися алфавшами;

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

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

Методы исследования: меюды лошческою upoi раммирования и дедук питых систем, аппарат математической логики и теории моделей.

Научная новизна

Резулыаш. полученные в рабою, являкнея новыми и cooibcicib\-Ю1 тенденции времени в част связанных с ними информационных задач. В частосш. до насюящей рабохы исследования по решению проблемы разложимости в теории с дизъюнктными сш натурами не вс!речались в публикациях. Не было показано ранее, чю 1Сория в лотке первою порядка определив! компоиешы связносчи cinnaiypbi однозначным образом. Также не была исследована взаимосвязь лих вопросов с современными иосьшовками задач информационною поиска и liniei рации nciочников данных.

Практическая ценность

Полученные резулыаш имечог ценное!ь для задач поиска и ише-I рации данШ)1Х с использованием декларативных баз знаний, декомпозиции логических программ, распределенною исполнения логических операции, таких как проверка на непротиворечивость, над декларашв-ными базами знаний большою обьема. Кроме юю, фак!ы. показанные в работе, представляют интерес в связи с исследованием проб ими рышттпоипи в лотке и философии.

Апробация работы

Резульгаш работы докладывались в рамках следующих научных вс!реч: Iiiformatik-2006 - немецкой конференции по информашке (i Дрезден, Германия), русско-немецком симпозиуме по биоинформашке в 2005 io,iy (i. Билефельд, Германия), семинаре СОМО (i. Дармппадк

Германии, 2005 г.), международной конференции по биоинформатике BGRS'200G (Новосибирск, 200G ь), конференции "Техно.юпш Майкрософт в информатике и иро1раммировании"(Новосибирк, 200G юд). Ме/кдународной Научной Студенческой Конференции в 20031оду (Новосибирск). а также на семинарах в Институте систем информатики СО РАН. Пнсшiyie математики СО РАН, Институте цито юпш и тенет ики СО РАН.

По Юме диссертации опубликовано 10 печатых работ.

Структура и объем работы

Диссертационная работ состоит из введения, треч глав и списка литературы. Объем диссертации - 89 страниц. Список литературы содержит 63 наименования. Работ включает 8 рисунков.

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

1. Исследовано применение декларативных описаний в дотике нерво-ю порядка для задач поиска информации и интсчрации исючников данных Разработана и реализована протраммно лотическая теория в области биоипформашки для анализа экспериментальных данных по экспрессии генов и фенотипическим аномалиям модельното организма Arabidopsis thaliana (L.).

2. В связи с использованием связей терминов в декларативных описаниях исследована возможность декомпозиции (разложения) формальных описаний тз .юшке первою порядка на компоненты с непересекающимися алфавитами. Сформулирован критерий разложимости.

3. Исследован вопрос синтаксической однозначности при описании знаний как ieopiiii в .км ике первою порядка. Доказана однозначное it, ра з-ложения геории на неразложимые компоненты с точностью до формул чистою равенства. Показано приведение теории к такому виду, по которому однозначно определяется ее разложение.

Заключение

В рамках соЕзременныч тенденций использования декларативных баз знаний для задач поиска и иннчрации информации автором в данной работе исследована проблема разложимоеiи (иементарных) кюрий дошки первою порядка.

Свойство разложимости cooiBeiciByei юму, чю исходную leopnio можно предемвить в виде обьединения двух (или более) теории. имеющих н(Ч1ересекаюшиеся сш натуры.

В облает формализации знаний вопрос разложимое!и интересен с ир<1ктической точки зрения, поскольку разложимость означаем возможность разбип» (формальное описание интересующей предметной облает на част, каждая из коюрых используем свой оiдельный ;u-(})авш. При носIроении формальною описания некоюрой предмешой облает часю оказываемся, чю данные, полученные oi жеперюв (или извлеченные авюмашчески), И1)едс1авляюг собой некоюрый набор факюв, которые необходимо с-1рукiурироиа 1 ь, чюбы получить из них адеквашую c|)op\uun>nyio модель. В часшосш, можем бы и, шперее-но. сущее 1вукн ли час ш знания, коюрые независимы др>ч oi друта Эю в ючносш cooiBeiciByei вопросу разложимоеш, если рассматривай, формальное описание предмешой облает как лотческио ieo-рию (скажем, в некотором фратмеше лотки первою порядка). Разложимосп, важна и для выполнения лснических операций над обьем-ными декларашвными базами знаний, в часшосш, для проверки их непротиворечивое ш. Если теория может бып, разбита в неско п,ко ча-cieii. имеющие различные сш шпуры, ю )ш част возможно подвер1nyib проверке на непро1иворечивое1ь по отдельности. Эю также дает возможность распределенною выполнения данной операции. Можно привести и дручие П1)имеры приложении данного вопроса. Пдеолош-чески все они исходяi из юю просюю факта, чю в любой сфере 'знаний декомпозиция всегда означает упрощение.

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

В настоящее время в ряде информационных задач, связанных с тер-минолоптческими базами знаний, широко используется понятие связи терминов но вхождению в одно (или близкие с определенной метрикой) высказывания. Декларативные 1ерминоло1 ические базы знаний обычно принято рассматривать с двух точек зрения: как 1рафы связности терминов и как наборы лотических утверждений. В связи с этим в работе рассмотрена проблема синтаксической однозначности при описании знаний в ло1 икс первою порядка Однозначность является важной. поскольку в ло1 неэквивалентные утверждения мотут различаться сшпаксически. В общем случае два (семантически) эквивалентных описания Moiyr отвечать разным компонентам связности терминов, что делает на первый взгляд невозможным использование связности по вхождению в высказывания. Автором в данной работе доказано, чю разложение теории на неразложимые компоненты веема однозначно Однозначность разложения соответствует однозначности в синтаксической записи утверждений с точки зрения вхождения сигнатурных элементов. Кроме тою, показано приведение теории к такому втщу. по которому однозначно определяется это разложение. Таким образом, настоящая работа устанавливает связь между подходом к рассмотрению связности юрминов с точки зрения 1рафов и с точки зрения формул л 01 и к тт.

1. Вегпогь-Lce Т., Hendler J., Lassila О. 'Ihe Semantic Web. // Scientific American, Maj, 2001.

2. G. Jasper R., Uschold М. A framework for understanding and classify mg ontolog\ applications // Proc IJCAI99 Workshop on Ontologies and Problem-Solving Methocls(KRRo), Stockholm, Sweden, August 1999

3. Guarino N. Гопиа! Ontologj and Information Sj stems Proc TOIS 9S. Trento, Italv, June. 199S P 3-13

4. Stuckenschmidt H., Giunchiglia F., van Ilarmelen F. Querj processing in ontolog\-based peer-to-peer Ь) stems // Ontologies for Agents Iheon and Experience-) Birkhauser, 2003.

5. Ralini E., Bernstein P. A sur\e> of approaches to automatic schema matching // 1 he YLDB Journal 2001 - \ 10(1).

6. Melnik S., Molina-Garcia H., Rahm E. Similarity flooding. A versatile graph matching <iIqorithm and its application to schema matching. // Proc International Conference on Data engineering (ICDE) 2002.

7. Maedche A., Staab S. Measuring similarity between ontologies // Proc EK WV'2002 P. 251-263.

8. Eu/enat J., Valtchev P. An integrative proximity measure for ontology alignment // Proc. ISWC-2003

9. Palchunov D. GABEK for Ontology Generation // GABEK Contributions to Knowledge Organization Wien LIT-pubhshing Company, 2003 - Vol. 2.

10. The Computable Plant project http //www computableplant org]

11. Omelianchuk N.A. et al. AGNS A database on expression of Arabulopsis genes // Bioinformaticb of Genome Regulation and Structure. I'roc. / BGRS'2001. .Novosibirsk, 2001 - Berlin, 200G - Volume 2 - P. 433-112

12. Karp P.D. An ontology for biological function based on molecular interactions // Bioinformatics 2000. X 16 P 260-285.17| Barcl J.В., Rliee S.Y. Ontologies in biology, design, applications and future challenges // Nat. Rev. Genet 2001. -No- P. 213-222

13. Bodenreider O. et al. Biomedical ontologies // Proc. Pacific Symposium on Bioconiputing 2003 - P. 76-78

14. McGuinness D. L., van Harmelen F. OWL Web Ontology Language Oyerview. // W3C Recommendation, <http://www.w3org/FR/owI-features

15. Patel-Schneider P.F., Hayes P., Ilorrocks I. OWL Web Ontology Language: Semantics and Abstract Syntax // W3C Recommendation chttp.//wvvvv.w3 org/1 R/owl-seniantics/>

16. Bander F., Calavnnese D., McGuiness D., Nardi D., Patel-Schneider P.1.e Description Logic Handbook Cambridge Universitv Pre^s, 2003

17. Клещев А.С., Артемьева И.Л. Математические моими онююшй иред-мегныч обллсюй. Член, II. Компоненты молели. // Научно-и'чническая информация 2001 - X 3 - С. 19-28

18. Клещев А.С., Артемьева И.Л. Необоыщенные системы лен ичеекпч соотношений // Научно-техническая информация 2000 - X 7 - 8 - .V" 7 С 18-28, .V» 8 С. 8-18

19. Garland F.M., McIIale N.A. LOP1. a gene involved ш аччш transport and vascular patterning ш Arabidopsis // Development. 1990 - X 122(G) - P 1S11-1819

20. Hermann G.T., Rosenberg G. Developmental Systems and language-. Amsterdam: Xorth-IIolIand Publishing Co , 19752(5. Лидл P., Ппльц Г. Примадная абстрактная плибра. Пер с англ. / Пот рел ЛИ Шенрина Ккатеринбур1. 1Ьд-ио Урал \н-та, 1996 г

21. Rosen R. Some further comments oil the DXA-protem coding problem. Bull Math Bioph\s 1959 - X 21 - P 289-297.

22. Rosen R. Foundations of Mathematical Biologv. Xev, York, Academic Press, 1972, 1973 - Vol. Mil

23. K. Krohn, R. Langer, J. Rhodes. Algebraic principle-, for the anah-ь of a biochemical ьу stem // I Comput. Syst. Sci -1976 Xl-P 119-136

24. TAIR Ihe Arabulopsis Information Resource, http //www arabidop-as org]

25. РОС Plant Ontology Consortium http.//\\\v\v.plantontolog\ org]

26. Vincent P. et al The Plant Ontology Consortium and plant ontologies Comparative and functional genomics. 2002 - X 3(2) - P 137-112.

27. Jaiswal P. et al. Plant ontology (PO): a controlled vocabulary of plant structures and growth stages // Comparative and functional genomics. 2006 - X 6(7-8) -P 388-397.

28. Aitken S. Formalizing concepts of species, ье\ and development stage ш cinatomical ontologies 11 Bioinformatics 2005 - N 21 - P. 2773-2779.

29. Smith D. et al. On the application of formal principle-, to life science data, a case stud} in the gene ontologv // Database Integration in the Life Sceienc.es -Springer Yerlag, 2004 P. 79-91

30. Smith B. et al. Relations in biomedical ontologies // Genome Hiologv 200") - X G chttp //genomebiologv com/2005/6/5/R 1G>

31. Smith 13. Mereotopologv • Л tlieorj of parts and boundaries // Data and Know ledge Engineering 199G - X 20 - P. 287-303

32. Fu G., Jones C., Abdelmoty A. Ontology-based bpatial querv expansion m information retrieval // Proc OTM Conferences 200") Vol 2

33. Muller H., Kenny E., Sternberg P. Textpresso. An ontologv-based information retrieval and extraction system for biological literature / PI.oS Biologv Journal- 2001 -X 2(11).

34. Chang K.-C., Garcia-Molina II. Approximate query mapping' Ac counting for translation closeness //1he VLDB Journal 2001 - X 10 - P. 155-181.

35. Castnno S., Ferrara A., Montanelli S., Pngani E., Rossi G. Ontologv-addre^sable contents in P2P networks. // Proc. 1st Workshop on Semantics in Peer-to-Peer and Grid Computing 2003.

36. Arumugam M., Sheth A., Arpinar I.B. Towards peer-to-peer semantic web. A distributed environment for sharing semantic knowledge on the web // Proc International World Wide Web Conference 2002 (WWW2002), Honolulu, Hawaii. USA, 2002.

37. Castano S., Ferrara A. Knowledge representation and transformation m ontologv-Ьач>(1 data integration. // Proc. ПС У Workshop oil Knowlidge Transformation for the Semantic Web, Lyon, Trance, July 2002 P 51-59

38. Madliavan J., Bernstein P.A., Domingos P., Halevy A.Y. Representing and reasoning about mappings between domain models // Proc. Eighteenth National Conference on Artificial Intelligence (АААГ2002), Edmonton, Canada- 2002 P. 80-8G.

39. Maedche A., Motik В., Stojanovic L. Managing multiple and distributed ontologies on the Semantic Web // The VLDB Journal 2003 - \ 12 - P. 2SG-302

40. Calvanasea D., De Giacomo G., Lenzerini M. Description logics for information integration / / Computational Logic: I ogic Programming and Beyond- Springer Yerlag, 2001 P. 11-60

41. Bergamabchi S., Cabtano S., Vincini M. Sem.intic integration of seini-structurcd and structured data sources // SIGMOD Records 1999 - X 28(1)

42. Кейслер Г, Чэн Ч.Ч. Ieopnn мошлеи \1.: Мир, 1977.

43. Otto М. An interpolation theorem // Bulletin of Svmbohc Logic 2000 X G.

44. Пальчунов Д.Е. Алгебраическое описании смысла высказываний естесюен-uoio языка // Впчислше и.иые системы / Модели коишпшиыч проще с on -Новосибирск, 1997 Нып 158 - С. 127-118.

45. Пальчунов Д.Е. Синтаксическая бниосгь пред ю/кеиий языка первою порядка // Вычислительные системы / Измерение и модели копштивиых процессов Новосибирск, 1998 - Bun 1G2 - С. 58-80

46. Шёнфплд Дж. Манпшическан лошка М.: Наука, 1975.

47. ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

48. Ponomaryov D. Semantic Web Ьаысъ ш logical consideration. // Lecture Note-, ш Informatics- Proc / Inforinatik-2()0G, Dresden, 200G Bonn, 2000 - Volume 2 - P 337-311

49. Mironova V.V., Poplavbky A.S., Ponomaryov D.K., Omelianchuk

50. N.A. Ontolog} of Arabidopsis Genenet Supplemental Database(AGNS) Cro-s references to TAIR ontologv. // Proc. Bioinformatics of Genome Regulation and Structure (BGRS'2006), Novosibirsk 2000 - P 209-212.

51. GO. Ponomarjov D. Lattice semantics for incremental data e\traction from declarative knowledge bases. Новосибирск, 200G - 13 cip. - (Ilpenp CO РАН Ин-тспси'м информашки; N131).

52. Пономарев Д.К. Залача разложимой» э ie\ieniapnn\ теорий и проб leva мшшмимшш in аксиом. // 1см коиферсниии-конмрса "Течпо ioi ии

53. Microsoft u информатике и профаммироваиии", Новосибирск, 22-21 феир.ин, 2006. С. 213-215

54. Пономарев Д.К. Применение языков описании оитодопш дщ построении \\е1)-ориен1нропанны\ информационных систем. // Вестник Новосибирскою Гос Ун-та / Информационные темютопш Новосибирск, 2001 - Г 1, Впи 1 - С. 5-20.

55. Пономарев Д.К. Применение Web-стандарго» описания метаданных д 1я представ п'нии предметных областей. // Tes. XLI Междуиароmoil ILi\мноп Студенческой Конференции (МНСК), Новосибирск, 11-17 апреля 2003 С 39-Ю.