時間邏輯

在邏輯中，術語時間邏輯被用來描述為表現和推理關於時間限定的命題的規則和符號化的任何系統。它有時也被稱為時態邏輯，這是 Arthur Prior 在1960年代介入的基於模態邏輯的特殊的時間邏輯系統。它後來被計算機科學家特別是 Amir Pnueli (阿米爾·伯努利) 和邏輯學家進一步的開發。中國著名計算機科學家唐稚松在這一領域亦有較深入的研究，並寫有專著《時序邏輯程序設計與軟件工程》^[1]。

時間邏輯首先被亞里士多德深入研究過，他的著作中有粗糙形式的一階時間模態二值邏輯。使用存在量詞或全稱量詞的任何邏輯都叫做一階邏輯。把時間看作狀態的序列的任何邏輯都是時間邏輯，只使用兩個真值的任何邏輯都是二值邏輯。

考慮陳述："我餓了"。儘管它的意思隨時間恆定，但這個陳述的真值隨時間可變。有時這個陳述為真，有時這個陳述為假，但是這個陳述不能同時為真並且為假。在時間邏輯中，陳述可以有隨時間變化的真值。與之相對的是非時間邏輯，它只能處理有着隨時間恆定的真值的陳述。