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

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

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

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

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

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

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

Синтаксис

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

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

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

• перетин (або кон'юнкція) концептів, позначається як ${\displaystyle C\sqcap D}$;
• об'єднання (або диз'юнкція) концептів, позначається як ${\displaystyle C\sqcup D}$;
• доповнення (або заперечення) концепту, позначається як ${\displaystyle \neg C}$;
• Обмеження на значення ролі (або обмеження квантором загальності), позначається як ${\displaystyle \forall R.C}$;
• Екзистенціальне обмеження (або обмеження квантором існування), позначається як ${\displaystyle \exists R.C}$;
• Чисельні обмеження на значення ролі, наприклад: ${\displaystyle ({\leq }n\,R)}$, ${\displaystyle ({\geq }n\,R.C)}$, та інші.

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

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

Описова логіка ${\displaystyle {\mathcal {ALC}}}$ (от Attributive Language with Complement) була введена в 1991 році^[2] і є однією з базових описових логік, на основі яких будуються багато інших описових логік. Нехай задані непусті скінченні множини атомарних концептів і атомарних ролей. Тоді наслідок є індуктивним визначенням складових концептів логіки ${\displaystyle {\mathcal {ALC}}}$ (для стислості в цьому визначенні будемо називати їх просто концептами):

• Всякий атомарний концепт є концептом;
• Вираження ${\displaystyle \top }$ і ${\displaystyle \bot }$ є концептами;
• Якщо ${\displaystyle C\,}$ є концепт, то його доповнення ${\displaystyle \neg C}$ є концептом;
• Якщо ${\displaystyle C\,}$ і ${\displaystyle D\,}$ є концепти, то їх перетин ${\displaystyle C\sqcap D}$ і об'єднання ${\displaystyle C\sqcup D}$ є концептами;
• Якщо ${\displaystyle C\,}$ є концепт, а ${\displaystyle R\,}$ є роль, то вираження ${\displaystyle \forall R.C}$ і ${\displaystyle \exists R.C}$ є концептами.

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

Семантика

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

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

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

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

Інтерпретуюча функція поширюється на складові концепти логіки ${\displaystyle {\mathcal {ALC}}}$ за такими правилами:

• ${\displaystyle \top }$ інтерпретується як весь домен: ${\displaystyle \top ^{\mathcal {I}}=\Delta ^{\mathcal {I}}}$
• ${\displaystyle \bot }$ інтерпретується як пуста множина: ${\displaystyle \bot ^{\mathcal {I}}=\varnothing }$
• Доповнення концепту інтерпретується як доповнення множини: ${\displaystyle (\neg C)^{\mathcal {I}}=\Delta ^{\mathcal {I}}\setminus C^{\mathcal {I}}}$
• Перетин концептів інтерпретується як перетин множин: ${\displaystyle (C\sqcap D)^{\mathcal {I}}=C^{\mathcal {I}}\cap D^{\mathcal {I}}}$
• Об'єднання концептів інтерпретується як об'єднання множин: ${\displaystyle (C\sqcup D)^{\mathcal {I}}=C^{\mathcal {I}}\cup D^{\mathcal {I}}}$
• Вираз ${\displaystyle \forall R.C}$ інтерпретується як безліч тих індивідів, у яких усі ${\displaystyle \,R}$-послідовники належать інтерпретації концепту ${\displaystyle \,C}$. Формально:

${\displaystyle (\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}}\,\}}$

• Вираз ${\displaystyle \exists R.C}$ інтерпретується як безліч тих індивідів, у яких є ${\displaystyle \,R}$-послідовник, що належить інтерпретації концепту${\displaystyle \,C}$. Формально:

${\displaystyle (\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}}\,\}}$

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

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

На перший погляд синтаксис описової логіки є незвичним для тих, хто знайомий з «традиційними» логіками (логікою висловлювань, логікою предикатів, модальною логікою та ін). Проте вже в 1991 році^[3] було помічено, що описова логіка ${\displaystyle {\mathcal {ALC}}}$ є не що інше, як записана в інших позначеннях модальна логіка ${\displaystyle \mathbf {K} _{n}}$, що має ${\displaystyle \,n}$ незалежних модальностей. А саме, якщо в ${\displaystyle {\mathcal {ALC}}}$ є атомарні концепти ${\displaystyle A_{1},\ldots ,A_{m}}$ і атомарні ролі ${\displaystyle R_{1},\ldots ,R_{n}}$, то відповідність між логіками здійснюється наступним чином:

• Атомарні концепти ${\displaystyle A_{i}\,}$ переходять в пропозиційні змінні ${\displaystyle p_{i}\,}$ модальної логіки;
• Перетин ${\displaystyle \sqcap }$, об'єднання ${\displaystyle \sqcup }$ і доповнення ${\displaystyle \neg }$ концептів переходить в булеві зв'язки кон'юнкцію ${\displaystyle \land }$, диз'юнкцію ${\displaystyle \lor }$ і заперечення ${\displaystyle \neg }$;
• Вираз ${\displaystyle \forall R_{j}}$ переходить в ${\displaystyle \Box _{j}}$, а вираз ${\displaystyle \exists R_{j}}$ переходить в ${\displaystyle \Diamond _{j}}$.

Наприклад, концепт ${\displaystyle \exists R_{1}.(A_{1}\sqcup \forall R_{2}.\neg A_{2})}$ переходить в модальну формулу ${\displaystyle \Diamond _{1}(p_{1}\lor \Box _{2}p_{2})}$. При такому перетворенні будь-який складовий концепт логіки ${\displaystyle {\mathcal {ALC}}}$ перетворюється на правильно побудовану формулу модальної логіки ${\displaystyle \mathbf {K} _{n}}$, причому будь-яка модальна формула є перекладом деякого концепту (тим самим, це одна і та ж мова, тільки записана в двох різних системах позначень). Більш того, дане перетворення узгоджується з вищеописаною семантикою логіки ${\displaystyle {\mathcal {ALC}}}$ з одного боку і семантикою Кріпке модальної логіки з іншого.

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

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

Багато описових логік, включаючи ${\displaystyle {\mathcal {ALC}}}$, можна розглядати як фрагменти логіки предикатів при «природному» перекладі концептів в предикатні формули. Якщо в ${\displaystyle {\mathcal {ALC}}}$ є атомарні концепти ${\displaystyle A_{1},\ldots ,A_{m}}$ і атомарні ролі ${\displaystyle R_{1},\ldots ,R_{n}}$, то для перекладу вводяться одномісні предикатні символи ${\displaystyle P_{1},\ldots ,P_{m}}$ і двомісні предикатні символи ${\displaystyle S_{1},\ldots ,S_{n}}$, а сам переклад задається індуктивно наступним чином:

• Атомарні концепти ${\displaystyle A_{i}\,}$ переходять у формули ${\displaystyle \,P_{i}(x)}$;
• Перетин ${\displaystyle \sqcap }$, об'єднання ${\displaystyle \sqcup }$ і доповнення ${\displaystyle \neg }$ концептів переходить в булеві зв'язки кон'юнкцію ${\displaystyle \land }$, диз'юнкцію ${\displaystyle \lor }$ і заперечення ${\displaystyle \neg }$;
• Вираз ${\displaystyle \forall R_{j}.C}$ переходить в ${\displaystyle \forall y(S_{j}(x,y)\Rightarrow C'(y))}$;
• Вираз ${\displaystyle \exists R_{j}.C}$ переходить в ${\displaystyle \exists y(S_{j}(x,y)\land C'(y))}$.

В останніх двох пунктах змінна ${\displaystyle \,y}$ — нова(не зустрічалася раніше), а ${\displaystyle \,C'}$ є переклад концепту ${\displaystyle \,C}$ (який вже побудований за припущенням індукції).

Легко бачити, що даний переклад узгоджується з описаною вище семантикою описової логіки, тобто в будь-якій інтерпретації, якщо атомарні концепти ${\displaystyle A_{i}\,}$ і атомарні ролі ${\displaystyle R_{j}\,}$ інтерпретовані так само, як відповідні їм предикати ${\displaystyle P_{i}\,}$ і ${\displaystyle \,S_{j}}$, то і будь-який складовий концепт інтерпретується тією ж самою множиною, що і відповідна йому при перекладі предикатна формула від однієї змінної. Слід також зазначити, що не всяка формула логіки предикатів є перекладом якогось концепту; наприклад, формула ${\displaystyle \forall xP_{1}(x)}$ не є такою.

В даному перекладі можна обійтися всього двома змінними,^[4] і таким чином описову логіку ${\displaystyle {\mathcal {ALC}}}$(а також багато її розширень) можна розглядати як фрагменти логіки предикатів з двома змінними, яка, як відомо, розв'язувана.^[5] Цей переклад дозволяє переносити результати про можливості розв'язання, обчислювальні складності, розвязувані алгоритми і т. ін. з області логіки предикатів в область описових логік.

База знань

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

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

• Набір термінологічних аксіом або TBox ${\displaystyle {\mathcal {T}}}$ та
• Набір тверджень про індивідів або ABox ${\displaystyle {\mathcal {A}}}$.

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

Аксіоми і TBox

Аксіомою вкладеності концептів називається вираз виду ${\displaystyle C\sqsubseteq D}$,а аксіомою еквівалентності концептів — вираз виду ${\displaystyle C\equiv D}$, де ${\displaystyle \,C}$ і ${\displaystyle \,D}$ — довільні концепти. Аналогічно, аксіомою вкладеності ролей називається вираз виду ${\displaystyle R\sqsubseteq S}$, а аксіомою еквівалентності ролей — вираз виду ${\displaystyle R\equiv S}$, де ${\displaystyle \,R}$ і ${\displaystyle \,S}$ — довільні ролі. Тут ${\displaystyle \sqsubseteq }$ є символ вкладеності (subsumption).

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

Семантика термінології визначається природним чином. Нехай дана інтерпретація ${\displaystyle {\mathcal {I}}}$. Аксіома ${\displaystyle C\sqsubseteq D}$виконується в інтерпретації ${\displaystyle {\mathcal {I}}}$, якщо ${\displaystyle C^{\mathcal {I}}\subseteq D^{\mathcal {I}}}$; в цьому випадку також кажуть, що ${\displaystyle {\mathcal {I}}}$ є моделлю аксіоми ${\displaystyle C\sqsubseteq D}$. Аналогічно для інших видів аксіом. Термінологія ${\displaystyle {\mathcal {T}}}$виконується в інтерпретації ${\displaystyle {\mathcal {I}}}$, а інтерпретація ${\displaystyle {\mathcal {I}}}$ називається моделлю термінології ${\displaystyle {\mathcal {T}}}$, якщо ${\displaystyle {\mathcal {I}}}$ є моделлю всіх вхідних в ${\displaystyle {\mathcal {T}}}$ аксіом.

Приклад. Наступна сукупність є термінологією (або TBox) в мові логіки ${\displaystyle {\mathcal {ALC}}}$:

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

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

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

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

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

• Твердження про належність індивіда ${\displaystyle ,\,a}$ концепту ${\displaystyle \,C}$ — записується як ${\displaystyle \,C(a)}$або${\displaystyle \,a\colon C}$;
• Твердження про зв'язки двох індивідів ${\displaystyle \,a}$і${\displaystyle \,b}$роллю ${\displaystyle \,R}$ — записується як ${\displaystyle \,R(a,b)}$ або ${\displaystyle \,(a,b)\colon R}$ або ${\displaystyle a\,R\,b}$.

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

Примітка. В деяких описових логіках допускаються також твердження виду ${\displaystyle \neg R(a,b)}$ в ABox.

Щоб задати семантику ABox, необхідно розширити інтерпретацію ${\displaystyle {\mathcal {I}}}$, а саме кожному імені індивіда ${\displaystyle \,a}$ зіставити певний елемент домену ${\displaystyle a^{\mathcal {I}}\in \Delta ^{\mathcal {I}}}$. Тоді кажуть, що твердження ${\displaystyle \,C(a)}$ або ${\displaystyle \,R(a,b)}$ виконуються в інтерпретації ${\displaystyle {\mathcal {I}}}$, якщо має місце ${\displaystyle a^{\mathcal {I}}\in C^{\mathcal {I}}}$ або ${\displaystyle (a^{\mathcal {I}},b^{\mathcal {I}})\in R^{\mathcal {I}}}$, відповідно. Кажуть, що ABox виконується в інтерпретації ${\displaystyle {\mathcal {I}}}$, а інтерпретація ${\displaystyle {\mathcal {I}}}$ є моделлю даного ABox, якщо всі його твердження виконуються в цій інтерпретації.

Приклад. Наступна сукупність є набором тверджень про індивідів (або ABox) в мові логіки ${\displaystyle {\mathcal {ALC}}}$:

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

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

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

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

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

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

Існують численні розширення логіки ${\displaystyle {\mathcal {ALC}}}$ додатковими конструкторами для побудови концептів, ролей, а також додатковими видами аксіом в TBox. Є неформальна угоду про іменування отриманих при цьому логік — зазвичай шляхом додавання до імені логіки букв, що відповідають доданим в мову конструкторам. Найбільш відомими розширеннями є:^[1]

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

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

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

Примітка. Якщо в описовій логіці присутні одночасно літери ${\displaystyle {\mathcal {S}}}$, ${\displaystyle {\mathcal {H}}}$ і або ${\displaystyle {\mathcal {Q}}}$ або ${\displaystyle {\mathcal {N}}}$, то додаткове обмеження накладається на правило побудови концептів: в концептах виду ${\displaystyle ({\leq }n\,R.C)}$ можна використовувати ролі ${\displaystyle \,R}$, що мають (з точки зору аксіом RBox) транзитивні під-ролі. Якщо не накладати дані обмеження, то логіка стає нерозв'язною.^[6]

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

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

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

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

• Кажуть, що концепція ${\displaystyle \,C}$ даної логіки виконується в інтерпретації ${\displaystyle {\mathcal {I}}}$, якщо ${\displaystyle C^{\mathcal {I}}\neq \varnothing }$.
• Концепт ${\displaystyle \,C}$ називається здійсненним, якщо існує інтерпретація, в якій він виконується.
• Концепт ${\displaystyle \,C}$ вкладений в концепт ${\displaystyle \,D}$ (або міститься в ньому, англ. «Is subsumed by»), якщо в будь-якій інтерпретації ${\displaystyle {\mathcal {I}}}$ виконується ${\displaystyle C^{\mathcal {I}}\subseteq D^{\mathcal {I}}}$.

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

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

• Індивід ${\displaystyle \,a}$ є прикладом концепції ${\displaystyle \,C}$ щодо бази знань ${\displaystyle {\mathcal {K}}}$, якщо в будь-якої моделі ${\displaystyle {\mathcal {I}}}$бази знань ${\displaystyle {\mathcal {K}}}$ має місце ${\displaystyle a^{\mathcal {I}}\in C^{\mathcal {I}}}$.

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

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

В логіках, що містять ${\displaystyle {\mathcal {ALC}}}$, проблема вкладеності концепцій зводиться до здійсненності концепції.^[1] Важливе практичне значення мають нестандартні алгоритмічні проблеми, зокрема:

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

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

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

• Розв'язність: зазвичай розглядають розв'язність проблем здійсненності концепту (щодо 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 — відповідає описовій логіці ${\displaystyle {\mathcal {SHIF}}(D)}$;
• OWL-DL — відповідає описовій логіці ${\displaystyle {\mathcal {SHOIN}}(D)}$;
• OWL-Full — не відповідає будь-якій описовій логіці, більш того, є нерозв'язною.

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

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

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

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

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

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

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

Див. також

• База знань
• Онтологія
• Мова OWL
• Семантична павутина

Примітки

1. Baader, F.; Calvanese, D.; McGuinness, D.L.; Nardi, D.; Patel-Schneider, P.F., ed. (2003). The Description Logic Handbook. New York: Cambridge University Press. ISBN ISBN 0-521-78176-0. {{cite book}}: Перевірте значення |isbn=: недійсний символ (довідка)
2. Schmidt-Schau?, M.; Smolka, G. (1991). Attributive concept descriptions with complements. Artificial Intelligence. 48 (1): 1—26.
3. 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.
4. 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).
5. Gradel, 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..
6. 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.
7. Tessaris, S. (2001). Questions and answers: Reasoning and querying in Description Logic (PhD Thesis ). University of Manchester.
8. 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.
9. Сайт розробників мови OWL 1.1. Архів оригіналу за 16 лютого 2008. Процитовано 1 квітня 2012.
10. Нові можливості мови OWL 2.0

Посилання

• Офіційний сайт спільноти дослідників описових логік логік
• Довідка з обчислювальної складності дескріпціонних логік
• Список описових логік reasoners

Джерела

• Бочаров В. А., Маркин В. И. Основы логики: Учебник. — М.: ИНФРА-М, 2001. — 296 с. — ISBN 5-16-000496-3
• Ивин А. А., Никифоров А. Л. Словарь по логике — М.: Туманит, ВЛАДОС, 1997. — 384 с. — ISBN 5-691-00099-3
• MindMap описової логіки (формат FreeMind)
• О формальных основах OWL