Beskrivningslogik

Beskrivningslogik [1] ( deskriptiv logik [2] , tidiga namn - terminologiskt system , begreppslogik ) är ett kunskapsrepresentationsspråk som låter dig beskriva ämnesområdets begrepp i en entydig, formaliserad form, organiserad efter typen av matematisk logiks språk . Beskrivningslogik kombinerar å ena sidan rika uttrycksmöjligheter, och å andra sidan goda beräkningsegenskaper, såsom avgörbarhet och relativt låg beräkningskomplexitet .grundläggande logiska problem, vilket gör deras tillämpning möjlig i praktiken, vilket ger en kompromiss mellan uttrycksfullhet och avgörbarhet. De kan betraktas som avgörbara fragment av predikatlogik , men syntaktiskt ligger de nära modal logik .

Familjen fick sitt moderna namn på 1980-talet, samtidigt som de studerades som förlängningar av teorierna om ramstrukturer och semantiska nätverk med mekanismer för formell logik. På 2000-talet användes beskrivningslogiker inom ramen för begreppet den semantiska webben , där de föreslogs användas i konstruktionen av ontologier . OWL-DL- och OWL-Lite- fragmenten av OWL -webontologispråket är också baserade på beskrivningslogik .

Allmän information

Beskrivningslogik fungerar med begreppen "koncept" och "roll", vilket i andra delar av matematisk logik motsvarar begreppen "enplatspredikat" (eller mängd, klass) och "tvåställspredikat" (eller binär relation) . Intuitivt används begrepp för att beskriva klasser av vissa objekt, såsom "Människor", "Kvinnor", "Maskiner". Roller används för att beskriva två-plats-relationer mellan objekt, till exempel på en uppsättning personer finns det en två-plats-relation "X is_a_parent_of_Y", och mellan människor och maskiner finns det en två-plats-relation "X owns_Y", där godtyckliga objekt kan ersätta X och Y. Med hjälp av den beskrivande logikens språk kan man formulera allmänna påståenden om klasser i allmänhet (varje kvinna är en man, varje maskin ägs_av högst en man) och särskilda påståenden om specifika föremål (Maria är en kvinna, Ivan äger en maskin1).

En uppsättning påståenden av allmän form eller terminologi ( engelsk  terminologi ) kallas TBox, en uppsättning påståenden ( engelska  assertions ) av en viss typ är ABox och tillsammans utgör de den så kallade kunskapsbasen [3] eller ontologi . Många ontologier har byggts och byggs inom en mängd olika ämnesområden som bioinformatik , genetik , medicin , kemi , biologi . När ontologin väl är uppbyggd uppstår frågan om hur man extraherar kunskapen som följer av kunskapen som finns i ontologin, om detta kan göras programmatiskt och vilka är lämpliga algoritmer. Alla dessa frågor löses teoretiskt inom vetenskapen om "beskrivningslogik", och i praktiken har många mjukvarusystem redan implementerats - resonemangsmekanismer ( eng.  reasoners ), som gör att du automatiskt kan hämta kunskap från ontologier och utföra andra operationer med ontologier.

Syntax

I matematisk logik kännetecknas varje språk av sin syntax , det vill säga reglerna för att konstruera uttryck för detta språk, och semantik , det vill säga hur dessa uttryck tilldelas en viss formell betydelse , till exempel genom att ange vilka uttryck som anses vara sanna och falskt.

För att formulera syntaxen för någon beskrivande logik är det nödvändigt att specificera icke-tomma (och vanligtvis ändliga) uppsättningar av symboler - de så kallade atomkoncepten och atomrollerna - från vilka uttrycken för denna logiks språk kommer att byggas. En konkret logik kännetecknas av en uppsättning konstruktörer och en induktiv regel genom vilken de sammansatta begreppen för den givna logiken byggs upp från atomkoncept och atomroller med hjälp av dessa konstruktörer.

Typiska konstruktörer för att konstruera sammansatta koncept är:

Konjunktion och disjunktion i beskrivande logik betecknas vanligtvis annorlunda för att betona skillnaden från andra typer av logiker. Det finns beskrivningslogiker där det också finns sammansatta roller byggda från enkla roller med hjälp av operationer: inversion, korsning, förening, addition, rollsammansättning, transitiv stängning och andra [4] .

ALC

Beskrivningslogik (från engelska attributiva språket med komplement ) utvecklades 1991 [5] och är ett av de grundläggande systemen som bygger på många andra beskrivningslogiker. Låt icke-tomma ändliga uppsättningar av atombegrepp och atomroller ges. Sedan är följande en induktiv definition av de sammansatta begreppen logik (begrepp):  

Strängt taget är  detta inte en logik, utan en familj av logiker, där varje logik i denna familj specificeras av valet av specifika uppsättningar av atomära begrepp och roller. Detta är analogt med att sätta signaturen för en första ordningens teori. Denna distinktion försummas dock vanligtvis.

Semantik

Beskrivningslogikens semantik ges genom att tolka dess atomkoncept som uppsättningar av objekt ("individer") valda från någon fast uppsättning ("domän") och atomroller som uppsättningar av par av individer, det vill säga binära relationer på domänen .

Formellt består en tolkning av en icke-tom uppsättning (domän) och en tolkningsfunktion som mappar till varje atomär begrepp en delmängd av , och varje atomroll  till en delmängd av . Om ett par individer tillhör tolkningen av någon roll , d.v.s. , då sägs individen vara individens efterföljare .

Vidare sträcker sig tolkningsfunktionen till sammansatta begrepp och roller. Eftersom de senare är olika i varje DL, betrakta som ett exempel semantiken för logiken som beskrivs ovan .

Till exempel, för ALC, utökas tolkningsfunktionen till de sammansatta begreppen logik enligt följande regler:

Exempel: om tolkningsdomänen består av alla människor, tolkas atombegreppet som en uppsättning manliga människor, och rollen som relation "är en förälder för". Då kommer begreppet att tolkas som en uppsättning människor som har alla manliga barn, och begreppet  som en uppsättning "fäder", det vill säga manliga människor som har minst ett barn.

Förhållande med modal logik

År 1991 [6] noterades att logik inte är något annat än modal logik skriven i annan notation och med oberoende modaliteter. Nämligen, om det finns atomära begrepp och atomroller i , utförs överensstämmelsen mellan logik enligt följande:

Till exempel går ett koncept in i en modal formel . Med en sådan transformation förvandlas vilket sammansatt begrepp av logik som helst till en välformad formel för modal logik , och vilken modal formel som helst är en översättning av något begrepp (det är alltså samma språk, bara skrivet i två olika notationssystem). Dessutom överensstämmer denna transformation med den ovan beskrivna logikens semantik å ena sidan och Kripkes semantik av modal logik å den andra.

Denna teknik, applicerad både på de två beskrivna logikerna och på deras olika utvidgningar, tillåter oss att överföra många kända fakta om modal logik till området för beskrivningslogik, till exempel om deras avgörbarhet , beräkningskomplexitet , upplösningsprocedurer och andra viktiga egenskaper. (modellernas ändlighet, trädlikhetsmodeller etc.).

Relation till predikatlogik

Många beskrivande logiker, inklusive , kan betraktas som fragment av predikats logik i den "naturliga" översättningen av begrepp till predikatsformler. Om det finns atomkoncept och atomroller , introduceras en-plats-predikatsymboler och två -plats-predikatsymboler för översättning , och själva översättningen ges induktivt enligt följande:

I de två sista styckena är variabeln  färsk (ej påträffad tidigare), men är en översättning av begreppet (som redan har byggts enligt induktionsantagandet).

En sådan översättning är förenlig med den beskrivande logikens semantik, det vill säga i vilken tolkning som helst, om atombegrepp och atomroller tolkas på samma sätt som motsvarande predikat och , då tolkas vilket sammansatt begrepp som helst av samma uppsättning som motsvarande predikatformel från en variabel. Det bör också noteras att inte varje formel för predikatlogik är en översättning av något begrepp; formeln är till exempel inte det.

Denna översättning kan klara sig med bara två variabler [7] och kan därför (liksom många av dess förlängningar) ses som fragment av en tvåvariabel predikatlogik som är känd för att kunna avgöras [8] . Denna översättning tillåter oss att överföra resultat om lösbarhet, beräkningskomplexitet, upplösningsalgoritmer etc. från domänen för predikatlogik till domänen för beskrivningslogik.

Kunskapsbas

Begreppen beskrivningslogik är intressanta inte så mycket i sig, utan som ett verktyg för att registrera kunskap om det beskrivna ämnesområdet . Denna kunskap är uppdelad i allmän kunskap om begrepp och deras relationer ( intensionell kunskap) och kunskap om enskilda objekt, deras egenskaper och relationer med andra objekt ( extensionell kunskap). De förra är mer stabila och permanenta, medan de senare är mer föremål för modifiering.

I enlighet med denna uppdelning delas kunskap som registrerats med hjälp av beskrivningslogikens språk in i:

Uppsättningen av axiom och påståenden utgör tillsammans den så kallade kunskapsbasen .

Terminologiska axiom

Begreppet häckande axiom är ett uttryck för formen , och begreppet ekvivalensaxiom  är ett uttryck för formen , där och  är godtyckliga begrepp. På liknande sätt är rollkapslingsaxiomet ett uttryck för formen och rollekvivalensaxiomet  är ett uttryck för formen där och  är godtyckliga roller. Det finns en häckningssymbol här.

En terminologi eller en uppsättning terminologiska axiom är en ändlig uppsättning axiom av de listade typerna. Ibland är axiomen för roller separerade i en separat uppsättning och kallas rollhierarkin eller . Förutom de listade typerna av axiom kan andra axiom (till exempel transitivitet av roller) tillåtas i terminologin.

Terminologins semantik bestäms på ett naturligt sätt. Låt en tolkning ges . Axiomet är uppfyllt i tolkningen om ; i detta fall sägs också vara en axiommodell . På samma sätt för andra typer av axiom. Terminologin utförs i tolkningen , och tolkningen kallas terminologimodellen om den är en modell av alla ingående axiom .

Till exempel är följande samling terminologi (eller TBox) på logikens språk :

Intuitivt (det vill säga under den "naturliga" tolkningen, när begreppet motsvarar mängden av alla människor, rollen motsvarar förhållandet "har_ett barn", etc.), säger dessa axiom att att vara kvinna betyder exakt att vara människa och att vara kvinna; att vara mamma betyder precis att vara kvinna och få ett barn; för varje person är varje barn också en person; varje läkare är människa. De två första axiomen ger tillsammans ett exempel på den så kallade acykliska terminologin .

Uttalanden om individer

Terminologier låter dig registrera allmän kunskap om begrepp och roller. Men utöver detta krävs det oftast också att man registrerar kunskap om specifika individer: vilken klass (begrepp) de tillhör, vilka relationer (roller) de är förknippade med varandra. Detta görs i den del av DL-kunskapsbasen som kallas (eller en uppsättning påståenden om individer).

För detta ändamål introduceras förutom atombegrepp och atomroller, det vill säga namn på klasser och relationer, även en ändlig uppsättning namn för individer. Påståenden om individer är av två typer:

Slutligen, en uppsättning påståenden om individer eller (från den engelska påstående rutan ) är den sista uppsättningen påståenden av dessa två typer.  

Vissa beskrivningslogiker tillåter också uttalanden av formen i .

För att specificera semantiken för ABox är det nödvändigt att utöka tolkningen av , nämligen till varje enskilt namn, för att associera något element i domänen . Då påståendet eller sägs vara uppfyllt i tolkningen om eller sker . En ABox sägs utföras i en tolkning , och en tolkning är en modell av denna ABox om alla dess uttalanden är uppfyllda i den tolkningen.

Till exempel är följande samling en uppsättning uttalanden om individer (eller ABox) på logikens språk :

Här är Maria och Peter namnen på individer. Intuitivt betyder dessa uttalanden att Maria är en kvinna, men inte en läkare, hon har ett kvinnligt barn, Peter är också Marias barn, och Peter är läkare och har inga barn.

Ofta övervägs endast tolkningar som uppfyller unika konventionen för namn . Det innebär att tolkningen måste associera olika delar av domänen med olika namn på individer. OWL - språket har inte denna konvention som standard, men det har konstruktioner som låter dig explicit specificera vilka individuella namn som är lika eller olika.

Skillnad från databaser

Förutom att kunskapsbaser är formulerade på ett lite annorlunda språk än databaser ligger deras huvudsakliga skillnad i användningen av det så kallade öppna världsantagandet i DL i logisk härledning , medan i databaser är världen stängd . Det senare betyder att om ett visst påstående inte är sant, så antas det vara falskt. Antagandet om världens öppenhet i detta fall anser att ett sådant uttalande varken är sant eller falskt. Detta påverkar i grunden vilka fakta som anses logiskt följa från en given kunskapsbas, och därav själva begreppet logisk konsekvens i DL.

Expressiv beskrivande logik

Det finns många utökningar av logik med ytterligare konstruktörer för att konstruera koncept, roller, såväl som ytterligare typer av axiom i . Det finns en informell namnkonvention för den resulterande logiken, vanligtvis genom att lägga till bokstäver till namnet på logiken som motsvarar konstruktörerna som lagts till i språket. De mest kända tilläggen är [4] :

Rollernas funktionalitet: begrepp av formen , vilket betyder: det finns högst en -följare
Roll Kardinalitetsbegränsningar: Begrepp av den sorten , vilket betyder: Det finns inga fler -följare
Kvalitativa begränsningar för rollernas kardinalitet: begrepp av formen , vilket betyder: det finns högst -anhängare i
Omvända roller: om det finns en roll så är det också en roll, vilket betyder omkastning av en binär relation
Valörer: om det finns ett namn på en individ, så finns det ett begrepp som betyder en uppsättning av ett element
Rollhierarki: Rollkapslingaxiom tillåtna i TBox
Transitiva roller: TBox tillåter transitivitetsaxiom för formen
Sammansatta axiom för rollkapsling i TBox ( , ) med acyklicitetstillstånd, där det finns rollsammansättning
Utöka språket med specifika domäner (datatyper)

Till exempel, logik utökad med omvända roller, valörer och rollkardinalitetsbegränsningar betecknas som .

Bokstaven läggs inte till i logikens namn, utan ersätter bokstäverna i den . Så, till exempel, logiken utökad med omvända roller (bokstav ), kvalitativa begränsningar av rollernas kardinalitet (bokstav ), transitiva roller (bokstav ) och rollhierarki (bokstav ), har namnet . Ursprunget till alla bokstäver framgår tydligt av de engelska namnen på konstruktörerna; Bokstaven valdes på grund av den nära kopplingen av den resulterande DL med modal logik [6] (även om bokstaven S i den senare betyder helt enkelt system , är det siffran 4 som skiljer själva logiken från andra modala logiker ).

Om logiken innehåller bokstäverna , och antingen eller , åläggs en ytterligare begränsning på regeln för att konstruera begrepp: i begrepp av formen kan du inte använda roller som har (ur synvinkeln av RBox-axiomen) transitiva sub- roller. Om dessa begränsningar inte införs, blir logiken oavgjord . [9]

Beskrivningslogiker beaktas också, där det är möjligt att bygga sammansatta roller med hjälp av operationerna union, korsning, addition, inversion, sammansättning, transitiv stängning och andra. Dessutom undersöks DL:er med flerplatsroller (som betecknar n-ära relationer). [fyra]

Logisk analys

Kunskapsbaser formulerade på språket för beskrivningslogik används inte bara för att representera kunskap om ämnesområdet, utan också för logisk analys ( engelska  resonemang ) av kunskap, såsom att kontrollera frånvaron av motsägelser i dem, hämta ny kunskap från befintliga, ger möjlighet att göra förfrågningar till kunskapsbaser (i analogi med frågor till databaser). På grund av att DL-kunskapsbaserna är skrivna i en formaliserad form är det möjligt att dra en strikt logisk slutsats. Och eftersom beskrivningslogikens syntax och semantik är konstruerade på ett sådant sätt att de huvudsakliga logiska problemen är lösbara, kan härledningen av ny kunskap utföras med datormedel - speciella program ( resonemang ).

Några definitioner av logisk analys:

Liknande koncept kan introduceras med avseende på vissa givna TBox , begränsade till modeller av den givna TBoxen. Till exempel sägs ett koncept vara tillfredsställande med avseende på en TBox om det finns en tolkning som är en modell av denna TBox där konceptet exekveras.

När inte bara TBox specificeras utan även ABox , vilket betyder att det finns en kunskapsbas , uppstår ett annat koncept:

Följande begrepp formaliserar de viktigaste algoritmiska problemen förknippade med en viss beskrivande logik:

I logiker som innehåller , reduceras konceptet kapslingsproblem till koncepttillfredsställelse. [4] Icke-standardiserade algoritmiska problem är av stor praktisk betydelse, särskilt:

Egenskaper

De grundläggande egenskaperna hos en viss deskriptiv logik är följande:

Ett stort antal resultat har erhållits angående dessa egenskaper hos olika beskrivningslogiker [12] .

Släktskap med OWL

Webontologispråket OWL utvecklas som ett språk där så kallade nätverksontologier kan formuleras och publiceras på webben  - formellt skrivna uttalanden om ett visst ämnesområdes begrepp och objekt. Ett av kraven för sådana ontologier är att kunskapen i dem är "tillgänglig" för maskinell bearbetning, i synnerhet för automatiserad slutledning av ny kunskap från befintliga. Detta kräver att språket som ontologierna är formulerade på har exakt semantik, och att motsvarande logiska problem är lösbara (och har praktiskt taget acceptabel beräkningskomplexitet). Dessutom är det önskvärt att ett sådant språk har en ganska stor uttryckskraft som lämpar sig för att formulera praktiskt betydelsefulla fakta i det.

Beskrivningslogiker har dessa egenskaper, och av denna anledning valdes de som den logiska grunden för webbontologispråket OWL. Det senare är ett XML -formaterat språk , så OWL kan sägas vara en omformulering av vissa DL:er med XML-syntax. Eftersom det finns många DL:er som varierar i både uttryckskraft och beräkningskomplexitet har detta lett till flera varianter i OWL.

Begreppen "koncept", "roll", "individ" och "kunskapsbas" som finns tillgängliga i beskrivningslogikerna i OWL motsvarar begreppen "klass", "egenskap", "objekt" respektive "ontologi".

Den officiella W3C- rekommendationen från den 10 februari 2004 är OWL 1.0 . Denna OWL-språkspecifikation är uppdelad i följande varianter:

Den nya versionen av OWL 1.1-språket, som är i utkaststadiet, täcker beskrivningslogiken , som inkluderar logiken , de sammansatta axiomen för kapsling av roller i TBox (bokstaven i logikens namn), samt som axiomen för osammanhängande, reflexivitet, irreflexivitet och rollasymmetri, den universella rollen (tolkad som ) , konstruktören av konceptet (tolkad som en uppsättning element som är -anhängare av sig själva) och tillåter påståenden i ABox [13] .

Samtidigt utvecklas nästa version av OWL 2.0-språket, som utöver ovanstående kommer att göra det möjligt att formulera ontologier på ett språk som motsvarar deskriptiv logik (fördelen med detta är att det har polynomberäkningar komplexitet); kommer att medföra syntaktiska förbättringar för att göra det lättare att fråga kunskapsbaser och ge svar på dem; och kommer också att innehålla mekanismer för att formulera slutledningsregler [14] .

Utdatamotorer och redigerare

Det finns många programvarusystem ( inferensmotorer ) som gör det möjligt att utföra logisk analys i beskrivningslogik (kontrollera ontologin för konsistens , bygga taxonomier, kontrollera genomförbarheten och kapsling av koncept, göra frågor till kunskapsbaser, etc.). Sådana system skiljer sig åt i de beskrivningslogiker som de stöder, i typen av aktiveringsprocedurer som implementeras i dem (till exempel resultattavlaalgoritm , upplösning etc.), i de dataformat som stöds, i det programmeringsspråk som de är implementerade i och i andra parametrar. Några välkända möjliga system [15] :

Det finns också ontologiredigerare som låter dig skapa ontologier, spara dem i olika format, vissa låter dig koppla ett resonemangsblock och  använda det för att utföra en logisk analys av ontologin. En av de mest kända är Protégé ontology editor , som låter dig arbeta med ontologier på OWL Full-språket.

Anteckningar

  1. Lapshin V. A., Ontologies in computer systems. RSDN Magazine, 4, 2009. . Datum för åtkomst: 21 oktober 2012. Arkiverad från originalet den 26 februari 2013.
  2. Russell, Norvig, 2006 , sid. 482.
  3. Description Logic Handbook, 2003 , Basic Description Logics, pp. 43-95.
  4. 1 2 3 4 Baader, F.; Calvanese, D.; McGuinness, D.L.; Nardi, D.; Patel-Schneider, PF, red. The Description Logic Handbook  (neopr.) . - New York: Cambridge University Press , 2003. - ISBN 0-521-78176-0 .
  5. Schmidt-Schauß, M.; Smolka, G. Attributiva begreppsbeskrivningar med komplement  (neopr.)  // Artificiell intelligens. - 1991. - T. 48 . - S. 1-26 .
  6. 1 2 Schild, K. En korrespondensteori för terminologisk logik: Preliminär rapport  //  In Proc. av den 12:e Int. Gemensam konf. om artificiell intelligens (IJCAI'91). : journal. - 1991. - S. 466-471 .
  7. Lutz, C.; Sattler, U.; Wolter, F. Modal logics and the two-variable fragment  (neopr.)  // In Annual Conference of the European Association for Computer Science Logic (CSL'2001). – 2001.
  8. Grädel, E.; Otto, M.; Rosen, E. Två variabla logik med räkning är avgörbar  (obestämd)  // In Proc. av det 12:e IEEE Symp. om logik i datavetenskap (LICS'97). - 1997. - S. 306-317 . .
  9. Horrocks, I.; Sattler, U.; Tobies, S. Praktiska resonemang för uttrycksfulla Beskrivningslogik  //  In Proc. av 6:e Int. Konferens om logik för programmering och automatiserat resonemang (LPAR'99): tidskrift. - 1999. - S. 161-180 .
  10. Tessaris, S. Frågor och svar: Resonemang och förfrågningar i Description Logic (PhD Thesis  ) . — University of Manchester, 2001.
  11. Glimm, B.; Horrocks, I.; Lutz, C.; Sattler, U. Konjunktiv fråga svarar för beskrivningslogiken SHIQ  //  In Proc. av den 20:e Int. Gemensam konf. om artificiell intelligens (IJCAI 2007). : journal. - 2007. - Vol. 31 . - S. 151-198 .
  12. ↑ Beskrivning Logic Complexity Navigator 
  13. OWL 1.1 utvecklarwebbplats . Hämtad 17 juni 2009. Arkiverad från originalet 16 februari 2008.
  14. Nya funktioner i OWL 2.0 . Hämtad 17 juni 2009. Arkiverad från originalet 26 juni 2009.
  15. lista över DL-utgångsmaskiner . Hämtad 4 maj 2017. Arkiverad från originalet 27 oktober 2015.
  16. C.E.L. _ Hämtad 17 juni 2009. Arkiverad från originalet 1 september 2009.
  17. FaCT++ . Hämtad 17 juni 2009. Arkiverad från originalet 6 juni 2009.
  18. Kaon2 . Hämtad 17 juni 2009. Arkiverad från originalet 6 januari 2006.
  19. Pellets
  20. RacerPro . Hämtad 17 juni 2009. Arkiverad från originalet 7 juni 2009.

Litteratur

Länkar