时间逻辑

在逻辑中，术语时间逻辑被用来描述为表现和推理关于时间限定的命题的规则和符号化的任何系统。它有时也被称为时态逻辑，这是 Arthur Prior 在1960年代介入的基于模态逻辑的特殊的时间逻辑系统。它后来被计算机科学家特别是 Amir Pnueli (阿米尔·伯努利) 和逻辑学家进一步的开发。中国著名计算机科学家唐稚松在这一领域亦有较深入的研究，并写有专著《时序逻辑程序设计与软件工程》^[1]。

时间逻辑首先被亚里士多德深入研究过，他的著作中有粗糙形式的一阶时间模态二值逻辑。使用存在量词或全称量词的任何逻辑都叫做一阶逻辑。把时间看作状态的序列的任何逻辑都是时间逻辑，只使用两个真值的任何逻辑都是二值逻辑。

考虑陈述："我饿了"。尽管它的意思随时间恒定，但这个陈述的真值随时间可变。有时这个陈述为真，有时这个陈述为假，但是这个陈述不能同时为真并且为假。在时间逻辑中，陈述可以有随时间变化的真值。与之相对的是非时间逻辑，它只能处理有着随时间恒定的真值的陈述。

三个基本时间算子是：总是、有时、和永不。

计算树逻辑（CTL）、线性时序逻辑（LTL）和间隔时间逻辑（ITL）是时间逻辑的例子。