Logik av grafer

Inom de matematiska områdena grafteori och finita modellteori handlar grafernas logik om formella specifikationer av grafegenskaper med hjälp av meningar av matematisk logik . Det finns flera variationer i de typer av logisk operation som kan användas i dessa meningar. Den första ordningens logik av grafer avser meningar där variablerna och predikaten berör enskilda hörn och kanter på en graf, medan monadisk andra ordningens graflogik tillåter kvantifiering över uppsättningar av hörn eller kanter. Logiker baserade på minst fixpunktsoperatorer tillåter mer allmänna predikat över tupel av hörn, men dessa predikat kan bara konstrueras genom fixpunktsoperatorer, vilket begränsar deras makt.

En mening $S$ kan vara sann för vissa grafer och falsk för andra; en graf $G$ sägs modellera $S$ , skriven $G\models S$ , om $S$ är sant för hörn och närliggande relation till ${ \displaystyle G}$ . Det algoritmiska problemet med modellkontroll handlar om att testa om en given graf modellerar en given mening. Det algoritmiska problemet med tillfredsställelse handlar om att testa om det finns en graf som modellerar en given mening. Även om både modellkontroll och tillfredsställelse i allmänhet är svåra, visar flera stora algoritmiska metateorem att egenskaper uttryckta på detta sätt kan testas effektivt för viktiga klasser av grafer.

Andra ämnen för forskning inom grafers logik inkluderar undersökningar av sannolikheten att en slumpmässig graf har en egenskap specificerad inom en viss typ av logik, och metoder för datakomprimering baserade på att hitta logiska meningar som är modellerade av en unik graf.

Första beställning

Grafen som visas här visas som en subgraf till en oriktad graf $G$ om och endast om $G$ modellerar meningen $\exists x_{1},x_{2},x_{3},x_{4}.$$x_{1}\sim x_{2}$$\ land$$x_{2}\sim x_{3}$$\land$$x_{3}\sim x_{1}$${\ displaystyle \land }$$x_{3}\sim x_{4}$$\land$$x_{1}\neq x_{4}$$\land$$x_{2}\neq x_{4}$ .

I första ordningens logik för grafer uttrycks en grafegenskap som en kvantifierad logisk mening vars variabler representerar grafens hörn , med predikat för likhets- och grannskapstestning.

Exempel

Till exempel kan villkoret att en graf inte har några isolerade hörn uttryckas av meningen

$$\forall u\exists v(u\sim v)$$

där $\sim$ symbolen indikerar den oriktade närliggande relationen mellan två hörn. Denna mening kan tolkas som att det för varje vertex $u$ finns en annan vertex $v$ som ligger intill $u$ .

Subgrafisomorfismproblemet för en fast subgraf $H$ frågar om $\displaystyle H}$ { visas som en subgraf till en större graf $G$ . Det kan uttryckas med en mening som anger förekomsten av hörn (en för varje hörn av $H$ ) så att för varje kant av $H$ representerar motsvarande par av variabler intilliggande hörn och sådant att för varje återstående par av hörn av $H$ representerar motsvarande par av variabler distinkta hörn; se illustrationen. Som ett specialfall klickproblemet (för en fast klickstorlek) uttryckas av en mening som anger att det finns ett antal hörn lika med klickstorleken, som alla ligger intill.

Axiom

För enkla oriktade grafer inkluderar första ordningens teori om grafer axiomen

$\forall u{\bigl (}\lnot (u\sim u){\bigr )}$ (grafen kan inte innehålla några loopar ), och

$\forall u\forall v(u\sim v\Rightarrow v\sim u)$ (kanterna är oriktade).

Andra typer av grafer, såsom riktade grafer , kan involvera olika axiom, och logiska formuleringar av multigrafegenskaper kräver speciell hantering som att ha flera kantrelationer eller separata variabler för hörn och kanter.

Noll-ett lag

Rado -grafen , en oändlig graf som modellerar exakt de första ordningens meningar som nästan alltid är sanna för ändliga grafer

Glebskiĭ et al. (1969) och, oberoende, Fagin (1976) visade en noll-ett-lag för första ordningens graflogik; Fagins bevis använde kompakthetssatsen . Enligt detta resultat är varje första ordningens mening antingen nästan alltid sann eller nästan alltid falsk för slumpmässiga grafer i Erdős–Rényi-modellen . Det vill säga låt $S$ vara en fast första ordningens mening och välj en slumpmässig $n$ -vertexgraf $G_{n}$ likformigt slumpmässigt bland alla grafer i en uppsättning av $n$ märkta hörn. Sedan i gränsen som $n$ att vara oändlig sannolikheten att $G_{n}$ modeller $S$ tenderar att antingen vara noll eller ett:

$$\lim _{n\to \infty }\operatörsnamn {Pr} [G_{n}\models S]\in \{0,1\}.$$

Dessutom finns det en specifik oändlig graf, Rado-grafen $R$ , så att meningarna som modelleras av Rado-grafen är exakt de för vilka sannolikheten att modelleras av en slumpmässig ändlig graf tenderar att vara ett:

$$R\models S\quad \Longleftrightarrow \quad \lim _{n\to \infty }\operatörsnamn {Pr} [G_{ n}\models S]=1.$$

För slumpmässiga grafer där varje kant ingår oberoende av de andra med en fast sannolikhet, är samma resultat sant, med samma meningar som har sannolikheter som tenderar mot noll eller ett.

Beräkningskomplexiteten för att avgöra om en given mening har en sannolikhet som tenderar mot noll eller till ett är hög: problemet är PSPACE-komplett . Om en grafegenskap av första ordningen har en sannolikhet som tenderar mot en på slumpmässiga grafer, så är det möjligt att lista alla de $n$ -vertexgraferna som modellerar egenskapen, med polynomfördröjning (som en funktion av $n$ ) per graf.

En liknande analys kan utföras för olikformiga slumpmässiga grafer, där sannolikheten att inkludera en kant är en funktion av antalet hörn, och där beslutet att inkludera eller exkludera en kant fattas oberoende med lika sannolikhet för alla kanter. Men för dessa grafer är situationen mer komplicerad. I detta fall kan en första ordningens egenskap ha en eller flera tröskelvärden, så att när sannolikheten för kantinkludering är avgränsad från tröskeln, tenderar sannolikheten att ha den givna egenskapen till noll eller ett. Dessa trösklar kan aldrig vara en irrationell potens av $n$ , så slumpmässiga grafer där sannolikheten för kantinkludering är en irrationell potens följer en noll-ett-lag analog med den för enhetligt slumpmässiga grafer. En liknande noll-ett-lag gäller för mycket glesa slumpmässiga grafer som har en kantinkluderingssannolikhet på $n^{-c}$ med $c>1$ , så länge som ${\ displaystyle c}$ är inte ett superpartikulärt förhållande . Om $c$ är superpartikulär, kan sannolikheten att ha en given egenskap tendera till en gräns som inte är noll eller ett, men denna gräns kan beräknas effektivt. Det finns första ordningens meningar som har oändligt många trösklar.

Parameteriserad komplexitet

Om en mening av första ordningen innehåller $k$ distinkta variabler, så kan egenskapen den beskriver testas i grafer av $n$ hörn genom att undersöka alla $k$ -tuplar av hörn; denna brute force-sökningsalgoritm är dock inte särskilt effektiv, den tar tid $O(n^{k})$ . Problemet med att kontrollera om en graf modellerar en given första ordningens mening inkluderar som specialfall subgrafisomorfismproblemet ( där meningen beskriver graferna som innehåller en fast subgraf) och klickproblemet ( där meningen beskriver grafer som innehåller kompletta subgrafer av en fast storlek). Klickproblemet är svårt för W(1) , den första nivån i en hierarki av svåra problem ur parametriserad komplexitets synvinkel . Därför är det osannolikt att ha en algoritm med fasta parametrar, en vars körtid har formen $O(f(k)n^{c})$ för en funktion $f$ och konstant $c$ som är oberoende av $k$ och $n$ . Starkare, om den exponentiella tidshypotesen är sann, skulle klicksökning och första ordningens modellkontroll nödvändigtvis ta tid proportionell mot en potens av $n$ vars exponent är proportionell mot $k$ .

På begränsade klasser av grafer kan modellkontroll av första ordningens meningar vara mycket effektivare. I synnerhet kan varje grafegenskap som kan uttryckas som en första ordningens mening testas i linjär tid för graferna för begränsad expansion . Dessa är de grafer där alla grunda moll är glesa grafer , med ett förhållande mellan kanter och hörn som begränsas av en funktion av djupet av moll. Ännu mer generellt kan första ordningens modellkontroll utföras i nästan linjär tid för grafer som inte är täta någonstans, klasser av grafer för vilka det på varje möjligt djup finns minst en förbjuden grund moll. Omvänt, om modellkontroll kan hanteras med fasta parametrar för en monoton familj av grafer, måste den familjen inte vara tät.

Datakomprimering och grafisomorfism

En första ordningens mening $S$ i grafernas logik sägs definiera en graf $G$ om $G$ är den enda grafen som modellerar $S$ . Varje graf kan definieras av minst en mening; till exempel kan man definiera vilken $n$ -vertexgraf som helst $G$ med en mening med $n+1$ variabler, en för varje vertex i grafen, och en till för att ange villkoret att det inte finns någon annan än grafens ${\displaystyle n} hörn.$ Ytterligare satser i meningen kan användas för att säkerställa att inga två vertexvariabler är lika, att varje kant av $G$ finns och att det inte finns någon kant mellan ett par icke-angränsande hörn av $G$ . Men för vissa grafer finns det betydligt kortare meningar som definierar grafen.

Flera olika grafinvarianter kan definieras från de enklaste meningarna (med olika mått på enkelhet) som definierar en given graf. Speciellt definieras det logiska djupet för en graf som miniminivån för kapsling av kvantifierare (kvantifierarrangen ) i en mening som definierar grafen. Meningen som beskrivs ovan kapar kvantifierarna för alla dess variabler, så den har logiskt djup $n+1$ . Den logiska bredden på en graf är det minsta antalet variabler i en mening som definierar den. I meningen ovan är detta antal variabler återigen $n+1$ . Både det logiska djupet och den logiska bredden kan avgränsas i termer av trädbredden för den givna grafen. Den logiska längden definieras analogt som längden på den kortaste meningen som beskriver grafen. Meningen som beskrivs ovan har en längd som är proportionell mot kvadraten på antalet hörn, men det är möjligt att definiera vilken graf som helst med en mening med längden proportionell mot dess antal kanter.

Alla träd, och de flesta grafer, kan beskrivas med första ordningens meningar med endast två variabler, men utökas genom att räkna predikat. För grafer som kan beskrivas med meningar i denna logik med ett fast konstant antal variabler är det möjligt att hitta en grafkanonisering i polynomtid (med exponenten för polynomet lika med antalet variabler). Genom att jämföra kanoniseringar är det möjligt att lösa grafisomorfismproblemet för dessa grafer i polynomtid.

Tillfredsställelse

Det är obestämbart om en given första ordningens mening kan realiseras med en ändlig oriktad graf. Det betyder att ingen algoritm kan svara korrekt på denna fråga för alla meningar.

Vissa första ordningens meningar är modellerade av oändliga grafer men inte av någon finit graf. Till exempel kan egenskapen att ha exakt en vertex av grad ett, med alla andra hörn som har grad exakt två, uttryckas med en första ordningens mening. Den är modellerad av en oändlig stråle , men bryter mot Eulers handskakningslemma för ändliga grafer. Det följer emellertid av den negativa lösningen på Entscheidungsproblemet (av Alonzo Church och Alan Turing på 1930-talet) att tillfredsställelsen av första ordningens meningar för grafer som inte är begränsade till att vara ändliga förblir obestämbar. Det är också obestämbart att skilja mellan meningarna av första ordningen som är sanna för alla grafer och de som är sanna för finita grafer men falska för vissa oändliga grafer.

Fixpunkt

Definiera en vertex $x$ som svag (markerad i rött) om, med högst ett undantag ${\displaystyle y},$ var och en av dess grannar $z$ är svag, enligt fixpunkten formel $W(x)\vänsterpil \exists y\forall z{\bigl (}x\sim z \Högerpil (y=z\vee W(z)){\bigr )}$ . De återstående blå hörnen bildar grafens två kärnor .

Minst fixpunktsbaserade logik för grafer utökar första ordningens logik för grafer genom att tillåta predikat (egenskaper för hörn eller tuplar av hörn) definierade av speciella fixpunktsoperatorer. Denna typ av definition börjar med en implikation, en formel som säger att när vissa värden i predikatet är sanna, så är andra värden också sanna. En "fast punkt" är vilket predikat som helst för vilket detta är en giltig implikation. Det kan finnas många fasta punkter, inklusive det alltid sanna predikatet; en "minst fixpunkt" är en fixpunkt som har så få sanna värden som möjligt. Mer exakt bör dess sanna värden vara en delmängd av de sanna värdena för någon annan fixpunkt.

Definiera till exempel $C(u,v)$ för att vara sant när de två hörnen $u$ och $v$ är sammankopplade med en väg i en given graf, och falskt annars. Sedan är varje vertex ansluten till sig själv, och när $u$ är ansluten till en granne till $v$ , kopplas den också med ett steg till $v$ . Om man uttrycker detta resonemang i logiska termer, $C$ den minst fixerade punkten i formeln

$$C(u,v)\leftarrow {\Bigl (}(u=v)\vee \exists w{\bigl (}C(u,w)\wedge w\sim v{\bigr )}{\ Större )}.$$

Här innebär att vara en fast punkt att sanningen på den högra sidan av formeln innebär sanningen på den vänstra sidan, som den omvända implikationspilen antyder. Att vara den minst fixerade punkten, i detta fall, innebär att inga två hörn kommer att definieras som anslutna om inte deras anslutning kommer från upprepad användning av denna implikation.

Flera varianter av fixpunktslogik har studerats. I minst fixpunktslogik måste den högra sidan av $\leftarrow$ i den definierande formeln endast använda predikatet positivt (det vill säga varje utseende ska kapslas in i ett jämnt antal negationer) för att göra den minst fasta punkten väl definierad. I en annan variant med ekvivalent logisk styrka, inflationär fixpunktslogik, behöver formeln inte vara monoton utan den resulterande fixpunkten definieras som den som erhålls genom att upprepade gånger tillämpa implikationer härledda från den definierande formeln med utgångspunkt från det helt falska predikatet. Andra varianter, som tillåter negativa implikationer eller flera samtidigt definierade predikat, är också möjliga, men ger ingen ytterligare definitionskraft. Ett predikat, definierat på ett av dessa sätt, kan sedan appliceras på en tuppel av hörn som en del av en större logisk mening.

Fixpunktslogik, och förlängningar av dessa logiker som också tillåter heltalsräkningsvariabler vars värden sträcker sig från 0 till antalet hörn, har använts i beskrivande komplexitet i ett försök att ge en logisk beskrivning av beslutsproblem inom grafteorin som kan avgöras i polynomtid . Den fasta punkten för en logisk formel kan konstrueras i polynomtid, med en algoritm som upprepade gånger lägger till tupel till den uppsättning värden för vilka predikatet är sant tills det når en fixpunkt, så att avgöra om en graf modellerar en mening i denna logik kan alltid avgöras i polynomtid. Inte varje polynomisk tidsgrafegenskap kan modelleras med en mening i en logik som bara använder fixpunkter och räkning. Men för vissa speciella klasser av grafer är polynomets tidsegenskaper desamma som egenskaperna som kan uttryckas i fixpunktslogik med räkning. Dessa inkluderar slumpmässiga grafer, intervallgrafer och (genom ett logiskt uttryck av grafstruktursatsen ) varje klass av grafer som kännetecknas av förbjudna mindretal .

Andra beställning

I den monadiska andra ordningens logik av grafer representerar variablerna objekt av upp till fyra typer: hörn, kanter, uppsättningar av hörn och uppsättningar av kanter. Det finns två huvudvarianter av monadisk andra ordningens graflogik: MSO ₁ där endast vertex- och vertexuppsättningsvariabler är tillåtna och MSO ₂ där alla fyra typer av variabler är tillåtna. Predikaten för dessa variabler inkluderar likhetstestning, medlemskapstestning och antingen vertex-kantincidens (om både vertex- och kantvariabler är tillåtna) eller närliggande mellan par av hörn (om bara vertexvariabler är tillåtna). Ytterligare variationer i definitionen tillåter ytterligare predikat såsom modulära räknepredikat.

Exempel

Som ett exempel kan anslutningen av en oriktad graf uttryckas i MSO ₁ som påståendet att det för varje partition av hörnen i två icke-tomma delmängder finns en kant från en delmängd till den andra. En partition av hörnen kan beskrivas av delmängden $S$ av hörn på ena sidan av partitionen, och varje sådan delmängd ska antingen beskriva en trivial partition (en där den ena eller andra sidan är tom) eller vara korsas av en kant. Det vill säga, en graf kopplas ihop när den modellerar MSO ₁ -satsen

$$\forall S{\Bigl (}\forall x(x\in S)\vee \forall y{\bigl (}\lnot (y\in S){\bigr )}\vee \exists x\exists y{\bigl (}x\in S\wedge \lnot (y\in S)\wedge x\sim y{\bigr )}{\Bigr )}.$$

heller uttryckas i existentiell MSO ₁ (fragmentet av MSO ₁ där alla uppsättningskvantifierare är existentiella och förekommer i början av meningen) eller ens existentiell MSO ₂ .

Hamiltonicitet kan uttryckas i MSO ₂ genom att det finns en uppsättning kanter som bildar en sammankopplad 2-reguljär graf på alla hörn, med anslutningsmöjlighet uttryckt som ovan och 2-regelbundenhet uttryckt som incidensen av två men inte tre distinkta kanter vid varje vertex. Hamiltonicitet kan dock inte uttryckas i MSO ₁ , eftersom MSO ₁ inte kan särskilja kompletta tvådelade grafer med lika många hörn på varje sida av tvådelade partitionen (som är Hamiltonska) från obalanserade kompletta tvådelade grafer (som inte är det).

Även om det inte ingår i definitionen av MSO ₂ , kan orienteringar av oriktade grafer representeras av en teknik som involverar Trémaux-träd . Detta gör att även andra grafegenskaper som involverar orienteringar kan uttryckas.

Courcelles sats

Enligt Courcelles teorem kan varje fast MSO ₂ -egenskap testas i linjär tid på grafer av begränsad trädbredd , och varje fast MSO ₁ -egenskap kan testas i linjär tid på grafer med begränsad klickbredd . Versionen av detta resultat för grafer med avgränsad trädbredd kan också implementeras i logaritmiskt utrymme . Tillämpningar av detta resultat inkluderar en handhavbar algoritm med fasta parametrar för att beräkna korsningsnumret för en graf.

Seeses sats

Tillfredsställbarhetsproblemet för en mening av monadisk andra ordningens logik är problemet med att avgöra om det finns åtminstone en graf (möjligen inom en begränsad familj av grafer) för vilken meningen är sann . För godtyckliga graffamiljer och godtyckliga meningar är detta problem oavgörbart . Emellertid är tillfredsställbarheten av MSO ₂ -meningar avgörbar för graferna för begränsad trädbredd, och tillfredsställbarheten för MSO ₁ -meningar kan avgöras för grafer med begränsad klickbredd. Beviset innebär att man använder Courcelles teorem för att bygga en automat som kan testa egenskapen, och sedan undersöka automaten för att avgöra om det finns någon graf den kan acceptera. Som en partiell omvändning bevisade Seese (1991) att närhelst en familj av grafer har ett avgörbart MSO ₂ -tillfredsställelseproblem, måste familjen ha avgränsad trädbredd. Beviset är baserat på ett teorem av Robertson och Seymour att familjerna av grafer med obegränsad trädbredd har godtyckligt stora rutnät mindre . Seese antog också att varje familj av grafer med ett avgörbart MSO ₁ -tillfredsställbarhetsproblem måste ha gränsad klickbredd. Detta har inte bevisats, men en försvagning av gissningarna som utökar MSO ₁ med modulära räknepredikat är sann.

Anteckningar

•    Bruggink, HJ Sander; König, Barbara (2018), "Recognizable languages ​​of arrows and cospans", Mathematical Structures in Computer Science , 28 (8): 1290–1332, doi : 10.1017 /S096012951800018X , MR 384296CID 38426C S771
•   Cai, Jin-Yi; Fürer, Martin; Immerman, Neil (1992), "En optimal nedre gräns för antalet variabler för grafidentifiering", Combinatorica , 12 (4): 389–410, doi : 10.1007/BF01305232 , MR 1194730
• Chen, Jianer; Huang, Xiuzhen; Kanj, Iyad A.; Xia, Ge (2006), "Strong computational lower bounds via parameterized complexity", Journal of Computer and System Sciences , 72 (8): 1346–1367, doi : 10.1016/j.jcss.2006.04.007
•    Courcelle, Bruno (1996), "Om uttrycket av grafegenskaper i vissa fragment av monadisk andra ordningens logik" (PDF) , i Immerman, Neil ; Kolaitis, Phokion G. (red.), Proc. Beskrivning Komplex. Finite Models , DIMACS, vol. 31, Amer. Matematik. Soc., s. 33–62, CiteSeerX 10.1.1.55.5184 , MR 1451381
•    Courcelle, Bruno ; Engelfriet, Joost (2012), Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach , Encyclopedia of Mathematics and its Applications, vol. 138, Cambridge University Press , ISBN 9781139644006 , Zbl 1257.68006
•   Courcelle, Bruno (2018), "Fly-automata for checking MSO ₂ graph properties", Discrete Applied Mathematics , 245 : 236–252, doi : 10.1016/j.dam.2016.10.018 , MR 3804787
•   Courcelle, Bruno ; Oum, Sang-il (2007), "Vertex-minors, monadisk andra ordningens logik och en gissning av Seese" ( PDF) , Journal of Combinatorial Theory , Series B, 97 (1): 91–126, doi : 10.1016 /j.jctb.2006.04.003 , MR 2278126
• Downey, RG ; Fellows, MR (1995), "Handbarhet och fullständighet med fasta parametrar. II. Om fullständighet för W[1]", Theoretical Computer Science , 141 (1–2): 109–131, doi : 10.1016/0304-3975(94) )00097-3
•      Dvořák, Zdeněk ; Kráľ, Daniel ; Thomas, Robin (2010), "Bestämmande första ordningens egenskaper för glesa grafer", Proc. 51st Annual IEEE Symposium on Foundations of Computer Science (FOCS 2010) , s. 133–142, CiteSeerX 10.1.1.170.9781 , doi : 10.1109/FOCS.2010.20 , ISBN 4-05-749 749 749 7 , S2CID 15264036
•   Elberfeld, Michael; Jakoby, Andreas; Tantau, Till (oktober 2010), "Logspace Versions of the Theorems of Bodlaender and Courcelle" (PDF) , Proc. 51:a årliga IEEE Symposium on Foundations of Computer Science (FOCS 2010) , s. 143–152, doi : 10.1109/FOCS.2010.21 , S2CID 1820251
•    Fagin, Ronald (1976), "Probabilities on finite models" , Journal of Symbolic Logic , 41 ( 1): 50–58, doi : 10.1017/s0022481200051756 , JSTOR 2272945 , MR 04764CID0 , S6338ID0 , S6314C  
•   Fagin, Ronald ; Stockmeyer, Larry J. ; Vardi, Moshe Y. (1995), "On monadic NP vs monadic co-NP", Information and Computation , 120 (1): 78–92, doi : 10.1006/inco.1995.1100 , MR 1340807
•   Glebskiĭ, Ju. V.; Kogan, DI; Liogon'kiĭ, MI; Talanov, VA (1969), "Volym och fraktion av tillfredsställelse av formler för den lägre predikatkalkylen", Otdelenie Matematiki, Mekhaniki i Kibernetiki Akademii Nauk Ukrainskoĭ SSR: Kibernetika (2): 17–27, MR 0300882
•    Goldberg, Leslie Ann (1993), "Polynomial space polynomial delay algorithms for listing familys of graphs", Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing (STOC '93) , New York, NY, USA: ACM, pp. . 218–225, doi : 10.1145/167088.167160 , ISBN 0-89791-591-7 , S2CID 6305108
•   Grandjean, Étienne (1983), "Complexity of the first-order theory of nästan alla finita strukturer", Information and Control , 57 (2–3): 180–204, doi : 10.1016/S0019-9958(83)80043-6 MR 0742707 _
•   Grohe, Martin (2001), "Computing crossing numbers in quadratic time", Proceedings of the Thirty-Third Annual ACM Symposium on Theory of Computing (STOC '01) , s. 231–236, arXiv : cs/0009010 , doi 1 : 4510 /380752.380805 , S2CID 724544
•    Grohe, Martin (2017), Beskrivande komplexitet, kanonisering och definierbar grafstrukturteori , Lecture Notes in Logic, vol. 47, Cambridge University Press, Cambridge, ISBN 978-1-107-01452-7 , MR 3729479
•    Grohe, Martin ; Kreutzer, Stephan; Siebertz, Sebastian (2014), "Deciding first-orders properties of nowhere dense graphs", Proceedings of the 46th Annual ACM Symposium on Theory of Computing (STOC '14) , New York: ACM, s. 89–98, arXiv : 1311.3899 , doi : 10.1145/2591796.2591851 , ISBN 978-1-4503-2710-7 , S2CID 13297133
•    Hella, Lauri; Kolaitis, Phokion G.; , "Almost everywhere equivalence of logics in finite model theory", The Bulletin of Symbolic Logic , 2 (4): 422–443, doi : 10.2307 /421173 , JSTOR 421173 , MR 6,423ID 1462C14601C1461C1460  
•     Henson, C. Ward (1972), "Countable homogeneous relational structures and $\aleph _{0}$ -categorical theories", The Journal of Symbolic Logic , 37 : 494–500, doi : 10.2307/2272734 , JSTOR 2272734 , MR 0321727 , S2CID 40662635
•   Immerman, Neil ; Lander, Eric (1990), "Describing graphs: a first-order approach to graph canonization", i Selman, Alan L. (red.), Complexity Theory Retrospective: In honor of Juris Hartmanis on the occasion of his sixtyth birthday , New York: Springer-Verlag, s. 59–81, doi : 10.1007/978-1-4612-4478-3_5 , MR 1060782
•   Lavrov, IA (1963), "Den effektiva icke-separerbarheten av uppsättningen av identiskt sanna formler och uppsättningen av ändligt vederläggbara formler för vissa elementära teorier", Algebra i Logika Sem. , 2 (1): 5-18, MR 0157904
•   Kawarabayashi, Ken-ichi ; Reed, Bruce (2007), "Computing crossing number in linear time", Proceedings of the Thirty-Ninth Annual ACM Symposium on Theory of Computing (STOC '07) , s. 382–390, doi : 10.1145/1250790.125 , S. 3100C 8100C
•     Koncewicz, Leszek (1973), "Definability of classes of graphs in the first order predicate calculus with identity", Polska vetenskapsakademin , 32 : 159–190, doi : 10.1007/BF02123839 , JSTOR 20014678 8ID 91 6 8 6 7 6 8 7 7 7 6 7 6 7 6 7 6 7 6 7 6 7 6 7 6 73 935
•    Laubner, Bastian (2010), "Capturing polynomial time on interval graphs", 25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010) , Los Alamitos, Kalifornien: IEEE Computer Society, s. 199–208, arXiv : 79911 , do 79911 . : 10.1109/LICS.2010.42 , MR 2963094 , S2CID 1450409
•     Libkin, Leonid (2004), Elements of finite model theory , Texts in Theoretical Computer Science: An EATCS Series, Springer-Verlag, Berlin, doi : 10.1007/978-3-662-07003-1 , ISBN 3-540-21202- 7 , MR 2102513 , S2CID 30176939
•   Lynch, James F. (1992), "Probabilities of sentences about very sparse random graphs", Random Structures & Algorithms , 3 (1): 33–53, doi : 10.1002/rsa.3240030105 , MR 1139487
•    Nešetřil, Jaroslav ; Ossona de Mendez, Patrice (2012), Sparsity: Graphs, Structures, and Algorithms , Algorithms and Combinatorics, vol. 28, Springer-Verlag, doi : 10.1007/978-3-642-27875-4 , ISBN 978-3-642-27874-7 , MR 2920058
•    Parys, Paweł (2014), "First-orders logic on CPDA graphs", Computer science—theory and applications , Lecture Notes in Computer Science , vol. 8476, New York: Springer-Verlag, s. 300–313, doi : 10.1007/978-3-319-06686-8_23 , MR 3218557 , S2CID 31640587
•    Pikhurko, Oleg; Spencer, Joel ; Verbitsky, Oleg (2006), "Succinct definitions in the first order theory of graphs", Annals of Pure and Applied Logic , 139 (1–3): 74–109, arXiv : math/0401307 , doi : 10.1016/j.apal .2005.04.003 , MR 2206252 , S2CID 3041191
•   Pikhurko, Oleg; Verbitsky, Oleg (2011), "Logical complexity of graphs: a survey" , i Grohe, Martin ; Makowsky, Johann A. (red.), Model Theoretic Methods in Finite Combinatorics (AMS-ASL Joint Special Session, 5-8 januari 2009, Washington, DC), Contemporary Mathematics, vol. 558, American Mathematical Society, s. 129–180, arXiv : 1003.4865 , ISBN 978-0-8218-8322-8
•   Seese, D. (1991), "The structure of the models of decidable monadic theories of graphs", Annals of Pure and Applied Logic , 53 (2): 169–195, doi : 10.1016/0168-0072(91)90054- P , MR 1114848
•    Shelah, Saharon ; Spencer, Joel (1988), "Zero-one laws for sparse random graphs", Journal of the American Mathematical Society , 1 (1): 97–115, doi : 10.2307/1990968 , JSTOR 1990968 , MR 0924703
•    Spencer, Joel (1990), "Infinite spectra in the first order theory of graphs", Combinatorica , 10 (1): 95–102, doi : 10.1007/BF02122699 , MR 1075070 , S2CID 257770500
•    Spencer, Joel (2001), The Strange Logic of Random Graphs , Algorithms and Combinatorics, vol. 22, Springer-Verlag, Berlin, doi : 10.1007/978-3-662-04538-1 , ISBN 3-540-41654-4 , MR 1847951
•   Trahtenbrot, BA (1950), "The imposibility of an algorithm for the decision problem for finita domäner", Doklady Akademii Nauk SSSR , New Series, 70 : 569–572, MR 0033784
•    Verbitsky, Oleg (2005), "The first order definability of graphs with separators via the Ehrenfeucht game", Theoretical Computer Science , 343 (1–2): 158–176, arXiv : math/0401361 , doi : 10.1016/j.tcs .2005.05.003 , MR 2168849 , S2CID 17886484
•    Verbitsky, Oleg; Zhukovskii, Maksim (2019), "Tight bounds on the asymptotic descriptive complexity of subgraph isomorphism", ACM Transactions on Computational Logic , 20 ( 2): A9:1–A9:18, arXiv : 1802.02143 , doi : 5/1310, MR 8/1310, 3/8130 , 30 . 3942556 , S2CID 3603039
•   Zeume, Thomas (2017), "The dynamic descriptive complexity of k -clique" (PDF) , Information and Computation , 256 : 9–22, doi : 10.1016 /j.ic.2017.04.005 , MR 3705411 , S12CID 1 , S12CID