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

Аннотация

2 недели назад я написал небольшую заметку о неопределенности в онтологиях и был весьма польщен, что она вызвала определенный интерес (в связи с чем выражаю глубокую признательность всем оставившим комментарии). Как и было обещано, я начал работу над продолжением, в котором я планировал более подробно остановиться на семантике вероятностной неопределенности в 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) позволяет нам сказать только «Зенит обыграл Спартак», а истинность его следует (или не следует) исключительно семантически.
Существует несколько вариантов задания формальной семантики. Мы затронем модельно-теоретическую семантику (modeltheoretic semanticsMTS), т.к. именно она чаще всего используется в FOL и DL (а соответственно и в OWL). Причем MTS мы рассмотрим сразу на примере простого DL-языка, опустив все общие замечания, а заодно и FOL (логика предикатов и ее семантика описывается в любом учебнике по мат. логике).

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

С давних пор считается естественным представлять знания о предметной области в виде иерархии структурированных объектов, связанных между собой отношениями. На этой идее базируются такие формализмы, как фреймы, семантические сети, UML и т.д. К сожалению, все эти языки лишены формальной семантики, т.к. выражаемая в них информация предназначены для *человеческого*, а не *машинного* восприятия. Человеку понятно, что в определенном контексте если прямоугольник «А» нарисован над прямоугольником «Б» и соединен стрелкой, то класс Б является подклассом А. Машине это неясно, ей нужно объяснить формально.
Это можно сделать при помощи FOL и простой формулы: \forall x: B(x) -> A(x). Но с FOL существует ряд проблем: нет удобной поддержки иерархий, нет удобных средств описания структурированных классов, а также логический вывод разрешим только наполовину (здесь я надеюсь, что читатели понимают, что такое теоретическая разрешимость/неразрешимость языков, если нет — поговорим об этом в комментариях. Вкратце, неразрешимость означает, что в принципе невозможно существование алгоритма для определения в общем случае того, принадлежит ли данная строка данному языку).
Итак, с одной стороны 20-25 лет назад были семантические сети и фреймы, где было все, кроме формальной семантики, а с другой — логика предикатов, в которой была семантика, но не было удобных средств преставления знаний о предметной области. Решение было совершенно логичным: Рон Брахман (Ron Brachman) в своей знаменитой системе управления знаниями под названием KLONE предложил скрестить семантические сети и FOL, постаравшись взять лучшее из обоих миров. То, что получилось, было названо терминологической логикой (этот термин и сейчас можно встретить в старых статьях), а далее в процессе бурного развития превратилось в семейство DL.
Важно помнить несколько ключевых вещей о DL:

  • DL — это не логика, а семейство логик, обладающих разными возможностями. Соответственно, разные приложения могут выбирать для своих целей разные логики семейства DL. Например, OWL Lite основан на DL под названием SHIF(D), а OWL-DL — на SHOIN(D) (в самом конце будет приведена краткая расшифровка аббревиатур для популярных DL)
  • Любая DL является подмножеством FOL. Это означает, что любое утверждение на DL можно представить в виде формулы FOL (но не наоборот!). При этом они семантически совместимы, т.е. если преобразовать базу знаний DL в базу знаний FOL, то из нее можно будет сделать такие же логические выводы, как и до преобразования.
  • В синтаксисе DL явно не используются переменные и кванторы (что очень удобно). Например утверждение A \subset B в DL — это то же самое, что и FOL-формула \forall x A(x) -> B(x), но без переменных.
  • Большинство логик DL аккуратно проектируются так, чтобы они были подмножеством не только FOL, но и его специального фрагмента под названием guarded fragment. Это означает, что DL, как правило, обладают свойством разрешимости, которое достигается за счет урезания некоторых возможностей FOL (в частности, тех же переменных). Забегая вперед замечу, что поэтому OWL DL разрешим и для него есть логические процессоры, а OWL Full, который не базируется на DL, — нет и для него логических процессоров нет.

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

ALC

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

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

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

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

  • Пересечение классов или коньюнкция (С \and D)
  • Объединение классов или дизьюнкция (C \or D)
  • Дополнение класса или отрицание (\not C)
  • Универсальное ограничение свойства (\forall R.C)
  • Экзистенциальное ограничение свойства (\exists R.C)

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

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

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

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

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

  • I отображает каждый базовый класс в NC на некоторое подмножество Dom, при этом I(top) = Dom, а I(bottom) = пустое множество
  • I отображает каждое свойство в NR на некоторое отношение на Dom (подмножество декартова произведения Dom x Dom)
  • I отображает каждый объект в NI на элемент в Dom

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

  • Интерпретация C \and D (или I(C \and D)) эквивалентна I(C) \and I(D)
  • I(C \or D) = I(C) \or I(D)
  • I(\not C) = Dom \ I(C)
  • I(\forall R.C) = все такие x \in Dom, что для любого y \in Dom верно, что (x,y) \in I(R) -> y \in I(C)
  • I(\exists R.C) = все такие x \in Dom, что существует такой y \in I(C), что (x,y) \in I(R)

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

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

  • Интерпретация I удовлетворяет аксиоме C \subset D если I(C) \subset I(D)
  • I удовлетворяет аксиоме a:C \in D если 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.
Вот, собственно, и вся семантика. При помощи домена и интерпретирующей функции мы *формально* определили смысл классов, объектов, свойств, а также логических формул (аксиом). Теперь можно переходить к логическому выводу.

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

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

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

  • Класс С когерентен в онтологии О тогда и только тогда, когда добавление новой аксиомы a:C (где объект «а» ранее не встречался в О) не приводит к потере согласованности. Т.е. вопрос когерентности С решается путем добавления новой аксиомы к О и проверки согласованности.
  • Аксиома А выводится из онтологии О тогда и только тогда, когда добавления *отрицания* аксиомы А к онтологии О приводит к потере согласованности. Здесь необходимо определить, что такое отрицание аксиомы. Для аксиомы «C \subset D» отрицанием будет аксиома а:(C \and \not D), а для a:C отрицанием будет a:\not C.

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

Все, что требуется для всех задач логического вывода в ALC — это алгоритм проверки согласованности онтологии.

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

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

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

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

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

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

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

PS. Приношу свои извинения за текстовое отображение математических символов в стиле LaTeX. Если честно, то просто лень сейчас разбираться c WordPress (может Сергей подскажет). Надеюсь, что у вас не будет из-за этого лишних проблем с пониманием.


Понравилась статья? Поделитесь с друзьями!


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

  1. Очень полезная и грамотная статья. Большое спасибо.

  2. Nata_Ke:

    Для поиска в Интернет хорошо бы также сопоставить терминам, которые привёл Павел, англоязычные эквиваленты:
    «когерентность класса» (я бы использовала еще «выполнимость») — «concept satisfiability»,
    «согласованность онтологии» — «ontology consistency».

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

  4. Да, Наталья права. Когерентность класса (concept coherency) чаще использовалась раньше в статьях по DL, в OWL чаще используется concept satisfiability.
    Интересный вопрос с согласованностью онтологии. Сейчас чаще используют именно consistency, хотя лично я бы предпочел satisfiability. По двум причинам:
    1. По сути нет никакой разницы по смыслу между concept satisfiability и ontology consistency. И там и там речь идет о наличии модели.
    2. Есть логики, где satisfiability и consistency обозначают *принципиально* разные вещи. Один из примеров — P-SHIQ, которая стоит за Pronto. При этом satisfiability по-прежнему означает наличие модели (этот термин *всегда* означает одно и то же), а consistency — способность делать логические выводы из данной онтологии. В частности, онтология может быть выполнимой (satisfiable), но несогласованной (inconsistent).
    Но в OWL принято говорить о согласованности, поэтому я так и оставил.
    Спасибо за замечание!

  5. А, как Вы думаете, в каких задачах может появиться необходимость использования OWL full?

  6. Это очень сложный вопрос. Отвечу так: реальных приложений, в которых бы выбор OWL Full был сделан осознанно (а не, скажем, ввиду ошибок/багов при проектировании онтологии в OWL DL) я не знаю. Мое мнение таково, что OWL Full — это *недоразумение*, явившееся нежелательным результатом проектирования OWL как семантического расширения RDF. Оговорюсь сразу, что это только мое мнение по очень спорному вопросу (у рабочей группы OWL нет единой позиции по нему).

  7. Все очень понятно объяснено — проштудировав статью, стал больше понятного в других работах, ранее понимание было приблизительное. Хотел спросить насчет такого термина как «уточнение», иногда встречаю его, но точно не могу понять. В одном источнике сказано: «Отношение уточнения абстрактных типов данных отличается от отношения тип/подтип тем, что спецификации типа наследуются подтипом, в то время как при отношении уточнения элементы
    спецификаций могут переименовываться, иметь
    отличную структуру и функциональность, но с
    известными отношениями между элементами двух
    моделей.» Есть, например, 2 онтологии в одной — класс МАШИНА имеет свойство МАРКА, связаннное с экземпляром класса МАРКА, в другой онтологии АВТОМОБИЛЬ имеет (к примеру) свой-во ВНЕШНИЙ_ВИД, связанное с экземплярами классов МАРКА/МОДЕЛЬ/ЦВЕТ.
    Можно ли тогда утверждать, что МАШИНА уточняет АВТОМОБИЛЬ?

  8. OWL — это монотонная логика и отношения is-a (subsumption) между классами — это именно «тип/подтип». Т.е. выражаясь формально, если А — подкласс В, то все, что верно для экземпляра В, будет также верно для экземпляра А (но не наоборот).
    В Вашем источнике наверное речь идет о том, что такое отношение (см., кстати, Liskov substitution principle) не совсем справедливо для ООП, т.к. в нем имеет место полиморфизм. Видимо в этих целях применяют термин «уточнение». Бывают немонотонные логики, которые позволяют «уточнять» ранее сделанные выводы. В частности, P-SHIQ — вероятностное расширение SHIQ. Например, «Сэм не летает» — это уточнение вывода «Сэм летает», сделанное после того, как выяснилось, что Сэм — не просто птица, а пингвин. В OWL такое невозможно, пингвины либо не должны быть подклассами птиц, либо должны летать.
    Что касается примера, то я бы пока тут утверждать ничего бы не стал :) Вот если сделать свойство ИМЕТЬ_МАРКУ подсвойством свойства ИМЕТЬ_ВНЕШНИЙ_ВИД и добавить класс-объединение МАРКА/МОДЕЛЬ/ЦВЕТ — вот тогда МАШИНА станет подтипом АВТОМОБИЛЬ.

  9. Можно ли утверждать(и верно ли), что семантика концепта *формально* задается, как его функцией интерпретации, так и аксиомами, касающимися его, и для которых ф-я интерпретации является моделью?
    Т.е. если есть термин МАШИНА:
    I(МАШИНА) = {«Жигули_моего_друга»,»Москвич_дяди_Васи»}
    I(СРЕДСТВА_ПЕРЕДВИЖЕНИЯ)={«Мой_велосипед»,»Трактор_у_дома»,»Жигули_моего_друга»,»Москвич_дяди_Васи»}
    Есть аксиома МАШИНА \subset СРЕДСТВА_ПЕРЕДВИЖЕНИЯ ей удовлетворяет функция интерпретации I: I(МАШИНА) \subset I(СРЕДСТВА_ПЕРЕДВИЖЕНИЯ)

    О смысле концепта МАШИНА мы знаем, что это то то и то и он обладает определенными свойствами + (благодаря аксиоме) мы такдже знаем что это средсво передвижения, а соответвенно обладает атрибутами, характерными для средства передвижения.

  10. Ну фактически да. Я всегда предлагаю смотреть на аксиомы как на ограничения. Т.е. если у нас есть просто концепт МАШИНА, то его интерпретацией может быть любое множество. Как только мы добавляем аксиому, что МАШИНА — это подкласс СРЕДСТВО_ПЕРЕДВИЖЕНИЯ, то мы автоматически накладываем ограничения на возможные интерпретации класса МАШИНА. Теперь уже интерпретацией может быть не любое множество, а только некоторое подмножество интерпретации концепта СРЕДСТВО_ПЕРЕДВИЖЕНИЯ.
    Таким образом, онтология — это не что иное, как система ограничений на возможные интерпретации концептов, свойств и объектов некоторой предметной области.
    Другое дело, что очень редко бывает так, что у концепта может быть только одна интерпретация. Как правило, их либо много, либо вообще нет (если он unsatisfiable). Даже в твоем примере существует несколько возможных интерпретаций концепта МАШИНА.

  11. До конца не могу понять такую вещь — воизбежании парадоска лжеца, создается 2 языка: с помощью одного создаются утверджения, с помощью другого — формулируются заключения об истинности этих утверждений.
    В случае ALC с помощью чего задается заключение об истинности — с помощью аксиомы или с помощью установления того факта что ее удовлетворяет или неудовлетворяет ее интерпретация?
    Например, есть аксиома:
    АКУЛЫ /subset РЫБЫ,
    есть ее интерпретация:
    I(АКУЛЫ /subset РЫБЫ)= I(АКУЛЫ) /subset I(РЫБЫ), где I(АКУЛЫ)={воробей, ворона} I(РЫБЫ)= {все рыбы}

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

  12. На основе какой-то одной, конкретной интерпретации нельзя доказать истинность (только выполнимость). Аксиома истинна в данной онтологии, если ЛЮБАЯ интерпретация онтологии также удовлетворяет аксиоме.
    Т.е. если в твоем примере есть некая онтология, которой удовлетворяет твоя интерпретация, то мы можем только сказать, что данная аксиома не вытекает из данной онтологии.
    В ALC заключение об истинности делается семантически. Т.е. делается предположение, что аксиома не истинна и оно добавляется в онтологию. Например, в твоем примере будет добавлен объект, являющийся акулой, но не рыбой. После этого будет сделана попытка построить интерпретацию онтологии, удовлетворяющую этому предположению. Если таковой не существует (т.е. пришли к противоречию), то значит исходная аксиома истинна. Если же таковая существует (например, твоя интерпретация выше), то аксиома не истинна.

  13. В OWL онтологиях, как правило используются символические лейблы для терминов: ЧЕЛОВЕК, HUMAN, CAR, HDD и др. Можно ли считать их в какой-то степени функциями интерпретации (одновременно задается термин и ф-я интерпретации), т.е. эксперт когда разрабатывает онтологию и называет термин — МАШИНА — подразумевает определенный набор объектов реального мира?

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

  15. :sad: Тогда я до конца не могу понять задаются ли ф-и интерпретации? и если да то в какой форме?

    Я находил определения онтологии в виде тройки множест: термины, отношения и функции интерпретации терминов/отношений.
    Т.е. интерпретации задаются, как-то неявно, но при этом, получается, они должны быть формальными, иначе ведь не получиться определять удовлетворяют ли они аксиомам.
    Если рассмотреть такой пример:
    Есть термин КВАДРАТ — это прямоугольник, у которого две смежные стороны равны или ромб, у которого все углы прямые.

    Это строгое определение в геометрии — т.е. задан термин и его значение. Используя это значение, можно из всего множества фигур выделить подмножнство, соответствующее ему — соответвенно ЗНАЧЕНИЕ термина, получается, является функцией интерпретации.

    Соответвенно если строиться онтология, скажем, геометрии Эвклида — то в ней сответвенно будут классы с лейблами: РОМБ, КВАРДАТ, ПРЯМОУГОЛЬНИК, связанные аксиомами:
    КВАДРАТ /subclass ПРЯМОУГОЛЬНИК
    КВАДРАТ /subclass РОМБ

    Соответвенно при проверке удовлетворимости I(КВАДРАТ /subclass ПРЯМОУГОЛЬНИК) аксиоме КВАДРАТ /subclass ПРЯМОУГОЛЬНИК, мы должны проверить истинно ли утверждение: I(КВАДРАТ) /subset I(ПРЯМОУГОЛЬНИК)
    Соответвенно функция интерпретации — есть определение термина КВАДРАТ и ПРЯМОУГОЛЬНИК, которое следует из их лейблов.

    Т.е. я не могу понять как еще можно задать фун-ии интерпретации, кроме как используя названия терминов.

  16. Еще раз: в онтологии (по крайней мере в DL и OWL) функции интерпретации дизайнером не задаются *никак*. Их в синтаксисе нет *вообще*. В любой логике есть строгое разделение на синтаксис (то, что разработчик определяет явно) и семантику (то, как reasoner интерпретирует синтаксис).
    Насчет тройки (термин, отношение, функция интерпретации) — то это неверно. По крайней мере для OWL (и любой логики) это 100% не так. Как только разрешить доступ к интерпретации в синтаксисе — мы тут же получим парадокс лжеца в чистом виде.
    В твоем примере с квадратом никакая функция интерпретации не задается. Достаточно простой аксиомы:
    Square = Rombus \and (\forall angle.Right).
    Видишь, я нигде явно не задаю отображение класса Square на множество объектов реального мира. Кстати, аксиома Square \subclass Rombus будет следствием моей онтологии, т.к. моя аксиома *гарантирует*, что I(Square) \subset I(Rombus)

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

  18. Естественно! Больше этим интеграторам онтологий информацию взять неоткуда, «моделей» (т.е. интерпретаций) онтологий они не видят. Они используют статистику и иногда онтологии верхнего уровня (или словари) для стыковки терминов-синонимов (типа МАШИНА — АВТОМОБИЛЬ). Поэтому и проблем и ошибок у них столько.
    В принципе, можно попробовать делать интеграцию на основе сходства моделей. Явно модель ни одного класса нам недоступна (более того, их может быть бесконечно много). Однако можно попробовать получить так называемую «каноническую модель» — некое представление того, как выглядят модели данного класса (грубо говоря, что у них общего). И делать интеграцию терминов из разных онтологий на основании схожести их канонических моделей.
    У нас в прошлом году был студент из Германии, который исследовал визуализацию канонических моделей OWL-классов и сделал прототип плагина для Протеже для их демонстрации. Если интересно — посмотри (и спрашивай, если есть вопросы) [1]

    [1] http://www.cs.man.ac.uk/~bauerj/supermodel/

  19. alex_kart:

    несколько неясно, что означает
    # Универсальное ограничение свойства (\forall R.C)
    # Экзистенциальное ограничение свойства (\exists R.C)
    нельзя ли объяснить на конкретном примере из естественного языка.

    Еще насчет функции интерпретации. Как я понял это просто связь между абстрактным набором символов который представляет онтологию и реальным миром? Т.е если к примеру с помощью Jena создать представление онтологии в виде программы на джаве Jena фактически будет представлять функцию интерпретации I, а Dom будет являться написанной программой?

  20. \forall R.C говорит, что *все* объекты, связанные отношением R с объектом нашего класса, будут принадлежать классу С. Например, можно сказать, что *все*, что ест вегетерианец, не является мясом (\forall eats.\not(Meat)). Заметь, что здесь пока не утверждается, что он непременно ест хоть что-нибудь.
    \exists R.C говорит, что есть *хотя бы* один объект, который связан с объектом нашего класса через R и является членом C. Например, любой вегетерианец ест *хотя бы* одно растение \exists eats.Plant.
    Между этими ограничениями существует очевидное свойство, знакомое по логике предикатов: \forall R.C = not(\exists R.\not(C)). Т.е. «вегетерианец ест только «не мясо» эквивалентно «не существует такого мяса, которое ест вегетерианец».
    Насчет второго вопроса: да, интерпретация — это именно связь символьного представления онтологии с реальным миром. Как я уже писал тут, явно интерпретации в онтологии не представляются, но ничего не мешает в качестве *одной* возможной интерпретации рассматривать набор программных объектов (уж в Jena или в чем-то еще — неважно).

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *


Ответить с помощью ВКонтакте: