圖的邏輯

在圖理論和有限模型理論的數學字段中，圖形的邏輯使用數學邏輯句子涉及圖形屬性的形式規格。這些句子中可以使用的邏輯操作類型有幾種變化。圖的一階邏輯涉及句子，其中變量和預測涉及圖的單個頂點和邊緣，而Monadic二階邏輯允許對一組頂點或邊緣進行量化。基於最小固定點運算符的邏輯允許對頂點的分組更一般的謂詞，但是這些謂詞只能通過固定點運算符構建，從而限制其功率。

句子對於某些圖，可能是正確的，而對於其他圖可能是錯誤的；圖據說是模特的 ，寫 ， 如果是對頂點和鄰接關係的正確 。模型檢查算法問題的算法問題是測試給定圖形是否模型給定句子。滿意度的算法問題涉及測試是否存在模擬給定句子的圖。儘管通常很難進行模型檢查和滿意度，但幾種主要的算法元元理論表明，以這種方式表達的屬性可以有效地測試重要的圖形類別。

圖表邏輯中的其他研究主題包括對隨機圖具有特定類型邏輯中指定屬性的概率的研究，以及基於查找由唯一圖建模的邏輯句子的數據壓縮方法。

第一個訂單

在圖的一階邏輯中，圖形屬性表示為量化的邏輯句子，其變量代表圖形頂點，具有相等性和鄰接測試的謂詞。

例子

例如，圖形沒有任何孤立頂點的條件可以由句子表達

在哪裡符號表示兩個頂點之間的無方向關係。這句話可以解釋為每個頂點的意思還有另一個頂點那與 。

固定子圖的子圖同構問題問是否作為較大圖的子圖顯示 。它可以通過一個句子來表示，該句子說明了頂點的存在（每個頂點一個 ）使得對於每個邊緣 ，相應的變量對代表相鄰的頂點，因此，對於每個其餘的對 ，相應的變量對代表不同的頂點；請參閱插圖。作為一種特殊情況，可以通過一個句子來表達集團問題（對於固定集團的大小），該句子表明存在許多等於集團大小的頂點，所有這些頂點都相鄰。

公理

對於簡單的無向圖，圖的一階理論包括公理

其他類型的圖形（例如有向圖）可能涉及不同的公理，而多編碼屬性的邏輯公理需要特殊處理，例如具有多個邊緣關係或用於頂點和邊緣的單獨變量。

零法律

Glebskiĭ等。 （1969年）和獨立的Fagin（1976）證明了一階圖邏輯的零法律； Fagin的證明使用了緊湊型定理。根據這個結果，對於ERDőS-Rényi模型中的隨機圖，每個一階句子幾乎總是真實的，或者幾乎總是假的。也就是說，讓成為固定的一階句子，然後選擇一個隨機的 -vertex圖一組的所有圖表中均勻地隨機標記的頂點。然後在極限傾向於無窮大的可能性型號將傾向於零或一個：

此外，還有一個特定的無限圖， rado圖 ，使得由RADO圖建模的句子正是由隨機有限圖建模的概率趨向於一個： 對於獨立於具有固定概率的其他邊緣的隨機圖，相同的結果是正確的，相同的句子的概率趨於零或一個。

確定給定句子是否具有零或一個概率的計算複雜性很高：問題是pspace complete 。如果一階圖屬性具有在隨機圖上的概率，則可以列出所有 - 以多項式延遲為特性建模的vertex圖（作為 ）按圖。

可以針對不均勻的隨機圖進行類似的分析，其中包括邊緣的概率是頂點數量的函數，並且決定包含或排除邊緣的函數是獨立於所有邊緣而獨立進行邊緣的。但是，對於這些圖，情況更加複雜。在這種情況下，一階屬性可能具有一個或多個閾值，因此，當邊緣包含概率遠離閾值時，具有給定屬性的概率趨於零或一個。這些閾值永遠不會成為 ，因此，邊緣包含概率是一種非理性冪的隨機圖遵守類似於統一隨機圖的零法則。相似的零法律適用於具有邊緣包含概率的非常稀疏的隨機圖和 ，只要不是超級比率。如果是超截面的，具有給定特性的概率可能趨於不零或一個極限，但是可以有效地計算此限制。存在無限多個閾值的一階句子。

參數化的複雜性

如果一階句子包括不同的變量，然後它描述的屬性可以在通過檢查所有人的頂點 - 頂點；但是，這種蠻力搜索算法並不是特別有效，花了時間 。檢查圖形是否模型是否為給定的一階句子模型包含特殊情況的子圖同構問題（其中句子描述了包含固定子圖的圖）和集團問題（其中句子描述了包含完整的圖表固定尺寸的子圖）。對於W（1）來說，集團問題很難，從參數化複雜性的角度來看，硬問題的層次結構的第一級。因此，不太可能具有固定參數可拖動算法，其運行時間為表單用於功能和恆定獨立於和 。更強烈的是，如果指數時間假設是正確的，那麼集團找到和一階模型檢查必然會與時間成比例的時間成正比指數與 。

在限制的圖表上，對一階句子的模型檢查可能會更有效。特別是，每個圖表屬性都可以在線性時間內用於有界擴展的圖表。這些圖是所有淺層未成年人都是稀疏圖的圖，其邊緣與頂點的比例是由小調深度的函數界定的。甚至更一般而言，一階模型檢查可以在近乎線性的時間內進行無處濃密的圖形，這是每個可能的深度，在每個可能的深度上，至少有一個被禁止的淺未成小調。相反，如果模型檢查是可用於任何單調圖的固定參數，則該家族必須無處濃度。

數據壓縮和圖形同構

一階句子據說在圖的邏輯中定義了圖如果是唯一模型的圖 。每個圖都可以通過至少一個句子來定義；例如，一個人可以定義任何 -vertex圖通過一個句子變量，一個圖表的每個頂點一個，另一種是說明沒有頂點以外沒有其他頂點的條件圖的頂點。該句子的其他條款可用於確保沒有兩個頂點變量相等， 存在，並且在一對的一對非標準頂點之間沒有邊緣 。但是，對於某些圖，存在明顯的句子來定義圖形。

可以從定義給定圖的最簡單句子（具有不同的簡單措施）中定義幾種不同的圖形不變性。特別地，圖的邏輯深度定義為定義圖的句子中量化器（量詞等級）嵌套的最小水平。上面概述的句子嵌套了其所有變量的量詞，因此它具有邏輯深度 。圖的邏輯寬度是定義它的句子中的最小變量數。在上面概述的句子中，這一數量的變量再次是 。邏輯深度和邏輯寬度都可以根據給定圖的樹寬範圍界定。類似地，邏輯長度定義為描述圖形的最短句子的長度。上面描述的句子的長度與頂點數量的平方成正比，但是可以通過與其邊緣數成正比的句子定義任何圖。

所有樹和大多數圖都可以通過只有兩個變量的一階句子來描述，但通過計算謂詞進行擴展。對於可以用固定常數變量數量的句子來描述的圖形，可以在多項式時間（多項式的指數等於變量的數量）中找到圖形典範。通過比較典範，可以在多項式時間內解決這些圖的圖形同構問題。

令人滿意

作為Trakhtenbrot定理的一種特殊情況，不可確定的一階句子是否可以通過有限的無向圖實現。這意味著沒有算法可以正確回答所有句子的問題。

某些一階句子是通過無限圖建模的，但不是通過任何有限圖。例如，可以通過一階句子表示，恰好具有一個精確度的頂點（所有其他具有學位二的頂點）的屬性。它是由無限射線建模的，但違反了歐拉（Euler）對有限圖的握手引理。但是，從負面解決方案到ientscheidungsproblem （由Alonzo Church和Alan Turing在1930年代），對不受限制的圖表的一階句子的滿意度仍然是不可確定的。還無法區分所有圖表的一階句子以及有限圖的真實句子，但對於某些無限圖，也是錯誤的。

固定點

圖形的最低基於固定點的邏輯通過允許由特殊固定點運算符定義的謂詞（頂點或頂點的元素）（頂點或頂點的元素的屬性）擴展圖形的一階邏輯。這種定義始於一個含義，一個公式表明，當謂詞的某些值是正確的時，其他值也是真實的。 “固定點”是任何這是有效含義的任何謂詞。可能有許多固定點，包括始終真實的謂詞； “最小固定點”是一個固定點，其真實值盡可能少。更確切地說，其真實值應該是任何其他固定點的真實值的子集。

例如，定義當兩個頂點和通過給定圖中的路徑連接，否則為錯誤。然後每個頂點都連接到自身，以及連接到鄰居 ，它也通過另外一步連接到 。用邏輯術語表達這種推理， 是公式的最小固定點

在這裡，作為一個固定點意味著公式的右側真相意味著左側的真相，正如箭頭所暗示的那樣。在這種情況下，作為最小的固定點意味著，除非其連接性來自反複使用這種含義，否則沒有兩個頂點被定義為連接。

已經研究了固定點邏輯的幾種變體。至少固定點邏輯， 定義公式中的運算符必須僅使用謂詞（即，每個外觀都嵌套在均勻數量的否定次數中）才能使最小定義的最小定義點。在具有等效邏輯功率的另一個變體中，通貨膨脹固定點邏輯，該公式不必單調，但所得的固定點被定義為通過反复應用從全率謂詞開始的定義公式得出的含義而獲得的固定點。其他變體（允許負面含義或同時定義的謂詞）也是可能的，但沒有提供額外的定義能力。然後以這些方式定義的謂詞可以作為較大邏輯句子的一部分應用於頂點元組。

固定點邏輯和這些邏輯的擴展也允許整數計數變量的值從0到頂點的數量，已用於描述性複雜性，以嘗試對圖理論中的決策問題進行邏輯描述，以確定可以決定的決策問題在多項式時間。邏輯公式的固定點可以通過多項式時間構建，該算法反復將元素添加到謂詞為真的值之前，直到達到固定點，因此確定圖形是否在此邏輯上模型可以模型，始終在多項式時間內決定。並非每個多項式時間圖屬性都可以通過僅使用固定點和計數的邏輯中的句子來建模。但是，對於某些特殊類別的圖，多項式時間屬性與在固定點邏輯中表達的屬性相同。這些包括隨機圖，間隔圖和（通過圖形定理的邏輯表達式）每個類別以禁止未成年人為特徵的圖形。

二階

在圖形的Monadic二階邏輯中，變量代表多達四種類型的對象：頂點，邊緣，一組頂點和一組邊緣。 Monadic二階邏輯有兩個主要變體：僅允許頂點和頂點集變量的MSO ₁ ，MSO ₂允許所有四種類型的變量。這些變量上的謂詞包括平等測試，成員資格測試以及頂點 - 邊緣的發生率（如果允許頂點和邊緣變量都允許）或對頂點對之間的鄰接（如果允許只有頂點變量）。定義中的其他變化允許其他謂詞，例如模塊化計數謂詞。

例子

例如，無向圖的連接可以在MSO ₁中表達為以下陳述，即對於兩個非空子集的每個分區，都存在一個從一個子集到另一個子集的邊緣。可以通過子集描述頂點的分區分區一側的頂點以及每個這樣的子集應描述一個瑣碎的分區（一個或另一側是空的），或者用邊緣越過。也就是說，當模擬MSO ₁句子時，將連接圖形

但是，連通性不能以一階圖邏輯表示，也不能以存在的MSO ₁ （MSO ₁的片段，其中所有設置的量詞都存在並且發生在句子的開頭），也無法使用MSO ₂ 。

Hamiltonicity可以通過在所有頂點上形成連接的2個規範圖的一組邊緣在MSO ₂中表達，其連通性表示為上述和2型的表達，並表示為兩個的發生率，但在每個頂點的發生率不超過兩個，但在每個角度上均不在3個不同的邊緣。頂點。但是，在MSO ₁中，漢密爾頓性不可表達，因為MSO ₁無法區分兩分之兩側（是漢密爾頓）和不平衡的完整的兩部分圖（不是）（不是）的完整兩部分圖。

儘管不是MSO ₂定義的一部分，但無向圖的方向可以通過涉及Trémaux樹的技術來表示。這也允許表達涉及方向的其他圖形屬性。

Courcelle的定理

根據Courcelle的定理，可以在有界樹寬的圖表上以線性時間測試每個固定的MSO ₂屬性，並且可以在有界集合寬度的圖表上以線性時間測試每個固定的MSO ₁屬性。也可以在對數空間中實現有界樹寬圖的結果的版本。此結果的應用包括用於計算圖形交叉數的固定參數可拖動算法。

塞斯定理

Monadic二階邏輯句子的滿足性問題是確定該句子是正確的至少存在一個圖（可能在受限的圖表中）的問題。對於任意的圖形家庭和任意句子，此問題是不可確定的。但是，MSO ₂句子的滿足性是有界樹寬圖的可決定性的，而MSO ₁句子的滿足性對於有限元寬度的圖是可決定的。證明涉及使用Courcelle的定理來構建可以測試屬性的自動機，然後檢查自動機以確定是否可以接受任何圖。作為部分匡威， Seese（Seese（Seese）（1991）證明，每當圖形家庭有可決定的MSO ₂滿意度問題時，家庭都必須具有有限的樹寬。證明是基於羅伯遜（Robertson）和西摩（Seymour）的定理，表明沒有邊際寬度的圖形家族任意較大的網格未成年人。塞斯還猜想，每個具有可確定的MSO ₁令人滿意問題的圖形家庭都必須具有有限的集團寬度。這尚未得到證明，但是延伸以模塊化計數謂詞擴展MSO ₁的猜想是正確的。