Описова Логіка

Описо́ві ло́гіки (англ.

Вони поєднують в собі, з одного боку, багаті виражальні можливості, а з іншого — хороші обчислювальні властивості, такі як розв'язність і відносно невисока обчислювальна складність основних логічних проблем, що робить можливим їх застосування на практиці. Таким чином, описові логіки являють собою компроміс між виражальністю і розв'язністю. Описову логіку можна розглядати як розв'язні фрагменти логіки предикатів, синтаксично ж вони близькі до модальних логік.

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

Загальні відомості

Описова Логіка 
Карта знань Описової Логіки

Описові логіки оперують поняттями концепт і роль, відповідними в інших розділах математичної логіки поняттям «одномісний предикат» (або множина, клас) та «двомісний предикат» (або бінарне відношення). Інтуїтивно, концепти використовуються для опису класів деяких об'єктів, наприклад, «Люди», «Жінки», «Машини». Ролі використовуються для опису двомісних відносин між об'єктами, наприклад, на безлічі людей є двомісне відношення «X є_родич_для Y», а між людьми і машинами є двомісне відношення «X має_у_власності Y», де як X і Y можна підставляти довільні предмети. За допомогою мови Описової логіки можна формулювати твердження загального вигляду — про класи взагалі (будь-яка Жінка є Людина, будь-яка Машина є_у_власності не більше ніж у однієї Людини) та приватного виду — про конкретні об'єкти (Марія є жінка, Іван має_у_власності_машину1).

На жаргоні описової логіки набір тверджень загального вигляду називається TBox, набір тверджень приватного виду — ABox, а разом вони складають так звану базу знань або онтологію . Численні онтології побудовані і будуються у найрізніших предметних областях, таких як біоінформатика, генетика, медицина, хімія, біологія. Як тільки онтологія побудована, постає питання про те, як можна отримувати знання, які слідують з наявних в онтології знань, чи можна це робити програмно і які відповідні алгоритми. Всі ці питання вирішуються теоретично в науці «описова логіка», а практично вже реалізовано безліч програмних систем (reasoners), які і дозволяють автоматизовано виводити знання з онтологій та виконувати інші операції з онтологіями.

Синтаксис

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

Щоб сформулювати синтаксис будь-якої описової логіки, необхідно задати непусті (і зазвичай скінченні) множини символів — так званих атомарних концептів і атомарних ролей — з яких будуватимуться вирази мови даної логіки. Конкретна описова логіка характеризується набором конструкторів і індуктивного правила, за допомогою якого складові концепти даної логіки будуються з атомарних концептів і атомарних ролей, використовуючи ці конструктори.

Типовими конструкторами для побудови складових концептів є:

  • перетин (або кон'юнкція) концептів, позначається як Описова Логіка ;
  • об'єднання (або диз'юнкція) концептів, позначається як Описова Логіка ;
  • доповнення (або заперечення) концепту, позначається як Описова Логіка ;
  • Обмеження на значення ролі (або обмеження квантором загальності), позначається як Описова Логіка ;
  • Екзистенціальне обмеження (або обмеження квантором існування), позначається як Описова Логіка ;
  • Чисельні обмеження на значення ролі, наприклад: Описова Логіка , Описова Логіка , та інші.

Як бачимо, в описовій логіці кон'юнкція і диз'юнкція позначаються інакше, щоб підкреслити відмінність від інших видів логік. Існують описові логіки, в яких є також складові ролі, що будуються з простих ролей за допомогою операцій: інверсії, перетину, об'єднання, доповнення, композиції ролей, транзитивного замикання та інших.

Синтаксис логіки ALC

Описова логіка Описова Логіка  (от Attributive Language with Complement) була введена в 1991 році і є однією з базових описових логік, на основі яких будуються багато інших описових логік. Нехай задані непусті скінченні множини атомарних концептів і атомарних ролей. Тоді наслідок є індуктивним визначенням складових концептів логіки Описова Логіка  (для стислості в цьому визначенні будемо називати їх просто концептами):

  • Всякий атомарний концепт є концептом;
  • Вираження Описова Логіка  і Описова Логіка  є концептами;
  • Якщо Описова Логіка  є концепт, то його доповнення Описова Логіка  є концептом;
  • Якщо Описова Логіка  і Описова Логіка  є концепти, то їх перетин Описова Логіка  і об'єднання Описова Логіка  є концептами;
  • Якщо Описова Логіка  є концепт, а Описова Логіка  є роль, то вираження Описова Логіка  і Описова Логіка  є концептами.

Примітка. Строго кажучи, Описова Логіка  — це не одна логіка, а сімейство логік, де кожна логіка цього сімейства задається вибором конкретних множин атомарних концептів і ролей. Це аналогічно завданню сигнатури теорії першого порядку. Однак, цим розходженням зазвичай нехтують, що ми і будемо робити надалі.

Семантика

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

Формально, інтерпретація Описова Логіка  складається з непорожньої безлічі Описова Логіка  (домену) і інтерпритуючої функції, яка зіставляє кожному атомарному концепту Описова Логіка  деяка підмножина Описова Логіка , а кожній атомарної ролі Описова Логіка  — деяка підмножина Описова Логіка . Якщо пара індивідів належить інтерпретації деякої ролі Описова Логіка , тобто Описова Логіка , то говорять, що індивід Описова Логіка  є Описова Логіка -послідовником індивіда Описова Логіка .

Далі інтерпретована функція поширюється на складові концепти і ролі. Оскільки останні в кожній описовій логіці різні, то як приклад розглянемо семантику для описаної вище логіки Описова Логіка .

Семантика логіки ALC

Інтерпретуюча функція поширюється на складові концепти логіки Описова Логіка  за такими правилами:

  • Описова Логіка  інтерпретується як весь домен: Описова Логіка 
  • Описова Логіка  інтерпретується як пуста множина: Описова Логіка 
  • Доповнення концепту інтерпретується як доповнення множини: Описова Логіка 
  • Перетин концептів інтерпретується як перетин множин: Описова Логіка 
  • Об'єднання концептів інтерпретується як об'єднання множин: Описова Логіка 
  • Вираз Описова Логіка  інтерпретується як безліч тих індивідів, у яких усі Описова Логіка -послідовники належать інтерпретації концепту Описова Логіка . Формально:
      Описова Логіка 
  • Вираз Описова Логіка  інтерпретується як безліч тих індивідів, у яких є Описова Логіка -послідовник, що належить інтерпретації концептуОписова Логіка . Формально:
      Описова Логіка 

Приклад. Нехай домен інтерпретації Описова Логіка  складається з усіх людей, атомарний концепт Описова Логіка  інтерпретований як безліч людей чоловічої статі, а роль Описова Логіка  як відношення «є батько для». Тоді концепт Описова Логіка  буде інтерпретований як безліч людей, у яких всі діти чоловічої статі, а концепт Описова Логіка  — як безліч «батьків», тобто людей чоловічої статі, які мають хоча б одну дитину.

Зв'язок з модальною логікою

На перший погляд синтаксис описової логіки є незвичним для тих, хто знайомий з «традиційними» логіками (логікою висловлювань, логікою предикатів, модальною логікою та ін). Проте вже в 1991 році було помічено, що описова логіка Описова Логіка  є не що інше, як записана в інших позначеннях модальна логіка Описова Логіка , що має Описова Логіка  незалежних модальностей. А саме, якщо в Описова Логіка  є атомарні концепти Описова Логіка  і атомарні ролі Описова Логіка , то відповідність між логіками здійснюється наступним чином:

  • Атомарні концепти Описова Логіка  переходять в пропозиційні змінні Описова Логіка  модальної логіки;
  • Перетин Описова Логіка , об'єднання Описова Логіка  і доповнення Описова Логіка  концептів переходить в булеві зв'язки кон'юнкцію Описова Логіка , диз'юнкцію Описова Логіка  і заперечення Описова Логіка ;
  • Вираз Описова Логіка  переходить в Описова Логіка , а вираз Описова Логіка  переходить в Описова Логіка .

Наприклад, концепт Описова Логіка  переходить в модальну формулу Описова Логіка . При такому перетворенні будь-який складовий концепт логіки Описова Логіка  перетворюється на правильно побудовану формулу модальної логіки Описова Логіка , причому будь-яка модальна формула є перекладом деякого концепту (тим самим, це одна і та ж мова, тільки записана в двох різних системах позначень). Більш того, дане перетворення узгоджується з вищеописаною семантикою логіки Описова Логіка  з одного боку і семантикою Кріпке модальної логіки з іншого.

Цей прийом, який застосовується як до описаних двох логік, так і до різних їх розширень, дозволяє перенести в область описових логік численні відомі факти про модальні логіки, наприклад, про їх розв'язності, обчислювальні складності , розв'язувані процедури та інших важливих властивостях (скінченність моделей, деревовидність моделей і т. ін.).

Зв'язок з логікою предикатів

Багато описових логік, включаючи Описова Логіка , можна розглядати як фрагменти логіки предикатів при «природному» перекладі концептів в предикатні формули. Якщо в Описова Логіка  є атомарні концепти Описова Логіка  і атомарні ролі Описова Логіка , то для перекладу вводяться одномісні предикатні символи Описова Логіка  і двомісні предикатні символи Описова Логіка , а сам переклад задається індуктивно наступним чином:

  • Атомарні концепти Описова Логіка  переходять у формули Описова Логіка ;
  • Перетин Описова Логіка , об'єднання Описова Логіка  і доповнення Описова Логіка  концептів переходить в булеві зв'язки кон'юнкцію Описова Логіка , диз'юнкцію Описова Логіка  і заперечення Описова Логіка ;
  • Вираз Описова Логіка  переходить в Описова Логіка ;
  • Вираз Описова Логіка  переходить в Описова Логіка .

В останніх двох пунктах змінна Описова Логіка  — нова(не зустрічалася раніше), а Описова Логіка  є переклад концепту Описова Логіка  (який вже побудований за припущенням індукції).

Легко бачити, що даний переклад узгоджується з описаною вище семантикою описової логіки, тобто в будь-якій інтерпретації, якщо атомарні концепти Описова Логіка  і атомарні ролі Описова Логіка  інтерпретовані так само, як відповідні їм предикати Описова Логіка  і Описова Логіка , то і будь-який складовий концепт інтерпретується тією ж самою множиною, що і відповідна йому при перекладі предикатна формула від однієї змінної. Слід також зазначити, що не всяка формула логіки предикатів є перекладом якогось концепту; наприклад, формула Описова Логіка  не є такою.

В даному перекладі можна обійтися всього двома змінними, і таким чином описову логіку Описова Логіка (а також багато її розширень) можна розглядати як фрагменти логіки предикатів з двома змінними, яка, як відомо, розв'язувана. Цей переклад дозволяє переносити результати про можливості розв'язання, обчислювальні складності, розвязувані алгоритми і т. ін. з області логіки предикатів в область описових логік.

База знань

Концепти описових логік цікаві не стільки самі по собі, скільки як інструмент для запису знань про описувану предметну області. Ці знання поділяються на загальні знання про поняття та їх взаємозв'язки (інтенсивні знання) і знання про індивідуальні об'єкти, їх властивості та зв'язки з іншими об'єктами (екстенсивні знання). Перші більш стабільні і постійні, тоді як другі більш схильні до модифікацій.

Відповідно до цього поділу, записувані за допомогою мови описових логік знання поділяються на

  • Набір термінологічних аксіом або TBox Описова Логіка  та
  • Набір тверджень про індивідів або ABox Описова Логіка .

Сукупність аксіом і тверджень разом складають так звану базу знань Описова Логіка . Далі ми окремо розглянемо види аксіом і тверджень, з яких може складатися TBox і ABox.

Аксіоми і TBox

Аксіомою вкладеності концептів називається вираз виду Описова Логіка аксіомою еквівалентності концептів — вираз виду Описова Логіка , де Описова Логіка  і Описова Логіка  — довільні концепти. Аналогічно, аксіомою вкладеності ролей називається вираз виду Описова Логіка , а аксіомою еквівалентності ролей — вираз виду Описова Логіка , де Описова Логіка  і Описова Логіка  — довільні ролі. Тут Описова Логіка  є символ вкладеності (subsumption).

Термінологією або набором термінологічних аксіом або TBox (від англ. Terminological box) називається скінченний набір аксіом перерахованих видів. Іноді аксіоми для ролей виділяються в окремий набір і називають його ієрархією ролей або RBox. Крім перерахованих видів аксіом, в термінології можуть допускатися й інші аксіоми (наприклад, транзитивність ролей); про них піде мова нижче.

Семантика термінології визначається природним чином. Нехай дана інтерпретація Описова Логіка . Аксіома Описова Логіка виконується в інтерпретації Описова Логіка , якщо Описова Логіка ; в цьому випадку також кажуть, що Описова Логіка  є моделлю аксіоми Описова Логіка . Аналогічно для інших видів аксіом. Термінологія Описова Логіка виконується в інтерпретації Описова Логіка , а інтерпретація Описова Логіка  називається моделлю термінології Описова Логіка , якщо Описова Логіка  є моделлю всіх вхідних в Описова Логіка  аксіом.

Приклад. Наступна сукупність є термінологією (або TBox) в мові логіки Описова Логіка :

Описова Логіка  Описова Логіка  Описова Логіка  Описова Логіка  

Інтуїтивно (тобто при «природній» інтерпретації, коли концепту Описова Логіка  відповідає безліч всіх людей, ролі Описова Логіка  відповідає ставлення «має_дитину» і т. д.) ці аксіоми кажуть, що бути жінкою означає точно бути людиною і бути жіночої статі; бути матір'ю означає точно бути жінкою і мати дітей; у будь-якої людини будь-яка дитина є теж людина, кожен доктор є людиною. Перші дві аксіоми разом являють собою приклад так званої ацикличної термінології.

Твердження і ABox

Термінології дозволяють записувати загальні знання про концепції і ролі. Однак крім цього зазвичай потрібно також записати знання про конкретні індивіди: до якого класу (концептції) вони належать, якими відносинами (ролями) вони пов'язані один з одним. Це робиться в тій частині бази знань описової логіки, яка називається ABox (або набір тверджень про індивідів).

З цією метою, крім атомарних концептів і атомарних ролей, тобто імен для класів і відносин, вводиться також скінченна множина імен для індивідів. Твердження про індивідів бувають двох видів:

  • Твердження про належність індивіда Описова Логіка  концепту Описова Логіка  — записується як Описова Логіка абоОписова Логіка ;
  • Твердження про зв'язки двох індивідів Описова Логіка іОписова Логіка роллю Описова Логіка  — записується як Описова Логіка  або Описова Логіка  або Описова Логіка .

Нарешті, набором тверджень про індивідів або ABox (від англ. Assertional box) називається скінченний набір тверджень цих двох видів.

Примітка. В деяких описових логіках допускаються також твердження виду Описова Логіка  в ABox.

Щоб задати семантику ABox, необхідно розширити інтерпретацію Описова Логіка , а саме кожному імені індивіда Описова Логіка  зіставити певний елемент домену Описова Логіка . Тоді кажуть, що твердження Описова Логіка  або Описова Логіка  виконуються в інтерпретації Описова Логіка , якщо має місце Описова Логіка  або Описова Логіка , відповідно. Кажуть, що ABox виконується в інтерпретації Описова Логіка , а інтерпретація Описова Логіка  є моделлю даного ABox, якщо всі його твердження виконуються в цій інтерпретації.

Приклад. Наступна сукупність є набором тверджень про індивідів (або ABox) в мові логіки Описова Логіка :

Описова Логіка  Описова Логіка  Описова Логіка  Описова Логіка  

Тут Mary і Peter є імена індивідів. Інтуїтивно ці твердження означають, що Mary є жінкою, але не доктором, у неї є дитина жіночої статі, Peter також є дитиною Mary, причому Peter є доктором і не має дітей.

Примітка. Часто розглядаються лише інтерпретації, які задовольняють узгодженість про унікальність імен (unique name assumption[en]). Це означає, що різним іменам індивідів інтерпретація зобов'язана зіставляти різні елементи домену. Мова OWL за замовчуванням не передбачає цю угоду, проте в ній є конструкції, за допомогою яких можна явно вказати, які імена індивідів вважати рівним або різними.

Відмінність від баз даних

Крім того, що бази знань формулюються дещо іншою мовою, ніж бази даних, їх головна відмінність полягає у використанні описової логіки при логічному виводі так званого припущення про відкритість світу, тоді як в базах даних приймається припущення про замкнутість світу. Останнє означає, що якщо деяке твердження не є істинним, то воно приймається хибним. Припущення ж про відкритість світу в цьому випадку вважає таке твердження ні істинним, ні хибним. Це кардинальним чином впливає на те, які факти вважаються логічно наступними із заданої бази знань, а значить, і на саме поняття логічного слідування в описовій логіці.

Виразні описові логіки

Існують численні розширення логіки Описова Логіка  додатковими конструкторами для побудови концептів, ролей, а також додатковими видами аксіом в TBox. Є неформальна угоду про іменування отриманих при цьому логік — зазвичай шляхом додавання до імені логіки букв, що відповідають доданим в мову конструкторам. Найбільш відомими розширеннями є:

Описова Логіка  Функціональність ролей: концепти виду Описова Логіка , що означають: існує не більше одного Описова Логіка -послідовника
Описова Логіка  Обмеження кардинальності ролей: концепти виду Описова Логіка , що означають: існує не більше Описова Логіка  Описова Логіка -послідовників
Описова Логіка  Якісні обмеження кардинальності ролей: концепти виду Описова Логіка , що означають: існує не більше Описова Логіка  Описова Логіка -послідовників в Описова Логіка 
Описова Логіка  Зворотні ролі: якщо Описова Логіка  є роль, то Описова Логіка  теж є роллю, що означає звернення бінарного відношення
Описова Логіка  Номінали: якщо Описова Логіка  є ім'я індивіда, то Описова Логіка  є концепт, що означає одноелементну множину
Описова Логіка  Ієрархія ролей: у TBox допускаються аксіоми вкладеності ролей Описова Логіка 
Описова Логіка  Транзитивні ролі: в TBox допускаються аксіоми транзитивності виду Описова Логіка 
Описова Логіка  Складові аксіоми вкладеності ролей в TBox (Описова Логіка , Описова Логіка )з умовою ациклічності, де Описова Логіка  є композиція ролей
Описова Логіка    Розширення мови конкретними доменами (типами даних)

Наприклад, логіка Описова Логіка , розширена інверсними ролями, номіналами та обмеженнями кардинальності ролей, позначається як Описова Логіка .

Примітка. Буква Описова Логіка  не додається до імені логіки, а заміщає в ньому букви Описова Логіка . Так, наприклад, логіка Описова Логіка , розширена інверсними ролями (буква Описова Логіка ), якісними обмеженнями кардинальності ролей (буква Описова Логіка ), транзитивними ролями (буква Описова Логіка ) і ієрархією ролей (буква Описова Логіка ), має назву Описова Логіка . Походження всіх букв зрозуміло з англійських назв конструкторів; буква Описова Логіка  була обрана через тісний зв'язок отриманої описової логіки з модальною логікою Описова Логіка (хоча в останній буква S означає просто system, саму ж логіку Описова Логіка  виділяє серед інших модальних логік саме цифра 4).

Примітка. Якщо в описовій логіці присутні одночасно літери Описова Логіка , Описова Логіка  і або Описова Логіка  або Описова Логіка , то додаткове обмеження накладається на правило побудови концептів: в концептах виду Описова Логіка  можна використовувати ролі Описова Логіка , що мають (з точки зору аксіом RBox) транзитивні під-ролі. Якщо не накладати дані обмеження, то логіка стає нерозв'язною.

Розглядаються також описові логіки, в яких можна будувати складові ролі за допомогою операцій об'єднання, перетину, доповнення, інверсії, композиції, транзитивного замикання та інших. Крім того, досліджено описові логіки, в яких є багатомісні ролі (позначають n-арні відносини).

Логічний аналіз

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

Нехай ми зафіксували деяку описову логіку. Введемо кілька важливих понять.

  • Кажуть, що концепція Описова Логіка  даної логіки виконується в інтерпретації Описова Логіка , якщо Описова Логіка .
  • Концепт Описова Логіка  називається здійсненним, якщо існує інтерпретація, в якій він виконується.
  • Концепт Описова Логіка  вкладений в концепт Описова Логіка  (або міститься в ньому, англ. «Is subsumed by»), якщо в будь-якій інтерпретації Описова Логіка  виконується Описова Логіка .

Аналогічні поняття можна ввести щодо деякого заданого TBox Описова Логіка , обмежуючись моделями даного TBox. Наприклад, концепція Описова Логіка  називається здійсненою щодо TBox Описова Логіка , якщо існує інтерпретація, яка є моделлю цього TBox, в якій дана концепція виконується.

Коли заданий не тільки TBox Описова Логіка , а й ABox Описова Логіка , а значить є база знань Описова Логіка , то виникає ще одне поняття.

  • Індивід Описова Логіка  є прикладом концепції Описова Логіка  щодо бази знань Описова Логіка , якщо в будь-якої моделі Описова Логіка бази знань Описова Логіка  має місце Описова Логіка .

Наступні поняття формалізують ключові алгоритмічні проблеми, пов'язані з конкретною описовою логікою:

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

В логіках, що містять Описова Логіка , проблема вкладеності концепцій зводиться до здійсненності концепції. Важливе практичне значення мають нестандартні алгоритмічні проблеми, зокрема:

  • Класифікація термінології: для даної термінології (тобто TBox) побудувати таксономію або ієрархію концептів, тобто упорядкувати всі атомарні концепти стосовно вкладення (відн. даного TBox) і видали відповідну частково упорядковану множину.
  • Добування екземплярів концепції: знайти всі екземпляри заданої концепції щодо заданої бази знань.
  • Найбільш вузький концепт для індивіда: знайти найменший (по вкладенню) концепт, прикладом якого є заданий індивід щодо заданої бази знань.
  • Відповідь на запит до бази знань: видати всі набори індивідів, які задовольняють заданому запит у щодо заданої бази знань. В даний час глибоко вивчені так звані кон'юнктивні запити до баз знань описової логіки (а також їх диз'юнкції), які схожі на аналогічні запити з області баз даних. У разі ж запитів загальнішого вигляду проблема швидко набуває високу обчислювальну складність або навіть стає нерозв'язною.

Властивості описових логік

Фундаментальними характеристиками тієї чи іншої описової логіки є наступні:

  • Розв'язність: зазвичай розглядають розв'язність проблем здійсненності концепту (щодо TBox), сумісності бази знань, відповіді на кон'юнктивні запити.
  • Обчислювальна складність: вивчається обчислювальна складність зазначених вище алгоритмічних проблем щодо розміру вхідних даних (концепту, TBox, ABox). Окремо виділяють складність проблеми здійсненності концепту при фіксованому TBox, складність проблеми здійсненності бази знань або проблеми відповіді на запити при фісованому TBox і мінливому ABox (так звана складність за даними, data complexity).
  • Властивість скінченних моделей, або інакше повнота щодо скінченних моделей ( finite model property[en]): досліджується питання, чи завжди вірно, що якщо концепт виконаємо (щодо TBox), то він виконається і на деякій скінченній моделі (даного TBox). З наявності даної властивості у конкретній описовій логіці зазвичай випливає, що для даної описової логіки більш просто будується роздільна процедура, наприклад, табло-алгоритм.
  • Властивість деревовидності моделей, або інакше повнота щодо деревовидних моделей (англ. tree model property): аналогічне питання, але не по скінченних, а про «деревовидних» моделях. При цьому деревовидними тут можуть вважати що структури, злегка відрізняються від традиційного поняття дерева; наприклад, можуть допускатися петлі (ребра, що ведуть з вершини в цю ж вершину), мультіребра (кілька ребер різних «типів», що ведуть з однієї вершини в іншу), транзитивні дерева (структури, що є транзитивним замиканням звичайних дерев), а також їх комбінації. У логік, що володіють даною властивістю, зазвичай нижча обчислювальна складність, зокрема, більш просто будується дозволяє табло-алгоритм.

Дотепер отримано велику кількість результатів, що стосуються цих властивостей різних описових логік. Переважну більшість їх зібрано у вигляді інтерактивної вебсторінки: Довідка за складністю описових логік, де крім того є посилання на першоджерела отриманих результатів.

Зв'язок з мовою OWL

Мова вебонтологій OWL розробляється як мова, на якій можна формулювати і публікувати в веб так звані мережеві онтології — формально записані твердження про поняття та об'єкти деякої предметної області. Одна з вимог до таких онтологій полягає в тому, щоб наявні в них знання були «доступні» для машинної обробки, зокрема, для автоматизованого логічного виведення нових знань із уже наявних. Для цього потрібно, щоб мова, якою формулюються онтології, мала точну семантику, а відповідні логічні проблеми були розв'язані (і мали практично допустиму обчислювальну складність). Крім того, бажано, щоб така мова мала досить велику виражальну силу, придатну для формулювання на ній практично значущих фактів.

Описові логіки мають такі властивостями, і з цієї причини вони були обрані як логічні основи для мови вебонтологій OWL. Остання є мовою, що має XML-формат, тому можна сказати, що OWL є переформулюванням деяких описових логік з використанням синтаксису XML. Оскільки існує багато описових логік, що розрізняються як силою виражальності, так і обчислювальною складністю, це призвело до того, що в мови OWL є кілька варіантів.

Відповідність термінів: наявні в описовій логіці поняття концепт, роль, індивід і база знань в OWL відповідають поняттям клас, властивість , об'єкт і онтологія, відповідно.

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

  • OWL-Lite — відповідає описовій логіці Описова Логіка ;
  • OWL-DL — відповідає описовій логіці Описова Логіка ;
  • OWL-Full — не відповідає будь-якій описовій логіці, більш того, є нерозв'язною.

Ще знаходиться в стадії робочого чернетки нова версія мови OWL 1.1 покриває описову логіку Описова Логіка , що включає в себе логіку Описова Логіка , складові аксіоми вкладеності ролей в TBox (буква Описова Логіка  в назві логіки), а також аксіоми не перетинання, рефлексивності, іррефлексівності і асиметричності ролей, універсальну роль (представлену як Описова Логіка ), конструктор концепії Описова Логіка  (інтерпретується як множина елементів, що є Описова Логіка -послідовниками самих себе) і допускає затвердження Описова Логіка  в ABox.

Одночасно з цим розробляється наступна версія мови OWL 2.0, яка, крім перерахованого, дасть можливість формулювати онтології у мові, представленій в описовій логіці Описова Логіка  (перевага якої в тому, що вона має поліноміальну обчислювальну складність); додасть синтаксичні поліпшення, що дозволяють легше складати запити до баз знань і видавати відповіді на них; а також буде містити механізми для формулювання правил логічного висновку.

Машини виводу і редактори

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

  • CEL — підтримує логіку Описова Логіка , що має поліноміальну складність, написані на LISP ;
  • FaCT++ — підтримує логіку Описова Логіка , а також OWL 2.0, реалізує табло-алгоритм, написаний на C++;
  • KAON2 — підтримує логіку Описова Логіка , розширену спеціальними правилами виведення, реалізує алгоритм, заснований на резолюції, написана на Java;
  • Pellet — підтримує логіку Описова Логіка , а також OWL 1.1, реалізує табло-алгоритм, написаний на Java;
  • RacerPro — підтримує логіку Описова Логіка , реалізує табло-алгоритм, написаний на LISP.

Створено єдиний ресурс — список машин виводу описових логік, постійно підтримуваний в актуальному стані і описує основні аспекти цих та інших програмних систем, що забезпечують логічний висновок в описових логіках.

Існують також редактори онтологій, що дозволяють створювати/редагувати онтології, зберігати їх в різних форматах, деякі дозволяють підключити reasoner і з його допомогою провести логічний аналіз онтології. Одним з найбільш відомих є редактор онтологій Protege, що дозволяє працювати з онтологіями у мові OWL Full.

Див. також

Примітки

Посилання

Джерела

Tags:

Описова Логіка Загальні відомостіОписова Логіка СинтаксисОписова Логіка СемантикаОписова Логіка Звязок з модальною логікоюОписова Логіка Звязок з логікою предикатівОписова Логіка База знаньОписова Логіка Виразні описові логікиОписова Логіка Логічний аналізОписова Логіка Властивості описових логікОписова Логіка Звязок з мовою OWLОписова Логіка Машини виводу і редакториОписова Логіка Див. такожОписова Логіка ПриміткиОписова Логіка ПосиланняОписова Логіка ДжерелаОписова ЛогікаАнглійська моваЛогіка першого порядкуМодальна логікаОбчислювальна складністьПредметна областьПредставлення знань

🔥 Trending searches on Wiki Українська:

Петро БамперЛесь Подерв'янськийУкраїна на пісенному конкурсі Євробачення 2023Слобоженко Олександр ОлександровичОргазмЛюдина2023 у телебаченніМілина (фільм)Майлі СайрусMcDonald'sОщадбанкParimatchПолтаваMinecraftКабінет Міністрів України58-ма окрема мотопіхотна бригада (Україна)Герб УкраїниПутін Володимир ВолодимировичЄлизавета IДень прикордонника УкраїниСписок президентів УкраїниСправа Вагнерівців120-мм міномет 2Б11SВінстон ЧерчилльДенисенко Наталія ОлександрівнаДержавні нагороди УкраїниКонвалія звичайнаВійськова служба правопорядку УкраїниВолинська областьКіровоградська областьЧад ГерліЕнеїда (Котляревський)Величко Сергій ОлеговичПрапор РосіїЛитваНаселення ЗемліДженніфер ЛоренсВійськові звання УкраїниКучма Леонід ДаниловичШарій Анатолій АнатолійовичПортугаліяГіга Степан ПетровичМавкаВенздейТіна КарольКарпатиДрогобичЖитомирУгода про асоціацію між Україною та Європейським СоюзомБандера Степан АндрійовичКовітіді Ольга ФедорівнаБВМП-84Епіцентр КРозстріляне відродженняЧорне дзеркалоГострий мієлобластний лейкозКоростень100-та окрема бригада територіальної оборони (Україна)Марсіянин (фільм)Категорії придатності до військової службиРосійське вторгнення в Україну (з 2022)ЛюксембургБілозір Ігор ЙосиповичСлобідська УкраїнаЛукашенко Олександр ГригоровичКонституція УкраїниBMW X5Московське царствоІспаніяТхір лісовийСан-БруноМацієвський Олександр ІгоровичМалінін Олександр МиколайовичПрип'ять (місто)ТравеньСухопутні війська Збройних сил УкраїниComfy🡆 More