Описо́ві ло́гіки (, іноді ще їх називають дескрипційними логіками) — сімейство мов представлення знань, що дозволяють описувати поняття предметної області в недвозначному, формалізованому вигляді. Вони поєднують в собі, з одного боку, багаті виражальні можливості, а з іншого — хороші обчислювальні властивості, такі як розв'язність і відносно невисока обчислювальна складність основних логічних проблем, що робить можливим їх застосування на практиці. Таким чином, описові логіки являють собою компроміс між виражальністю і розв'язністю. Описову логіку можна розглядати як розв'язні фрагменти логіки предикатів, синтаксично ж вони близькі до модальних логік.
Свою сучасну назву описові логіки отримали в 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 (від ) називається скінченний набір аксіом перерахованих видів. Іноді аксіоми для ролей виділяються в окремий набір і називають його ієрархією ролей або RBox. Крім перерахованих видів аксіом, в термінології можуть допускатися й інші аксіоми (наприклад, транзитивність ролей); про них піде мова нижче.
Семантика термінології визначається природним чином. Нехай дана інтерпретація . Аксіома виконується в інтерпретації , якщо ; в цьому випадку також кажуть, що є моделлю аксіоми . Аналогічно для інших видів аксіом. Термінологія виконується в інтерпретації , а інтерпретація називається моделлю термінології , якщо є моделлю всіх вхідних в аксіом.
Приклад. Наступна сукупність є термінологією (або TBox) в мові логіки :