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:

skärningspunkt (eller konjunktion ) av begrepp, betecknad som ; $C\sqcap D$
förening (eller disjunktion ) av begrepp, betecknad som ; $C\sqcup D$
tillägg (eller negation ) av begreppet, betecknat som ; $\neg C$
begränsning av rollvärden (eller begränsning av den universella kvantifieraren), betecknad som ; $\forall RC$
existentiell begränsning (eller begränsning av den existentiella kvantifieraren), betecknad som ; $\existerar RC$
numeriska begränsningar för rollvärden, till exempel: , , och andra. $({\le}n\,R)$ $({\ge}n\,RC)$

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): $\mathcal{ALC}$ $\mathcal{ALC}$

varje atomär koncept är ett koncept;
uttryck och är begrepp; $\topp$ $\bot$
om det finns ett koncept, så är dess komplement ett koncept; $C$ $\neg C$
om det finns begrepp, så är deras skärningspunkt och förening begrepp; $C$ $D$ $C\sqcap D$ $C\sqcup D$
om det finns ett begrepp och det finns en roll, så är uttryck begrepp. $C$ $R$ $\forall RC$ $\existerar RC$

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. $\mathcal{ALC}$

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 . $\mathcal{I}$ $\Delta^\mathcal{I}$ $A$ ${A^\mathcal{I}\subseteq\Delta^\mathcal{I}}$ $R$ ${R^\mathcal{I}\subseteq\Delta^\mathcal{I}\times\Delta^\mathcal{I}}$ $R$ $(e,d)\in R^\mathcal{I}$ $d$ $R$ $e$

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 . $\mathcal{ALC}$

Till exempel, för ALC, utökas tolkningsfunktionen till de sammansatta begreppen logik enligt följande regler: $\mathcal{ALC}$

$\topp$ tolkas som hela domänen: $\top^\mathcal{I}=\Delta^\mathcal{I}$
$\bot$ tolkas som en tom uppsättning: $\bot^\mathcal{I}=\varnothing$
komplementet till konceptet tolkas som komplementet till uppsättningen: $(\neg C)^\mathcal{I}=\Delta^\mathcal{I}\setminus C^\mathcal{I}$
skärningspunkten mellan begrepp tolkas som skärningen av mängder: $(C\sqcap D)^\mathcal{I}=C^\mathcal{I}\cap D^\mathcal{I}$
föreningen av begrepp tolkas som föreningen av mängder: $(C\sqcup D)^\mathcal{I}=C^\mathcal{I}\cup D^\mathcal{I}$
uttrycket tolkas som uppsättningen av de individer där alla anhängare tillhör tolkningen av begreppet . Formellt: $\forall RC$ $R$ $C$

(\forall RC)^\mathcal{I} = \{\,e\in\Delta^\mathcal{I} \mid \forall d\in\Delta^\mathcal{I}:\ (e,d)\ i R^\mathcal{I} \Rightarrow d\in C^\mathcal{I} \,\}

uttrycket tolkas som en uppsättning av de individer som har en -följare som hör till tolkningen av begreppet . Formellt: $\existerar RC$ $R$ $C$

(\exists RC)^\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} \,\}

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. $\Delta^\mathcal{I}$ $M$ $R$ $\forall RM$ $M\sqcap\finns R.\top$

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: $\mathcal{ALC}$ $\mathbf{K}_n$ $n$ $\mathcal{ALC}$ $A_1,\ldots,A_m$ $R_1,\ldots,R_n$

atomära begrepp övergår i propositionella variabler för modal logik; $A_{i}$ $pi}$
skärning , förening och tillägg av begrepp förvandlas till booleska konnektiver konjunktion , disjunktion och negation ; $\sqcap$ $\sqcup$ $\neg$ $\landa$ $\lor$ $\neg$
uttryck går till och uttryck går till . $\forall R_j$ $\Box_j$ $\existerar R_j$ $\Diamond_j$

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. $\exists R_1.(A_1\sqcup\forall R_2.\neg A_2)$ $\Diamond_1(p_1\lor\Box_2p_2)$ $\mathcal{ALC}$ $\mathbf{K}_n$ $\mathcal{ALC}$

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: $\mathcal{ALC}$ $\mathcal{ALC}$ $A_1,\ldots,A_m$ $R_1,\ldots,R_n$ $P_1,\ldots,P_m$ $S_1,\ldots,S_n$

atombegrepp övergår i formler ; $A_{i}$ $P_{i}(x)$
skärning , förening och tillägg av begrepp förvandlas till booleska konnektiver konjunktion , disjunktion och negation ; $\sqcap$ $\sqcup$ $\neg$ $\landa$ $\lor$ $\neg$
uttryck går till ; $\forall R_j.C$ $\forall y (S_j(x,y)\Högerpil C'(y))$
uttryck går till . $\existerar R_j.C$ $\existerar y (S_j(x,y)\land C'(y))$

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). $y$ $C'$ $C$

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. $A_{i}$ ${\displaystyle R_{j))$ $Pi}$ $S_j$ $\forall x P_1(x)$

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. $\mathcal{ALC}$

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:

en uppsättning terminologiska axiom eller och $TBox{\mathcal {T}}$
en uppsättning uttalanden om individer eller . $ABox{\mathcal {A}}$

Uppsättningen av axiom och påståenden utgör tillsammans den så kallade kunskapsbasen . $\mathcal{K}=\mathcal{T}\cup\mathcal{A}$

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. $C\sqsubseteq D$ $C\equiv D$ $C$ $D$ $R\sqsubseteq S$ $R\equiv S$ $R$ $S$ $\sqsubseteq$

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. $TBox$ $RBox$

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 . $\mathcal{I}$ $C\sqsubseteq D$ $\mathcal{I}$ $C^\mathcal{I}\subseteq D^\mathcal{I}$ $\mathcal{I}$ $C\sqsubseteq D$ $\mathcal{T}$ $\mathcal{I}$ $\mathcal{I}$ $\mathcal{T}$ $\mathcal{I}$ $\mathcal{T}$

Till exempel är följande samling terminologi (eller TBox) på logikens språk : $\mathcal{ALC}$

\mathsf{Kvinna}\equiv\mathsf{Person}\sqcap\mathsf{Kvinna}

\mathsf{Mamma}\equiv\mathsf{Kvinna}\sqcap\exists\mathsf{hasChild}.\top

\forall {\mathsf {hasChild}}.{\mathsf {Person}}\sqsubseteq {\mathsf {Person}}

\mathsf{Doctor}\sqsubseteq\mathsf{Person}

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 . $\mathsf{Person}$ $\mathsf{hasChild}$

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). $ABox$

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:

uttalande om en individs tillhörighet till ett begrepp - skrivs som eller ; $a$ $C$ $C(a)$ $a\colon C$
ett uttalande om förhållandet mellan två individer och en roll - skrivs som eller eller . $a$ $b$ $R$ $R(a,b)$ $(a,b)\colon R$ $a\,R\,b$

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. $ABox$

Vissa beskrivningslogiker tillåter också uttalanden av formen i . $\neg R(a,b)$ $ABox$

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. $\mathcal{I}$ $a$ $a^\mathcal{I}\in\Delta^\mathcal{I}$ $C(a)$ $R(a,b)$ $\mathcal{I}$ $a^\mathcal{I}\in C^\mathcal{I}$ $(a^\mathcal{I},b^\mathcal{I})\in R^\mathcal{I}$ $\mathcal{I}$ $\mathcal{I}$

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

\mathsf{Mary}\colon\mathsf{Woman}\sqcap\neg\mathsf{Doctor}

\mathsf{Mary}\colon\exists\mathsf{hasChild}.\mathsf{Kvinna}

\mathsf{Mary}\,\mathsf{hasChild}\,\mathsf{Peter}

\mathsf{Peter}\colon\mathsf{Doctor}\sqcap\forall\mathsf{hasChild}.\bot

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] : $\mathcal{ALC}$ $TBox$

${\mathcal {F}}$	Rollernas funktionalitet: begrepp av formen , vilket betyder: det finns högst en -följare $({\le}1\,R)$ $R$

$\mathcal{N}$	Roll Kardinalitetsbegränsningar: Begrepp av den sorten , vilket betyder: Det finns inga fler -följare $({\le}n\,R)$ $n$ $R$

$\mathcal{Q}$	Kvalitativa begränsningar för rollernas kardinalitet: begrepp av formen , vilket betyder: det finns högst -anhängare i $({\le}n\,RC)$ $n$ $R$ $C$

$\mathcal{I}$	Omvända roller: om det finns en roll så är det också en roll, vilket betyder omkastning av en binär relation $R$ $R^{-}$

$\mathcal{O}$	Valörer: om det finns ett namn på en individ, så finns det ett begrepp som betyder en uppsättning av ett element $a$ $\{a\}$

${\mathcal {H}}$	Rollhierarki: Rollkapslingaxiom tillåtna i TBox $R\sqsubseteq S$

$\mathcal{S}$	Transitiva roller: TBox tillåter transitivitetsaxiom för formen $\mathsf{Tr}(R)$

$\mathcal{R}$	Sammansatta axiom för rollkapsling i TBox ( , ) med acyklicitetstillstånd, där det finns rollsammansättning $R\circ S\sqsubseteq R$ $R\circ S\sqsubseteq S$ $R\cirkel S$

$(D)$	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 . $\mathcal{ALC}$ $\mathcal{ALCIOQ}$

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 ). $\mathcal{S}$ $\mathcal{ALC}$ $\mathcal{ALC}$ $\mathcal{I}$ $\mathcal{Q}$ $\mathcal{S}$ ${\mathcal {H}}$ $\mathcal{SHIQ}$ $\mathcal{S}$ $\mathbf {S4}$ $\mathbf {S4}$

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] $\mathcal{S}$ ${\mathcal {H}}$ $\mathcal{Q}$ $\mathcal{N}$ $({\le}n\,RC)$ $R$

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:

konceptet med denna logik exekveras i tolkningen om ; $C$ $\mathcal{I}$ $C^\mathcal{I}\ne\varnothing$
ett begrepp kallas tillfredsställbart om det finns en tolkning där det är uppfyllt; $C$
konceptet är kapslat i konceptet (eller ingår i det; eng. subsumeras av ) om någon tolkning är sant . $C$ $D$ $\mathcal{I}$ $C^\mathcal{I}\subseteq D^\mathcal{I}$

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. $\mathcal{T}$ $C$ $\mathcal{T}$

När inte bara TBox specificeras utan även ABox , vilket betyder att det finns en kunskapsbas , uppstår ett annat koncept: $\mathcal{T}$ $\mathcal{A}$ $\mathcal{K}=\mathcal{T}\cup\mathcal{A}$

en individ är en instans av konceptet med avseende på kunskapsbasen om det finns i någon modell av kunskapsbasen . $a$ $C$ $\mathcal{K}$ $\mathcal{I}$ $\mathcal{K}$ $a^\mathcal{I}\in C^\mathcal{I}$

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

koncepttillfredsställelse: är det givna konceptet tillfredsställbart med avseende på den givna TBoxen?
kapsling av begrepp: är det sant att ett givet begrepp är kapslat i ett annat i förhållande till en given TBox?
TBox-kompatibilitet: Har en given TBox minst en modell?
kunskapsbaskompatibilitet: har det givna paret (TBox, ABox) minst en modell?

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

terminologiklassificering: för en given terminologi (dvs. TBox), bygg en taxonomi eller begreppshierarki, det vill säga ordna alla atomära begrepp med avseende på kapsling (relativt till en given TBox) och returnera motsvarande partiellt ordnade mängd ;
extrahering av begreppsinstanser: hitta alla instanser av ett givet begrepp i förhållande till en given kunskapsbas;
det smalaste begreppet för en individ: hitta det minsta (genom kapsling) begreppet, vars instans är en given individ med avseende på en given kunskapsbas;
svar på en fråga till kunskapsbasen: returnera alla uppsättningar av individer som uppfyller den givna frågan med avseende på den givna kunskapsbasen. För närvarande har de så kallade konjunktiva frågorna till kunskapsbaser för beskrivningslogiker (såväl som deras disjunktioner), som liknar liknande frågor från området databaser , studerats djupt ; i fallet med frågor av mer allmän form får problemet snabbt hög beräkningskomplexitet eller blir till och med olösligt [10] [11] .

Egenskaper

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

lösbarhet : överväg vanligtvis lösbarheten av problem med konceptets genomförbarhet (med avseende på TBox), kunskapsbaskompatibilitet, svar på konjunktiva frågor;
beräkningskomplexitet : beräkningskomplexiteten hos ovanstående algoritmiska problem med avseende på storleken på indata (koncept, TBox, ABox) studeras. Separat pekas ut komplexiteten i konceptets genomförbarhetsproblem med en fast TBox, komplexiteten i kunskapsbasens genomförbarhetsproblem eller problemet med att svara på förfrågningar med en fast TBox och en föränderlig ABox (den så kallade datakomplexiteten ) .
modellfiniteness egenskap (fullständighet med avseende på finita modeller): frågan undersöks om det alltid är sant att om ett koncept är genomförbart (med avseende på TBox), så är det också genomförbart på någon finit modell (given TBox) ; av närvaron av denna egenskap i en viss logik, följer det vanligtvis att det är lättare att bygga en lösningsprocedur för den, till exempel en resultattavlaalgoritm ;
trädmodellegenskap (fullständighet med avseende på trädmodeller, eng. trädmodellegenskap ): en liknande fråga, men inte om finita, utan om "träd"-modeller, medan strukturer som skiljer sig något från det traditionella konceptet med ett träd kan övervägas trädliknande här ; till exempel slingor (kanter som leder från en vertex till samma vertex), flerkanter (flera kanter av olika "typer" som leder från en vertex till en annan), transitiva träd (strukturer som är den transitiva stängningen av vanliga träd), som samt deras kombinationer kan tillåtas; logik med denna egenskap har vanligtvis lägre beräkningskomplexitet, i synnerhet är algoritmen för upplösning av resultattavlan enklare byggd .

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:

OWL-Lite - motsvarar beskrivningslogiken ; $\mathcal{SHIF}(D)$
OWL-DL - motsvarar beskrivningslogiken ; $\mathcal{SHOIN}(D)$
OWL-Full - motsvarar inte någon beskrivande logik, är dessutom oavgörbar.

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] . $s\mathcal{ROIQ}(D)$ $\mathcal{SHOIQ}(D)$ $\mathcal{R}$ $\Delta^\mathcal{I}\times\Delta^\mathcal{I}$ $\exists R.\mathsf{Själv}$ $R$ $\neg R(a,b)$

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] . $\mathcal{EL}$

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] :

CEL - stöder logik som har polynom komplexitet, skriven i Lisp [16] ; $\mathcal{EL}+$
FaCT++ - stöder logik , såväl som OWL 2.0, implementerar en resultattavlaalgoritm, skriven i C++ [17] ; $s\mathcal{ROIQ}(D)$
Kaon2 - stöder logik utökad med speciella slutledningsregler, implementerar upplösningsbaserad algoritm, skriven i Java [18] ; $\mathcal{SHIQ}$
Pellet - stöder logik , såväl som OWL 1.1, implementerar en resultattavlaalgoritm, skriven i Java [19] ; $s\mathcal{ROIQ}(D)$
RacerPro - stöder logik , implementerar en resultattavlaalgoritm, skriven i Lisp [20] . $\mathcal{SHIQ}(D)$

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

↑ 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. (obestämd)
↑ Russell, Norvig, 2006 , sid. 482.
↑ Description Logic Handbook, 2003 , Basic Description Logics, pp. 43-95.
↑ 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 .
↑ Schmidt-Schauß, M.; Smolka, G. Attributiva begreppsbeskrivningar med komplement (neopr.) // Artificiell intelligens. - 1991. - T. 48 . - S. 1-26 .
↑ 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 .
↑ 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.
↑ 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 . .
↑ 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 .
↑ Tessaris, S. Frågor och svar: Resonemang och förfrågningar i Description Logic (PhD Thesis ) . — University of Manchester, 2001.
↑ 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 .
↑ Beskrivning Logic Complexity Navigator
↑ OWL 1.1 utvecklarwebbplats . Hämtad 17 juni 2009. Arkiverad från originalet 16 februari 2008. (obestämd)
↑ Nya funktioner i OWL 2.0 . Hämtad 17 juni 2009. Arkiverad från originalet 26 juni 2009. (obestämd)
↑ lista över DL-utgångsmaskiner . Hämtad 4 maj 2017. Arkiverad från originalet 27 oktober 2015. (obestämd)
↑ C.E.L. _ Hämtad 17 juni 2009. Arkiverad från originalet 1 september 2009. (obestämd)
↑ FaCT++ . Hämtad 17 juni 2009. Arkiverad från originalet 6 juni 2009. (obestämd)
↑ Kaon2 . Hämtad 17 juni 2009. Arkiverad från originalet 6 januari 2006. (obestämd)
↑ Pellets
↑ RacerPro . Hämtad 17 juni 2009. Arkiverad från originalet 7 juni 2009. (obestämd)

Litteratur

Russell S., Norvig P. Artificiell intelligens: ett modernt tillvägagångssätt. - M . : Publishing House "Williams", 2006. - 1408 sid. — ISBN 5-8459-0887-6 .
Franz Baader och Diego Calvanese och eborah L. McGuinness och Daniele Nardi och Peter F. Patel-Schneider. Beskrivningslogikhandboken: teori, implementering och tillämpningar . - Cambridge University Press, 2003. - ISBN 0-521-78176-0 .

Länkar

Ordböcker och uppslagsverk	stor kines

semantisk webb
Grunderna	World Wide Web Internet Hypertext Databas Semantiska nätverk Ontologier Beskrivningslogik
Underavsnitt	Länkad data datawebb Hyperdata Server för exekvering av affärsregel Datautrymmen
Ansökningar	Semantisk Wiki Semantisk publicering Semantisk sökning Semantisk beräkning semantisk reklam Semantisk resonemangsmekanism semantisk matchning semantisk kartläggare semantisk mäklare semantisk analys semantisk tjänsteorienterad arkitektur
Relaterade ämnen	Folksonomi Bibliotek 2.0 Webb 2.0 Länkar Informationsarkitektur Kunskapshantering kollektiv intelligens Tematiska kartor Att göra tankekartor metadata Geotaggning webbvetenskap
Standarder	Syntax : RDF RDF/XML Notation 3 Sköldpadda N-trippel JSON-LD SPARQL URI http XML Schema, ontologier : RDFS UGGLA Regelutbytesformat Semantisk webbregelspråk gemensam logik Schema.org Semantisk anteckning : RDFa eRDF GRDDL Mikroformat Mikrodata Ordböcker : DOAP FOAF SIOC Dublins kärna SKOS FLOCK Historik : Vanlig gammal semantisk HTML DAML+OLJA

Logik

Filosofi • Semantik • Syntax • Historia

Logiska grupper

klassisk logik	Aristotelisk logik propositionell logik Första beställningslogik Andra ordningens logik högre ordningslogik
matematisk logik	mängdteori Modellteori Beräkningsbarhetsteori Bevisteori och konstruktiv matematik Linjär logik formellt system naturlig slutsats Sekvenskalkyl Algebra av logik Relevant logik Deontisk logik intuitionistisk logik Lambek kalkyl
Icke-klassisk logik	intuitionism rolig logik Substrukturell logik logik Beskrivningslogik Flervärdig logik Logisk syntes Bindande logik Temporal logik Modal logik ( Hybrid logik ) epistemisk logik
Filosofisk logik	Kritiskt tänkande informell logik deduktiva resonemang

Komponenter

Bortförande (logik)
Sannolikhet
påstående
Avdrag / Induktion / Traduktion
Verklighet
induktivt resonemang
slutledning
boolesk konstant
Sann
logiskt följa
Logisk form
Nödvändiga och tillräckliga förutsättningar
Beskrivning
Definition
Utbyte
Paket
Kontrovers ( Antinomy )
Syntetisk bedömning / Analytisk bedömning
Länk

Lista över booleska symboler