Дескрипционная логика

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

Описательные ло́гики[1] или дескрипцио́нные ло́гики[2][источник не указан 1330 дней](сокр. ДЛ, англ. description logics, иногда используется неточный перевод: дескрипти́вные логики) — семейство языков представления знаний, позволяющих описывать понятия предметной области в недвусмысленном, формализованном виде. Они сочетают в себе, с одной стороны, богатые выразительные возможности, а с другой — хорошие вычислительные свойства, такие как разрешимость и относительно невысокая вычислительная сложность основных логических проблем, что делает возможным их применение на практике. Таким образом, ДЛ представляют собой компромисс между выразительностью и разрешимостью. ДЛ можно рассматривать как разрешимые фрагменты логики предикатов, синтаксически же они близки к модальным логикам.

Свое современное название ДЛ получили в 1980-х. Прежние названия (в хронологическом порядке): терминологические системы, логики концептов. Изначально ДЛ зародились как расширение фреймовых структур и семантических сетей механизмами формальной логики. В настоящее время ДЛ являются важным в концепции Семантической паутины, где их предполагается использовать при построении онтологий. Фрагменты OWL-DL и OWL-Lite языка веб-онтологий OWL также основаны на ДЛ.

Общие сведения[править | править исходный текст]

Дескрипционные логики оперируют понятиями конце́пт и роль, соответствующими в других разделах математической логики понятиям «одноместный предикат» (или множество, класс) и «двуместный предикат» (или бинарное отношение). Интуитивно, концепты используются для описания классов некоторых объектов, например, «Люди», «Женщины», «Машины». Роли используются для описания двуместных отношений между объектами, например, на множестве людей имеется двуместное отношение «X есть_родитель_для Y», а между людьми и машинами имеется двуместное отношение «X имеет_в_собственности Y», где в качестве X и Y можно подставлять произвольные предметы. С помощью языка ДЛ можно формулировать утверждения общего вида — о классах вообще (всякая Женщина есть Человек, всякая Машина имеется_в_собственности не более чем у одного Человека) и частного вида — о конкретных объектах (Мария есть Женщина, Иван имеет_в_собственности Машину1).

На жаргоне ДЛ набор утверждений общего вида или терминоголии (англ. terminology) называется TBox, набор утверждений (англ. assertions) частного вида — ABox, а вместе они составляют так называемую базу знаний[3] или онтологию. Многочисленные онтологии построены и строятся в самых различных предметных областях, таких как биоинформатика, генетика, медицина, химия, биология. Как только онтология построена, встает вопрос о том, как можно извлекать знания, следующие из содержащихся в онтологии знаний, можно ли это делать программно и каковы соответствующие алгоритмы. Все эти вопросы решаются теоретически в науке «дескрипционная логика», а практически уже реализовано множество программных систем — механизмов рассуждений (англ. reasoners), которые и позволяют автоматизированно выводить знания из онтологий и производить другие операции с онтологиями.

Синтаксис[править | править исходный текст]

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

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

Типичными конструкторами для построения составных концептов являются:

  • пересечение (или конъюнкция) концептов, обозначается как C\sqcap D;
  • объединение (или дизъюнкция) концептов, обозначается как C\sqcup D;
  • дополнение (или отрицание) концепта, обозначается как \neg C;
  • ограничение на значения роли (или ограничение квантором всеобщности), обозначается как \forall R.C;
  • экзистенциальное ограничение (или ограничение квантором существования), обозначается как \exists R.C;
  • численные ограничения на значения роли, например: ({\le}n\,R), ({\ge}n\,R.C), и другие.

Как видим, в ДЛ конъюнкция и дизъюнкция обозначаются иначе, чтобы подчеркнуть отличие от других видов логик. Существуют дескрипционные логики, в которых имеются также составные роли, строящиеся из простых ролей с помощью операций: инверсии, пересечения, объединения, дополнения, композиции ролей, транзитивного замыкания и других.[4]

Синтаксис логики ALC[править | править исходный текст]

Дескрипционная логика \mathcal{ALC} (от Attributive Language with Complement) была введена в 1991 году[5] и является одной из базовых ДЛ, на основе которой строятся многие другие ДЛ. Пусть заданы непустые конечные множества атомарных концептов и атомарных ролей. Тогда следующее является индуктивным определением составных концептов логики \mathcal{ALC} (для краткости в этом определении будем называть их просто концептами):

  • всякий атомарный концепт является концептом;
  • выражения \top и \bot являются концептами;
  • если C\, есть концепт, то его дополнение \neg C является концептом;
  • если C\, и D\, есть концепты, то их пересечение C\sqcap D и объединение C\sqcup D являются концептами;
  • если C\, есть концепт, а R\, есть роль, то выражения \forall R.C и \exists R.C являются концептами.

Примечание. Строго говоря, \mathcal{ALC} — это не одна логика, а семейство логик, где каждая логика этого семейства задается выбором конкретных множеств атомарных концептов и ролей. Это аналогично заданию сигнатуры теории первого порядка. Однако, этим различием обычно пренебрегают, что мы и будем делать в дальнейшем.

Семантика[править | править исходный текст]

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

Формально, интерпретация \mathcal{I} состоит из непустого множества \Delta^\mathcal{I} (домена) и интерпретирующей функции, которая сопоставляет каждому атомарному концепту A\, некоторое подмножество {A^\mathcal{I}\subseteq\Delta^\mathcal{I}}, а каждой атомарной роли R\, — некоторое подмножество {R^\mathcal{I}\subseteq\Delta^\mathcal{I}\times\Delta^\mathcal{I}}. Если пара индивидов принадлежит интерпретации некоторой роли R\,, то есть (e,d)\in R^\mathcal{I}, то говорят, что индивид d\, является \,R-последователем индивида \,e.

Далее интерпретирующая функция распространяется на составные концепты и роли. Поскольку последние в каждой ДЛ свои, то в качестве примера рассмотрим семантику для описанной выше логики \mathcal{ALC}.

Семантика логики ALC[править | править исходный текст]

Интерпретирующая функция распространяется на составные концепты логики \mathcal{ALC} по следующим правилам:

  • \top интерпретируется как весь домен: \top^\mathcal{I}=\Delta^\mathcal{I}
  • \bot интерпретируется как пустое множество: \bot^\mathcal{I}=\varnothing
  • дополнение концепта интерпретируется как дополнение множества: (\neg C)^\mathcal{I}=\Delta^\mathcal{I}\setminus C^\mathcal{I}
  • пересечение концептов интерпретируется как пересечение множеств: (C\sqcap D)^\mathcal{I}=C^\mathcal{I}\cap D^\mathcal{I}
  • объединение концептов интерпретируется как объединение множеств: (C\sqcup D)^\mathcal{I}=C^\mathcal{I}\cup D^\mathcal{I}
  • выражение \forall R.C интерпретируется как множество тех индивидов, у которых все \,R-последователи принадлежат интерпретации концепта \,C. Формально:
(\forall R.C)^\mathcal{I} = \{\,e\in\Delta^\mathcal{I} \mid \forall d\in\Delta^\mathcal{I}:\  (e,d)\in R^\mathcal{I} \Rightarrow d\in C^\mathcal{I} \,\}
  • выражение \exists R.C интерпретируется как множество тех индивидов, у которых имеется \,R-последователь, принадлежащий интерпретации концепта \,C. Формально:
(\exists R.C)^\mathcal{I} = \{\,e\in\Delta^\mathcal{I} \mid \exists d\in\Delta^\mathcal{I}: (e,d)\in R^\mathcal{I} \land d\in C^\mathcal{I} \,\}

Пример. Пусть домен интерпретации \Delta^\mathcal{I} состоит из всех людей, атомарный концепт \,M интерпретирован как множество людей мужского пола, а роль \,R как отношение «есть родитель для». Тогда концепт \forall R.M будет интерпретирован как множество людей, у которых все дети мужского пола, а концепт M\sqcap\exists R.\top — как множество «отцов», то есть людей мужского пола, имеющих хотя бы одного ребенка.

Связь с модальной логикой[править | править исходный текст]

На первый взгляд синтаксис ДЛ является непривычным для тех, кто знаком с «традиционными» логиками (логикой высказываний, логикой предикатов, модальной логикой и др.). Однако уже в 1991 году[6] было замечено, что ДЛ \mathcal{ALC} есть не что иное, как записанная в других обозначениях модальная логика \mathbf{K}_n, имеющая \,n независимых модальностей. А именно, если в \mathcal{ALC} имеются атомарные концепты A_1,\ldots,A_m и атомарные роли R_1,\ldots,R_n, то соответствие между логиками осуществляется следующим образом:

  • атомарные концепты A_i\, переходят в пропозициональные переменные p_i\, модальной логики;
  • пересечение \sqcap, объединение \sqcup и дополнение \neg концептов переходит в булевы связки конъюнкцию \land, дизъюнкцию \lor и отрицание \neg;
  • выражение \forall R_j переходит в \Box_j, а выражение \exists R_j переходит в \Diamond_j.

Например, концепт \exists R_1.(A_1\sqcup\forall R_2.\neg A_2) переходит в модальную формулу \Diamond_1(p_1\lor\Box_2p_2). При таком преобразовании всякий составной концепт логики \mathcal{ALC} превращается в правильно построенную формулу модальной логики \mathbf{K}_n, причем всякая модальная формула является переводом некоторого концепта (тем самым, это один и тот же язык, только записанный в двух разных системах обозначений). Более того, данное преобразование согласуется с вышеописанной семантикой логики \mathcal{ALC} с одной стороны и семантикой Крипке модальной логики с другой.

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

Связь с логикой предикатов[править | править исходный текст]

Многие ДЛ, включая \mathcal{ALC}, можно рассматривать как фрагменты логики предикатов при «естественном» переводе концептов в предикатные формулы. Если в \mathcal{ALC} имеются атомарные концепты A_1,\ldots,A_m и атомарные роли R_1,\ldots,R_n, то для перевода вводятся одноместные предикатные символы P_1,\ldots,P_m и двуместные предикатные символы S_1,\ldots,S_n, а сам перевод задается индуктивно следующим образом:

  • атомарные концепты A_i\, переходят в формулы \,P_i(x);
  • пересечение \sqcap, объединение \sqcup и дополнение \neg концептов переходит в булевы связки конъюнкцию \land, дизъюнкцию \lor и отрицание \neg;
  • выражение \forall R_j.C переходит в \forall y (S_j(x,y)\Rightarrow C'(y));
  • выражение \exists R_j.C переходит в \exists y (S_j(x,y)\land C'(y)).

В последних двух пунктах переменная \,y — свежая (не встречавшаяся ранее), а \,C' есть перевод концепта \,C (который уже построен по предположению индукции).

Легко видеть, что данный перевод согласуется с описанной выше семантикой ДЛ, то есть в любой интерпретации, если атомарные концепты A_i\, и атомарные роли R_j\, интерпретированы так же, как соответствующие им предикаты P_i\, и \,S_j, то и всякий составной концепт интерпретируется тем же самым множеством, что и соответствующая ему при переводе предикатная формула от одной переменной. Следует также отметить, что не всякая формула логики предикатов является переводом какого-либо концепта; например, формула \forall x P_1(x) не является таковой.

В данном переводе можно обойтись всего двумя переменными,[7] и таким образом ДЛ \mathcal{ALC} (а также многие ее расширения) можно рассматривать как фрагменты логики предикатов с двумя переменными, которая, как известно, разрешима.[8] Данный перевод позволяет переносить результаты о разрешимости, вычислительной сложности, разрешающих алгоритмах и т. п. из области логики предикатов в область дескрипционных логик.

База знаний[править | править исходный текст]

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

В соответствии с этим делением, записываемые с помощью языка ДЛ знания подразделяются на

  • набор терминологических аксиом или TBox \mathcal{T} и
  • набор утверждений об индивидах или ABox \mathcal{A}.

Совокупность аксиом и утверждений вместе составляют так называемую базу знаний \mathcal{K}=\mathcal{T}\cup\mathcal{A}. Далее мы по отдельности рассмотрим виды аксиом и утверждений, из которых может состоять TBox и ABox.

Аксиомы и TBox[править | править исходный текст]

Аксиомой вложенности концептов называется выражение вида C\sqsubseteq D, а аксиомой эквивалентности концептов — выражение вида C\equiv D, где \,C и \,D — произвольные концепты. Аналогично, аксиомой вложенности ролей называется выражение вида R\sqsubseteq S, а аксиомой эквивалентности ролей — выражение вида R\equiv S, где \,R и \,S — произвольные роли. Здесь \sqsubseteq есть символ вложенности (subsumption).

Терминологией или набором терминологических аксиом или TBox (от англ. terminological box) называется конечный набор аксиом перечисленных видов. Иногда аксиомы для ролей выделяются в отдельный набор и называют его иерархией ролей или RBox. Помимо перечисленных видов аксиом, в терминологии могут допускаться и другие аксиомы (например, транзитивность ролей); о них пойдет речь ниже.

Семантика терминологии определяется естественным образом. Пусть дана интерпретация \mathcal{I}. Аксиома C\sqsubseteq D выполняется в интерпретации \mathcal{I}, если C^\mathcal{I}\subseteq D^\mathcal{I}; в этом случае также говорят, что \mathcal{I} является моделью аксиомы C\sqsubseteq D. Аналогично для остальных видов аксиом. Терминология \mathcal{T} выполняется в интерпретации \mathcal{I}, а интерпретация \mathcal{I} называется моделью терминологии \mathcal{T}, если \mathcal{I} является моделью всех входящих в \mathcal{T} аксиом.

Пример. Следующая совокупность является терминологией (или TBox) в языке логики \mathcal{ALC}:

\mathsf{Woman}\equiv\mathsf{Person}\sqcap\mathsf{Female}
\mathsf{Mother}\equiv\mathsf{Woman}\sqcap\exists\mathsf{hasChild}.\top
\mathsf{Person}\sqsubseteq\forall\mathsf{hasChild}.\mathsf{Person}
\mathsf{Doctor}\sqsubseteq\mathsf{Person}

Интуитивно (то есть при «естественной» интерпретации, когда концепту \mathsf{Person} соответствует множество всех людей, роли \mathsf{hasChild} соответствует отношение «имеет_ребенка» и т. д.) эти аксиомы говорят, что быть женщиной означает в точности быть человеком и быть женского пола; быть матерью означает в точности быть женщиной и иметь ребенка; у всякого человека всякий ребенок есть тоже человек; всякий доктор является человеком. Первые две аксиомы вместе представляют собой пример так называемой ациклической терминологии.

Утверждения и ABox[править | править исходный текст]

Терминологии позволяют записывать общие знания о концептах и ролях. Однако помимо этого обычно требуется также записать знания о конкретных индивидах: к какому классу (концепту) они принадлежат, какими отношениями (ролями) они связаны друг с другом. Это делается в той части базы знаний ДЛ, которая называется ABox (или набор утверждений об индивидах).

С этой целью, помимо атомарных концептов и атомарных ролей, то есть имен для классов и отношений, вводится также конечное множество имён для индивидов. Утверждения об индивидах бывают двух видов:

  • утверждение о принадлежности индивида \,a концепту \,C — записывается как \,C(a) или \,a\colon C;
  • утверждение о связи двух индивидов \,a и \,b ролью \,R — записывается как \,R(a,b) или \,(a,b)\colon R или a\,R\,b.

Наконец, набором утверждений об индивидах или ABox (от англ. assertional box) называется конечный набор утверждений этих двух видов.

Примечание. В некоторых ДЛ допускаются также утверждения вида \neg R(a,b) в ABox.

Чтобы задать семантику ABox, необходимо расширить интерпретацию \mathcal{I}, а именно каждому имени индивида \,a сопоставить некоторый элемент домена a^\mathcal{I}\in\Delta^\mathcal{I}. Тогда говорят, что утверждение \,C(a) или \,R(a,b) выполняются в интерпретации \mathcal{I}, если имеет место a^\mathcal{I}\in C^\mathcal{I} или (a^\mathcal{I},b^\mathcal{I})\in R^\mathcal{I}, соответственно. Говорят, что ABox выполняется в интерпретации \mathcal{I}, а интерпретация \mathcal{I} является моделью данного ABox, если все его утверждения выполняются в этой интерпретации.

Пример. Следующая совокупность является набором утверждений об индивидах (или ABox) в языке логики \mathcal{ALC}:

\mathsf{Mary}\colon\mathsf{Woman}\sqcap\neg\mathsf{Doctor}
\mathsf{Mary}\colon\exists\mathsf{hasChild}.\mathsf{Female}
\mathsf{Mary}\,\mathsf{hasChild}\,\mathsf{Peter}
\mathsf{Peter}\colon\mathsf{Doctor}\sqcap\forall\mathsf{hasChild}.\bot

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

Примечание. Часто рассматриваются лишь интерпретации, которые удовлетворяют соглашению об уникальности имён (unique name assumption). Оно означает, что разным именам индивидов интерпретация обязана сопоставлять различные элементы домена. Язык OWL по умолчанию не предполагает данное соглашение, однако в нем есть конструкции, с помощью которых можно явно указать, какие имена индивидов считать равным либо различными.

Отличие от баз данных[править | править исходный текст]

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

Выразительные ДЛ[править | править исходный текст]

Существуют многочисленные расширения логики \mathcal{ALC} дополнительными конструкторами для построения концептов, ролей, а также дополнительными видами аксиом в TBox. Имеется неформальное соглашение об именовании получающихся при этом логик — обычно путем добавления к имени логики букв, отвечающих добавленным в язык конструкторам. Наиболее известными расширениями являются:[4]

\mathcal{F} Функциональность ролей: концепты вида ({\le}1\,R), означающие: существует не более одного \,R-последователя
\mathcal{N} Ограничения кардинальности ролей: концепты вида ({\le}n\,R), означающие: существует не более \,n \,R-последователей
\mathcal{Q} Качественные ограничения кардинальности ролей: концепты вида ({\le}n\,R.C), означающие: существует не более \,n \,R-последователей в \,C
\mathcal{I} Обратные роли: если \,R есть роль, то \,R^{-} тоже является ролью, означающей обращение бинарного отношения
\mathcal{O} Номиналы: если \,a есть имя индивида, то \,\{a\} есть концепт, означающий одноэлементное множество
\mathcal{H} Иерархия ролей: в TBox допускаются аксиомы вложенности ролей R\sqsubseteq S
\mathcal{S} Транзитивные роли: в TBox допускаются аксиомы транзитивности вида \mathsf{Tr}(R)
\mathcal{R} Составные аксиомы вложенности ролей в TBox (R\circ S\sqsubseteq R, R\circ S\sqsubseteq S) с условием ацикличности, где R\circ S есть композиция ролей
(D)\,   Расширение языка конкретными доменами (типами данных)

Например, логика \mathcal{ALC}, расширенная инверсными ролями, номиналами и ограничениями кардинальности ролей, обозначается как \mathcal{ALCIOQ}.

Примечание. Буква \mathcal{S} не добавляется к имени логики, а замещает в нем буквы \mathcal{ALC}. Так, например, логика \mathcal{ALC}, расширенная инверсными ролями (буква \mathcal{I}), качественными ограничениями кардинальности ролей (буква \mathcal{Q}), транзитивными ролями (буква \mathcal{S}) и иерархией ролей (буква \mathcal{H}), имеет название \mathcal{SHIQ}. Происхождение всех букв понятно из английских названий конструкторов; буква \mathcal{S} же была выбрана из-за тесной связи получающейся ДЛ с модальной логикой \,\mathbf{S4}[6] (хотя в последней буква S означает просто system, саму же логику \,\mathbf{S4} выделяет среди других модальных логик именно цифра 4).

Примечание. Если в ДЛ присутствуют одновременно буквы \mathcal{S}, \mathcal{H} и либо \mathcal{Q} либо \mathcal{N}, то дополнительное ограничение налагается на правило построения концептов: в концептах вида ({\le}n\,R.C) нельзя использовать роли \,R, имеющие (с точки зрения аксиом RBox) транзитивные под-роли. Если не налагать данные ограничения, то логика становится неразрешимой.[9]

Рассматриваются также ДЛ, в которых можно строить составные роли с помощью операций объединения, пересечения, дополнения, инверсии, композиции, транзитивного замыкания и других. Кроме того, исследованы ДЛ, в которых имеются многоместные роли (обозначающие n-арные отношения).[4]

Логический анализ[править | править исходный текст]

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

Пусть мы фиксировали некоторую ДЛ. Введем несколько важных понятий.

  • Говорят, что концепт \,C данной логики выполняется в интерпретации \mathcal{I}, если C^\mathcal{I}\ne\varnothing.
  • Концепт \,C называется выполнимым, если существует интерпретация, в которой он выполняется.
  • Концепт \,C вложен в концепт \,D (или содержится в нем; англ. «is subsumed by»), если в любой интерпретации \mathcal{I} выполняется C^\mathcal{I}\subseteq D^\mathcal{I}.

Аналогичные понятия можно ввести относительно некоторого заданного TBox \mathcal{T}, ограничиваясь моделями данного TBox. Например, концепт \,C называется выполнимым относительно TBox \mathcal{T}, если существует интерпретация, являющаяся моделью этого TBox, в которой данный концепт выполняется.

Когда задан не только TBox \mathcal{T}, но и ABox \mathcal{A}, а значит имеется база знаний \mathcal{K}=\mathcal{T}\cup\mathcal{A}, то возникает еще одно понятие.

  • Индивид \,a является экземпляром концепта \,C относительно базы знаний \mathcal{K}, если в любой модели \mathcal{I} базы знаний \mathcal{K} имеет место a^\mathcal{I}\in C^\mathcal{I}.

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

  • Выполнимость концепта: является ли заданный концепт выполнимым относительно заданного TBox?
  • Вложенность концептов: верно ли, что один заданный концепт вложен в другой относительно заданного TBox?
  • Совместимость TBox: имеет ли заданный TBox хотя бы одну модель?
  • Совместимость базы знаний: имеет ли заданная пара (TBox, ABox) хотя бы одну модель?

В логиках, содержащих \mathcal{ALC}, проблема вложенности концептов сводится к выполнимости концепта.[4] Важное практическое значение имеют нестандартные алгоритмические проблемы, в частности:

  • Классификация терминологии: для данной терминологии (то есть TBox) построить таксономию или иерархию концептов, то есть упорядочить все атомарные концепты по отношению вложения (отн. данного TBox) и выдать соответствующее частично упорядоченное множество.
  • Извлечение экземпляров концепта: найти все экземпляры заданного концепта относительно заданной базы знаний.
  • Наиболее узкий концепт для индивида: найти наименьший (по вложению) концепт, экземпляром которого является заданный индивид относительно заданной базы знаний.
  • Ответ на запрос к базе знаний: выдать все наборы индивидов, которые удовлетворяют заданному запросу относительно заданной базы знаний. В настоящее время глубоко изучены так называемые конъюнктивные запросы к базам знаний ДЛ (а также их дизъюнкции), которые похожи на аналогичные запросы из области баз данных. В случае же запросов более общего вида проблема быстро приобретает высокую вычислительную сложность или даже становится неразрешимой.[10][11]

Свойства ДЛ[править | править исходный текст]

Фундаментальными характеристиками той или иной ДЛ являются следующие:

  • Разрешимость: обычно рассматривают разрешимость проблем выполнимости концепта (относительно TBox), совместимости базы знаний, ответа на конъюнктивные запросы.
  • Вычислительная сложность: изучается вычислительная сложность указанных выше алгоритмических проблем относительно размера входных данных (концепта, TBox, ABox). Отдельно выделяют сложность проблемы выполнимости концепта при фиксированном TBox, сложность проблемы выполнимости базы знаний или проблемы ответа на запросы при фиксированном TBox и меняющемся ABox (так называемая сложность по данным, англ. data complexity).
  • Свойство конечности моделей, или иначе полнота относительно конечных моделей (finite model property): исследуется вопрос, всегда ли верно, что если концепт выполним (относительно TBox), то он выполним и на некоторой конечной модели (данного TBox). Из наличия данного свойства у конкретной ДЛ обычно следует, что для данной ДЛ более просто строится разрешающая процедура, например, табло-алгоритм.
  • Свойство древовидности моделей, или иначе полнота относительно древовидных моделей (tree model property): аналогичный вопрос, но не о конечных, а о «древовидных» моделях. При этом древовидными здесь могут считаться структуры, слегка отличающиеся от традиционного понятия дерева; например, могут допускаться петли (ребра, ведущие из вершины в эту же вершину), мультирёбра (несколько ребер различных «типов», ведущих из одной вершины в другую), транзитивные деревья (структуры, являющиеся транзитивным замыканием обычных деревьев), а также их комбинации. У логик, обладающих данным свойством, обычно более низкая вычислительная сложность, в частности, более просто строится разрешающий табло-алгоритм.

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

Связь с языком OWL[править | править исходный текст]

Язык веб-онтологий OWL разрабатывается как язык, на котором можно формулировать и публиковать в веб так называемые сетевые онтологии — формально записанные утверждения о понятиях и объектах некоторой предметной области. Одним из требований к таким онтологиям заключается в том, чтобы содержащиеся в них знания были «доступны» для машинной обработки, в частности, для автоматизированного логического вывода новых знаний из уже имеющихся. Для этого требуется, чтобы язык, на котором формулируются онтологии, имел точную семантику, а соответствующие логические проблемы были разрешимы (и имели практически допустимую вычислительную сложность). Кроме того, желательно, чтобы такой язык имел довольно большую выразительную силу, пригодную для формулировки на нём практически значимых фактов.

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

Соответствие терминов: имеющиеся в ДЛ понятия концепт, роль, индивид и база знаний в OWL соответствуют понятиям класс, свойство, объект и онтология, соответственно.

Официальной рекомендацией W3C от 10 февраля 2004 года является версия языка OWL 1.0. Данная спецификация языка OWL подразделяется на следующие варианты:

  • OWL-Lite — соответствует дескрипционной логике \mathcal{SHIF}(D);
  • OWL-DL — соответствует дескрипционной логике \mathcal{SHOIN}(D);
  • OWL-Full — не соответствует какой-либо ДЛ, более того, является неразрешимым.

Находящаяся в стадии рабочего черновика новая версия языка OWL 1.1 покрывает дескрипционную логику s\mathcal{ROIQ}(D), включающую в себя логику \mathcal{SHOIQ}(D), составные аксиомы вложенности ролей в TBox (буква \mathcal{R} в названии логики), а также аксиомы непересекаемости, рефлексивности, иррефлексивности и асимметричности ролей, универсальную роль (интерпретируемую как \Delta^\mathcal{I}\times\Delta^\mathcal{I}), конструктор концепта \exists R.\mathsf{Self} (интерпретируемый как множество элементов, являющихся \,R-последователем самих себя) и допускает утверждения \neg R(a,b) в ABox.[12]

Одновременно с этим разрабатывается следующая версия языка OWL 2.0, которая, помимо перечисленного, даст возможность формулировать онтологии в языке, соответствующем дескрипционной логике \mathcal{EL} (преимущество которой в том, что она имеет полиномиальную вычислительную сложность); привнесет синтаксические улучшения, позволяющие легче составлять запросы к базам знаний и выдавать ответы на них; а также будет содержать механизмы для формулировки правил логического вывода.[13]

Машины вывода и редакторы[править | править исходный текст]

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

  • CEL — поддерживает логику \mathcal{EL}+, имеющую полиномиальную сложность, написан на LISP;
  • FaCT++ — поддерживает логику s\mathcal{ROIQ}(D), а также OWL 2.0, реализует табло-алгоритм, написан на C++;
  • KAON2 — поддерживает логику \mathcal{SHIQ}, расширенную специальными правилами вывода, реализует алгоритм, основанный на резолюции, написан на Java;
  • Pellet — поддерживает логику s\mathcal{ROIQ}(D), а также OWL 1.1, реализует табло-алгоритм, написан на Java;
  • RacerPro — поддерживает логику \mathcal{SHIQ}(D), реализует табло-алгоритм, написан на LISP.

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

Существуют также редакторы онтологий, позволяющие создавать/редактировать онтологии, сохранять их в различных форматах, некоторые позволяют подключить блок рассуждений (англ. reasoner) и с его помощью произвести логический анализ онтологии. Одним из наиболее известных является редактор онтологий Protégé, позволяющий работать с онтологиями в языке OWL Full.

См. также[править | править исходный текст]

Примечания[править | править исходный текст]

  1. Рассел, Норвиг, 2006, с. 482
  2. Лапшин В. А., Онтологии в компьютерных системах. RSDN Magazine, 4, 2009.
  3. Description Logic Handbook, 2003, Basic Description Logics, pp. 43-95
  4. 1 2 3 4 Baader F. The Description Logic Handbook. — New York: Cambridge University Press, 2003. — ISBN ISBN 0-521-78176-0
  5. Schmidt-Schauß, M.; Smolka, G. (1991). «Attributive concept descriptions with complements». Artificial Intelligence 48: 1–26.
  6. 1 2 Schild, K. (1991). «A correspondence theory for terminological logics: Preliminary report». In Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI'91).: 466–471.
  7. Lutz, C.; Sattler, U.; Wolter, F. (2001). «Modal logics and the two-variable fragment». In Annual Conference of the European Association for Computer Science Logic (CSL'2001).
  8. Grädel, E.; Otto, M.; Rosen, E. (1997). «Two variable logic with counting is decidable». In Proc. of the 12th IEEE Symp. on Logic in Computer Science (LICS'97): 306–317..
  9. Horrocks, I.; Sattler, U.; Tobies, S. (1999). «Practical reasoning for expressive Description Logics». In Proc. of the 6th Int. Conference on Logic for Programming and Automated Reasoning (LPAR'99): 161–180.
  10. Tessaris S. Questions and answers: Reasoning and querying in Description Logic (PhD Thesis). — University of Manchester, 2001.
  11. Glimm, B.; Horrocks, I.; Lutz, C.; Sattler, U. (2007). «Conjunctive query answering for the description logic SHIQ». In Proc. of the 20th Int. Joint Conf. on Artificial Intelligence (IJCAI 2007). 31: 151–198.
  12. Сайт разработчиков языка OWL 1.1
  13. Новые возможности языка OWL 2.0

Ссылки[править | править исходный текст]

Литература[править | править исходный текст]