時序(Sequent)是一個表示式 
, 其中 
和 
是（可能為空的）公式序列。這裡，
被稱為前件(antecedent)，
被稱為後件(consequent)。對時序的非正式理解是，時序 
對應於 
。所有推導的初始時序是
 |
(1)
|
時序演算的推理規則分為兩類：結構規則和邏輯規則。對於每個命題連線詞和每個量詞，至少有兩個邏輯規則；其中一個應用於前件，而另一個應用於後件。結構規則包括：弱化,
 |
(2)
|
收縮,
 |
(3)
|
交換,
 |
(4)
|
和 cut 規則,
 |
(5)
|
邏輯規則由以下規則給出：合取,
 |
(6)
|
析取,
 |
(7)
|
否定,
 |
(8)
|
蘊涵,
 |
(9)
|
全稱量詞,
 |
(10)
|
和存在量詞
 |
(11)
|
這裡，變數 
在 
中是自由的，並且 
是透過將 
中所有自由出現的 
替換為 
而獲得的。在 
-後繼式規則和 
-前件式規則中出現的變數 
被稱為本徵變數。它不得出現在相應規則的下層時序中。
時序演算指定了經典一階邏輯，並且相同的框架也可以用於指定直覺邏輯。為了將推導限制為直覺邏輯，添加了額外的約束，即每個後繼式最多隻能有一個公式。根岑提出的經典（多後繼式）變體稱為 LK，直覺（單後繼式）變體稱為 LJ。LK 也可以被定義為單後繼式演算，並使用排中律作為另一個基本時序進行擴充。基於時序推理規則的證明理論也稱為根岑型。隨後引入了許多其他基於時序的邏輯公式。
雙重否定提供了一個示例推導，它在時序演算的經典變體中有效，但在直覺變體中無效。
上面顯示了第二個推導（這是一個有效的直覺推導）。
時序演算是證明論的一個非常有用的工具，主要是因為 cut 規則的可容許性，它可以從推導中消除，而不會影響可推導公式的集合。
