在證明理論中，是句法和相關邏輯的決策程序，也是一階邏輯公式的證明程序。一個分析表是為一個邏輯公式計算的樹狀結構，在每個節點上都有一個要證明或反駁的原公式的子公式。計算構建了這個樹，并使用它來證明或反駁整個公式。tableau方法也可以確定各種邏輯的有限公式集的可滿足性。

對于反駁表法來說，其目的是要證明一個公式的否定不能被滿足。從主連接詞開始，有處理每個常用連接詞的規則。在許多情況下，應用這些規則會導致副表層一分為二。定量詞被實例化了。如果一個表格的任何分支導致明顯的矛盾，該分支就會關閉。如果所有的分支都關閉了，證明就完成了，原始公式就是一個邏輯真理。盡管分析表法的基本思想來自于結構性證明理論的切割消除定理，但表法計算的起源在于邏輯連接詞的意義（或語義），因為與證明理論的聯系是在最近幾十年才建立的。更具體地說，表計算由一個有限的規則集合組成，每個規則都規定了如何將一個邏輯連接詞分解成其組成部分。這些規則通常用有限的公式集來表達，盡管有些邏輯我們必須使用更復雜的數據結構，比如多集、列表，甚至是公式樹。因此，集表示{集、多集、列表、樹}中的任何一個。如果每個邏輯連接詞都有這樣的規則，那么這個程序最終會產生一個只由原子公式和它們的否定式組成的集合，它不能再被進一步分解了。就有關邏輯的語義而言，這樣一個集合很容易被識別為可滿足或不可滿足。為了跟蹤這個過程，表本身的節點以樹的形式列出，這個樹的分支以系統的方式被創建和評估。這樣一種搜索這棵樹的系統性方法，產生了一種進行演繹和自動推理的算法。請注意，無論節點是否包含集、多集、列表或樹，都存在這棵較大的樹。

它可以用來檢查有效性或必然性：如果一個公式的否定是不可滿足的，那么它就是有效的，而公式命題表格的主要原則是試圖將復雜的公式分解成更小的公式，直到產生互補的字詞對或無法進一步擴展。該方法在一棵樹上工作，樹上的節點被標記為公式。在每一步，這棵樹都會被修改；在命題的情況下，xxx允許的修改是增加一個節點作為葉子的后代。這個過程開始于生成由集合中的所有公式組成的樹，以證明不滿足性。然后，以下程序可以非確定性地重復應用。

挑選一個開放的葉子節點。在所選節點上方的分支上挑選一個適用的節點。應用適用的節點，這相當于根據一些擴展規則擴展所選葉子節點下方的樹。對于每個新創建的節點，既是一個字面/否定字面，并且其補碼出現在同一分支的先前節點中，標記該分支為關閉。將所有其他新創建的節點標記為開放節點。最終，這個過程會終止，因為在某些時候，每個適用的節點都會被應用，而擴展規則保證樹中的每個節點都比用來創建它的適用節點更簡單。