О формальных основах OWL

Павел Клинов
	Павел Клинов
	Pavel Klinov
Род деятельности:	научно-исследовательская
Роль участника:	Участник, Модератор, Администратор
Основной раздел:	Semantic Web
Круг интересов:	логика, OWL, неопределенность и неточность знаний
Дата рождения:	1981
Место рождения:	Москва
Гражданство:	РФ
Сайт:	http://www.cs.man.ac.uk/~klinovp
Nickname	PavelK
О себе:	Аспирант (университет Манчестера, Великобритания)

Материал из Semantic Future

Перейти к: навигация, поиск

Содержание

1 Аннотация
2 Введение
3 Математическая логика и формальная семантика – это скучно?!
4 DL: Шаг навстречу логическому представлению знаний
5 Язык ALC
6 Вместо заключения

Аннотация

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

Введение

Итак, начнем с главного: что такое OWL? Многие из вас знают, что OWL – это язык для описания онтологий в Web. Но многие ли смогут ответить на вопрос, почему OWL таков, как он есть? Что стоит за его синтаксисом? И почему для описания онтологий пришлось создавать какой-то новый язык. Почему бы не использовать RDF или старые добрые фреймы и семантические сети, topic maps и т.д. и т.п. Или просто логику предикатов первого порядка?

Главное, что отличает OWL от всех этих формализмов (кроме предикатной логики) – это его семантика. Я не могу себе позволить пуститься в пространные сравнения семантики OWL и семантики вышеперечисленных языков (хотя у меня есть желание написать заметку о семантической совместимости OWL и RDF). Вместо этого мы просто обсудим семантику OWL и ее привлекательность. Для этого придется слегка углубиться в математику и немножко вспомнить формальную логику, так как OWL – это не что иное, как семейство логик (так называемых Description Logics – описательных логик или DL) + некоторый синтаксис (их несколько: RDF/XML, абстрактный синтаксис, манчестерский синтаксис, OWL/XML, etc.). Поэтому мы начнем с семантики в логике вообще, а затем поговорим о семантике простейших DL. Я также попробую объяснить принципы логического вывода в DL, которые используются, в том числе, и в OWL.

Математическая логика и формальная семантика – это скучно?!

Искренне надеюсь, что большинство читателей еще не до конца забыли курс математической логики 1-2 курса университета и помнят, что такое «логика» в формальном смысле этого слова. Логика – это совокупность двух компонентов:

Синтаксис или формальное описание языка. Напомню, что формальный язык – это множество строк, построенных из символов определенного алфавита. Описание языка обычно задается в виде грамматики, в частности, широко используется форма Бэкуса-Наура. Грамматики для логики высказываний, логики предикатов, а также XML и огромного разнообразия языков программирования несложно найти в Интернете.

Семантика или механизм придания смысла предложениям, описанным в соответствии с синтаксисом.

Ключевое отличие логик от других формальных языков – это наличие формальной семантики. Например, С++ не имеет формальной семантики, так как смысл конструкций С++ задан в Стандарте С++ на естественном языке (английском). В случае же логики, семантика описывается формально, т.е.по сути является вторым формальным языком (первый используется для описания синтаксиса). Иногда его еще называют метаязыком.

Зачем же нужен этот второй язык, который есть у логики предикатов первого порядка (FOL), DL, а также OWL? По двум основным причинам: во-первых, он лишен неоднозначностей, т.е. смысл логических утверждений всегда строго определен (в отличие от неформального описания семантики). А во-вторых, наличие второго языка позволяет разнести по разным языкам сами логические утверждения и заключения об их истинности. Например, в классических логиках запрещены утверждения типа «утверждение “Зенит обыграл Спартак” – ложно». Как известно, они приводят к знаменитому парадоксу лжеца, поэтому еще в 50-х знаменитый философ и логик Альфред Тарский (Alfred Tarski) предложил формальную (модельно-теоретическую семантику), чтобы его избежать. Теперь, синтаксис логического языка (например, FOL) позволяет нам сказать только «Зенит обыграл Спартак», а истинность его следует (или не следует) исключительно семантически. Существует несколько вариантов задания формальной семантики. Мы затронем модельно-теоретическую семантику (model-theoretic semantics – MTS), т.к. именно она чаще всего используется в FOL и DL (а соответственно и в OWL). Причем MTS мы рассмотрим сразу на примере простого DL-языка, опустив все общие замечания, а заодно и FOL (логика предикатов и ее семантика описывается в любом учебнике по мат. логике).

DL: Шаг навстречу логическому представлению знаний

С давних пор считается естественным представлять знания о предметной области в виде иерархии структурированных объектов, связанных между собой отношениями. На этой идее базируются такие формализмы, как фреймы, семантические сети, UML и т.д. К сожалению, все эти языки лишены формальной семантики, т.к. выражаемая в них информация предназначены для человеческого, а не машинного восприятия. Человеку понятно, что в определенном контексте если прямоугольник «А» нарисован над прямоугольником «Б» и соединен стрелкой, то класс Б является подклассом А. Машине это неясно, ей нужно объяснить формально.

Это можно сделать при помощи FOL и простой формулы: $\forall x: B(x) \rightarrow A(x)$ . Но с FOL существует ряд проблем: нет удобной поддержки иерархий, нет удобных средств описания структурированных классов, а также логический вывод разрешим только наполовину (Здесь я надеюсь, что читатели понимают, что такое теоретическая разрешимость/неразрешимость языков, если нет – поговорим об этом в комментариях. Вкратце, неразрешимость означает, что в принципе невозможно существование алгоритма для определения в общем случае того, принадлежит ли данная строка данному языку).

Итак, с одной стороны 20-25 лет назад были семантические сети и фреймы, где было все, кроме формальной семантики, а с другой – логика предикатов, в которой была семантика, но не было удобных средств преставления знаний о предметной области. Решение было совершенно логичным: Рон Брахман (Ron Brachman) в своей знаменитой системе управления знаниями под названием KL-ONE предложил скрестить семантические сети и FOL, постаравшись взять лучшее из обоих миров. То, что получилось, было названо терминологической логикой (этот термин и сейчас можно встретить в старых статьях), а далее в процессе бурного развития превратилось в семейство DL. Важно помнить несколько ключевых вещей о DL:

DL – это не логика, а семейство логик, обладающих разными возможностями. Соответственно, разные приложения могут выбирать для своих целей разные логики семейства DL. Например, OWL Lite основан на DL под названием $\mathcal{SHIF}(D)$ , а OWL-DL – на $\mathcal{SHOIN}(D)$ (в самом конце будет приведена краткая расшифровка аббревиатур для популярных DL)

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

В синтаксисе DL явно не используются переменные и кванторы (что очень удобно). Например, утверждение $A \sqsubset B$ в DL – это то же самое, что и FOL-формула $\forall x A(x) \rightarrow B(x)$ , но без переменных.

Большинство логик DL аккуратно проектируются так, чтобы они были подмножеством не только FOL, но и его специального фрагмента под названием guarded fragment. Это означает, что DL, как правило, обладают свойством разрешимости, которое достигается за счет урезания некоторых возможностей FOL (в частности, тех же переменных). Забегая вперед, замечу, что поэтому OWL DL разрешим и для него есть логические процессоры, а OWL Full, который не базируется на DL, – нет и для него логических процессоров нет.

На этом мы закончим пространные рассуждения о DL вообще и перейдем к конкретному примеру – логике $\mathcal{ALC}$ , которая хотя и проста, но содержит многие ключевые возможности OWL. $\mathcal{ALC}$ – это подмножество DL, на которых базируется OWL, причем для очень многих реальных онтологий вполне достаточно $\mathcal{ALC}$ .

Язык ALC

Язык $\mathcal{ALC}$ (Attributive Language with Complements) был впервые рассмотрен Манфредом Шмидтом-Шауссом и Гертом Смолкой (Manfred Schmidt-Shauss, Gert Smolka) в начале 90-х. Как и любая логика, он состоит из синтаксиса и семантики. Начнем с синтаксиса.

Синтаксис $\mathcal{ALC}$

Язык $\mathcal{ALC}$ содержит алфавит (т.е. набор базовых символов), который состоит из трех компонентов:

Набор имен базовых классов (NC) плюс два специальных класса ( $\top$ или универсальный класс и $\bot$ – пустой класс)
Набор имен свойств (NR)
Набор имен объектов (NI)

Центральной возможностью $\mathcal{ALC}$ , как и многих DL, является возможность описания сложных классов (понятий). Это делается при помощи следующих операторов, называемых «конструкторами классов»:

Пересечение классов или конъюнкция $C \sqcap D$
Объединение классов или дизъюнкция $C \sqcup D$
Дополнение класса или отрицание $\neg C$
Универсальное ограничение свойства $\forall R.C$
Экзистенциальное ограничение свойства $\exists R.C$

Пример: Допустим, у нас есть базовые классы Мать и Отец. На их основе мы можем определить сложный класс Родитель как «Мать Отец». Или предположим, что есть базовые классы Человек и свойство «имеетРебенка». Тогда класс Родитель можно определить как «Человек ( имеетРебенка.Человек)». Неформально это означает: «К классу Родитель относится любой объект, который, во-первых, является человеком, а, во-вторых, имеет ребенка, являющегося человеком» (ниже мы покажем, как эту семантику можно задать формально).

Далее рассмотрим логические формулы в $\mathcal{ALC}$ (они называются аксиомами). Аксиомы бывают 3-х типов:

Отношения типа «дочерний класс». Эти аксиомы имеют вид $C \sqsubseteq D$ , где C и D – это произвольные (возможно сложные) классы.
Отношения типа «экземпляр класса». Они имеют вид a:C, где a обозначает объект, а C – произвольный класс.
Отношения типа «экземпляр свойства». Они имеют вид (a,b):P, где a,b обозначают два объекта, а Р – произвольное свойство.

Набор аксиом типа 1 называется TBox (сокращение от terminological box). Набор аксиом типа 2 и 3 называется ABox (assertional box).

База знаний (или онтология) в $\mathcal{ALC}$ – это совокупность TBox и ABox. Перед тем, как перейти к формальной семантике, скажем пару слов о TBox и ABox. TBox – это фактически описание иерархии классов (понятий предметной области). ABox – это набор фактов о конкретных объектах, т.к. к каким классам они относятся и какими свойствами обладают. Теперь определим эту семантику формально:

Семантика $\mathcal{ALC}$

Семантика $\mathcal{ALC}$ является разновидностью MTS. Это означает, что в ее основе лежат два ключевых компонента: домен Dom и интерпретирующая функция I. Dom – это просто конечное множество элементов (иногда их называют элементами реального мира), а I определяется индуктивно следующим образом:

I отображает каждый базовый класс в NC на некоторое подмножество Dom, при этом $I(\top) = Dom$ , а $I(\bot) = \emptyset$
I отображает каждое свойство в NR на некоторое отношение на Dom (подмножество декартова произведения $Dom \times Dom$ )
I отображает каждый объект в NI на элемент в Dom

Попросту говоря, $I (C) = X$ означает примерно следующее: «Символ С обозначает множество элементов Х реального мира». Например «Слово „Автомобиль“ обозначает множество всех самодвижущихся 4-хколесных устройств» – это не что иное, как интерпретация класса Автомобиль. Далее самое интересное – как интерпретируются сложные классы:

Интерпретация $C \sqcap D$ (или $I(C \sqcap D)$ ) эквивалентна $I(C) \cap I(D)$
$I(C \sqcup D) = I(C) \cup I(D)$
$I(\neg C) = Dom \setminus I(C)$
$I(\forall R.C) = \{x \in Dom | \forall y \in Dom, (x,y) \in I(R) \rightarrow y \in I(C)\}$
$I(\exists R.C) = \{x \in Dom | \exists y \in I(C), (x,y) \in I(R)\}$

Не пугайтесь формул. Например, предпоследняя формула задает следующий простой смысл для конструктора $\forall R.C$ : «Если класс X определен как $\forall R.C$ , то X обозначает множество всех объектов x, таких что все объекты, связанные с ними свойством R являются элементами класса С». Например, класс « имеетРебенка.Мальчик» интерпретируется как набор всех объектов, таких что все их дети являются мальчиками. Класс « имеетРебенка.Мальчик» интерпретируется как набор всех объектов, у которых есть хотя бы один ребенок мужского пола.

Далее переходим от классов к аксиомам:

Интерпретация I удовлетворяет аксиоме $C \sqsubseteq D$ если $I(C) \sqsubseteq I(D)$
I удовлетворяет аксиоме a:C если $I(a) \in I(C)$
I удовлетворяет аксиоме (x,y):P если $(I(x),I(y)) \in I(P)$

Если интерпретация I удовлетворяет некоторой аксиоме А, то она называется моделью А (отсюда и название семантики – модельно-теоретическая). Например, если мы говорим об аксиомах типа 1, удовлетворение попросту означает, что смысл классов С и D не противоречит смыслу аксиомы.

Теперь самое главное:

Интерпретация I удовлетворяет TBox (или является моделью TBox) если она является моделью всех аксиом TBox. Аналогично определяется модель ABox. Наконец, интерпретация является моделью онтологии, если она является моделью ее TBox и ABox. Вот, собственно, и вся семантика. При помощи домена и интерпретирующей функции мы формально определили смысл классов, объектов, свойств, а также логических формул (аксиом). Теперь можно переходить к логическому выводу.

Задачи логического вывода в $\mathcal{ALC}$

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

Согласованность (или непротиворечивость) онтологии. Онтология называется непротиворечивой, если у нее существует, хотя бы, одна модель. Другими словами, если существует такой способ интерпретации (т.е. присвоения смысла) классов, объектов и свойств, который не противоречит ни одной заданной аксиоме (TBox или ABox).

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

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

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

Класс С когерентен в онтологии О тогда и только тогда, когда добавление новой аксиомы a:C (где объект а ранее не встречался в О) не приводит к потере согласованности. Т.е. вопрос когерентности С решается путем добавления новой аксиомы к О и проверки согласованности.

Аксиома А выводится из онтологии О тогда и только тогда, когда добавления отрицания аксиомы А к онтологии О приводит к потере согласованности. Здесь необходимо определить, что такое отрицание аксиомы. Для аксиомы $C \sqsubset D$ отрицанием будет аксиома $a:(C \sqcap \neg D)$ , а для a:C отрицанием будет $a:\neg C$ .

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

Все, что требуется для всех задач логического вывода в $\mathcal{ALC}$ – это алгоритм проверки согласованности онтологии.

То же самое справедливо и для других DL, и для OWL. Процессоры логического вывода по своей сути делают только одно: проверяют согласованность онтологии. Все остальное – это тривиальная работа препроцессора, заключающаяся в добавлении отрицаний аксиом (плюс некоторые другие несущественные моменты). Отдельного рассмотрения заслуживают алгоритмы классификации (т.е. вычисления всех возможных отношений типа «подкласс» между всеми парами классов, это позволяет построить законченную иерархию классов), поскольку наивное сведение к задаче согласованности будет крайне неэффективно. Но технологии оптимизации сейчас настолько обширны, что их обсуждение займет несколько статей (даже не считая тех, о которых я не в курсе, так как процессоры постоянно совершенствуются).

Вместо заключения

Пока это все. Сегодня у меня уже нет сил писать про принципы алгоритмов проверки согласованности в $\mathcal{ALC}$ (так называемые tableaux-based proofs). Если будет интерес, то напишу чуть позже. Хочу только сказать, что практически все принципы (синтаксические и семантические) $\mathcal{ALC}$ по-прежнему работают в более мощных DL, в том числе и тех, на которых основаны OWL Lite, OWL DL и новый OWL 2 (его логика называет $\mathcal{SROIQ}(D)$ ).

Последнее, что я бы хотел сделать – это расшифровать некоторые аббревиатуры. Наверное, многие из вас видели эти странные наборы символов – $\mathcal{SHIQ}$ , $\mathcal{SHIF}$ , $\mathcal{SHOIN}$ , $\mathcal{SROIQ}$ и т.д. Когда я только начинал заниматься DL, они повергали меня в ужас. Надеюсь, что следующее небольшое объяснение наиболее популярных букв кому-то поможет. Итак:

Начнем с S. DL S – это $\mathcal{ALC}$ + транзитивные свойства (ее еще иногда называют $\mathcal{ALC}+$ ). Транзитивность означает, что из R(a,b) и R(b,c) вытекает R(a,c) для любых a, b, c. Буква S скорее всего произошла от известной модальной логики S4, которая в определенном смысле является синтаксической формой $\mathcal{ALC}$ (кстати, это очень интересная тема!).
$\mathcal{SH}$ – это $\mathcal{S}$ + иерархии свойств (а не только классов как в $\mathcal{ALC}$ ).
$\mathcal{SHI}$ – это $\mathcal{SH}$ + обратные (inverse) свойства. R- является обратным по отношению к R, если R-(x,y) эквивалентно R(y,x).
$\mathcal{SHIF}$ – это $\mathcal{SHI}$ + функциональные свойства. Т.е. есть возможность объявлять некоторые свойства как функции (например, «мать» – это явно функциональное свойство, т.к. она у человека только одна).
$\mathcal{SHIN}$ – это $\mathcal{SHI}$ + ограничения на размер области значений свойств (т.н. non-qualified number restrictions)
$\mathcal{SHIQ}$ – это $\mathcal{SHI}$ + ограничения на размер области значений свойств и класс значений свойств (qualified number restrictions). Например, можно сказать: «>2 имеетРебенка.Человек». Это означает, что определяется класс объектов, которые имеют более двух детей (объектов класса Человек). Таким образом, в частности, можно определить класс МногодетнаяМать.
$\mathcal{SHOIQ}$ – это $\mathcal{SHIQ}$ + так называемые номиналы (nominals). Они позволяют описывать классы в виде перечислений объектов. Например, можно определить класс СНГ как {Россия, Украина, Беларусь, …}, где каждый элемент – это просто объект. Внимание: эта возможность – самая проблемная в плане производительности и вычислительной сложности! Совместное использование номиналов, обратных свойств и численных ограничений приводит к скачку сложности алгоритма проверки согласованности с EXPTIME-Complete до NEXPTIME-Complete.
$\mathcal{SROIQ}$ – это $\mathcal{SHOIQ}$ , в котором иерархии свойств расширены до композиций свойств (одно из главных новшеств OWL 2).
Наконец $\mathcal{SROIQ}(D)$ – это $\mathcal{SROIQ}$ + так называемые «типы данных» и свойства, связывающие объекты с типами данных. Например, если нам надо сказать, что рост Анны = 180, то «180» логично задавать в виде числа (тем более, что xs:integer определен в XML Schema), а не в виде служебного объекта.

Разумеется, все буквы можно компоновать произвольным образом, создавая тем самым DL, наиболее подходящую для вашего конкретного приложения. Ну вот и все. Теперь вы понимаете, что такое $\mathcal{SHIF}(D)$ , лежащий в основе OWL Lite или $\mathcal{SHOIN}(D)$ , который лежит в основе OWL DL.

Заранее благодарен за комментарии!

О формальных основах OWL

Содержание

Аннотация

Введение

Математическая логика и формальная семантика – это скучно?!

DL: Шаг навстречу логическому представлению знаний

Язык ALC

Вместо заключения

Личные инструменты

Пространства имён

Варианты

Просмотры

Действия

Поиск

Проект SF:

Деятельность:

Сообщество:

Хранилище знаний:

Гиды:

Руководства:

Инструменты