時間邏輯

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

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

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

三個基本時間算子是：總是、有時、和永不。

計算樹邏輯（CTL）、線性時序邏輯（LTL）和間隔時間邏輯（ITL）是時間邏輯的例子。

參見

• 持續時間演算 (DC)
• 混合邏輯
• 間隔時間邏輯
• 有限狀態驗證中的時間邏輯
• 動作的時間邏輯 (TLA)
• 在形式驗證中重要出版物（包括在形式驗證中時間邏輯的使用）

參考

1. 唐稚松. 时序逻辑程序设计与软件工程（上）. 北京: 科學出版社. 1999. ISBN 7-03-007006-2 （中文（簡體））. 改

外部連結

• Anthony Galton, Temporal Logic （頁面存檔備份，存於互聯網檔案館） in the Stanford Encyclopedia of Philosophy （頁面存檔備份，存於互聯網檔案館）.