时间逻辑 temporal (Valentin Goranko and Antje Rumberg)

首次发表于 1999 年 11 月 29 日星期一；实质性修订于 2020 年 2 月 7 日星期五。

时间逻辑这个术语被广泛用于涵盖关于时间和时间信息的推理的所有方法，以及它们在逻辑框架内的形式表示，更狭义地指的是由亚瑟·普赖尔于 1960 年左右引入的模态逻辑类型的方法，后来又由许多逻辑学家和计算机科学家进一步发展。时间逻辑的应用包括将其用作澄清关于时间的哲学问题的形式化工具，作为定义自然语言中时间表达的语义的框架，作为在人工智能中编码时间知识的语言，以及作为规范、形式分析和验证计算机程序和系统执行的工具。

在这里，我们提供了一个广泛代表性的、简洁而不可避免地不完整的概述，介绍了过去 50 年中引入和研究的丰富多样的时间模型和逻辑。

---

1. 从古代到现代的时间推理

对时间性和时间推理的讨论可以追溯到古代，甚至在《圣经》中也可以找到例子（Boyd 2014）。著名的箭飞矛盾悖论提到了时间的本质，并涉及到相应的变化概念。然而，早期的时间讨论主要集中在未来的偶然性问题上，即关于既非必然也非不可能的未来事件陈述是否具有确定的真值的问题。最广为人知且可能被引用最多的例子是亚里士多德在《解释学》（第 9 章）中讨论的海战场景。亚里士多德认为，像“明天将有一场海战”这样的陈述，以及相反的预测“明天将没有海战”，在现在并不具有必然性，因此缺乏确定的真值，同时承认明天要么会有一场海战，要么不会有。几十年后，哲学家迪奥多罗斯·克罗纳斯在他著名的主要论证中展示了未来的偶然性问题，这使他将可能定义为“是或将成为事实”。迪奥多罗斯论证的详细讨论可参见 Rescher 和 Urquhart（1971 年，第 XVII 章）以及有关未来偶然性的条目。

关于时间和偶然未来的哲学讨论在中世纪继续进行，这一主题被彼得·奥雷利、奥卡姆的威廉和路易斯·莫利纳等作家所接受。这里的焦点是如何将上帝的预知与人类自由的观念相调和。例如，奥卡姆接受了真实或实际未来的观念，认为未来的偶然陈述要么是真的，要么是假的，尽管只有上帝知道它们的真值。根据奥卡姆的观点，这并不意味着未来的偶然陈述是必然的，也就是说，人类有多种选择的可能性。后来，一些哲学家和逻辑学家致力于解决时间性与自由意志、不确定性和开放未来的问题，并提出了各种不同的解决方案。C.S.皮尔斯反对未来的偶然陈述可以有确定的真值的观念。他提出了只有现在和过去是实际的观点，而未来是可能性和必然性的领域。在类似的精神下，J.卢卡谢维奇设计了一种三值逻辑，将未来的偶然陈述的真值视为未确定的。有关自由意志、不确定性和开放未来的更近期的哲学讨论，请参见 Belnap 等人（2001）和穆勒（2014）。

现代形式时间逻辑的时代始于亚瑟·N·普赖尔的开创性工作，重要的先驱包括 H·赖兴巴赫，J·芬德利，J·卢卡谢维奇和 J·洛斯[1]。从 20 世纪 50 年代初开始，普赖尔引入并详细分析了几个不同版本的时态逻辑，其中许多在下文中讨论。普赖尔发明时态逻辑主要是出于哲学考虑。特别是 Diodorus Chronus 的主要论证和时间、（不）确定性、上帝的预知以及人类自由之间错综复杂的关系在他的工作中起到了关键作用。普赖尔相信，适当的逻辑方法可以帮助澄清和解决这些哲学问题。他引入了时间运算符，研究了度量时态逻辑，是混合时态逻辑的先驱者，设计了两个分支时间时态逻辑的版本，分别反映了奥卡姆和皮尔斯的观点等。他的工作为时间逻辑的广泛和多样化领域的发展铺平了道路，这个领域在哲学以外，还在计算机科学、人工智能和语言学等领域有许多重要应用。有关普赖尔的观点和工作的更多信息，请参见 Hasle 等人（2017）；Blackburn 等人（2019）；以及关于亚瑟·普赖尔的条目。关于时间推理和逻辑的历史提供了 Øhrstrøm 和 Hasle（1995）的全面概述。另请参阅 Øhrstrøm 和 Hasle（2006）以及 Dyke 和 Bardon（2013，第一部分）。

2. 时间的形式模型

时间的本体性质和属性引发了基本的哲学问题，这些问题在时间逻辑中使用的丰富的形式模型中得到了表达。例如，时间是基于瞬间还是间隔？它是离散的、稠密的还是连续的？时间有开始或结束吗？它是线性的、分支的还是循环的？在我们转向时间逻辑的形式语言和它们的语义之前，我们简要介绍下面两种最基本类型的时间形式模型以及它们的一些相关属性：基于瞬间和基于间隔的模型。

2.1 基于瞬间的时间模型

在基于瞬间的模型中，原始的时间实体是时间点，即时间瞬间，它们之间的基本关系（除了相等性）是时间的先后关系。因此，时间的流动由一个非空的时间瞬间集合 T 以及其上的先后关系 ≺ 表示：T=⟨T,≺⟩。

有一些基本属性可以自然地施加在基于瞬时的时间流上。时间的先行关系通常要求是一个严格的偏序关系，即一个非自反的、传递的、因此是非对称的关系。然而，有时候它被假设为自反的，然后加上反对称性条件。相关的属性如下所列。

在基于瞬时的时间模型领域中，一个基本的区别是线性模型和反向线性模型之间的区别，其中时间流被描绘为一条线，而反向线性模型允许树状表示，支持过去是固定的（因此是线性的），而未来可能是开放的（分支成多个可能的未来）。在任一情况下，时间的排序可能包含最小或最大元素，分别对应于时间中的第一个或最后一个瞬时。

另一个重要的区别是时间的离散模型，在计算机科学中很常见，以及密集或连续模型，在自然科学和哲学中更为常见。在正向离散（反向离散）模型中，每个具有后继（前任）的时间瞬时总是有一个相应的直接后继（直接前任）。相比之下，在密集模型中，任意两个连续的时间瞬时之间都存在另一个瞬时。

时间的基于瞬间的模型 T=⟨T,≺⟩ 可能具有的许多但不是全部的属性可以通过以下一阶句子来表达（其中 ⪯ 是 x≺y∨x=y 的缩写）：

• 反身性：∀x(x≺x)；

• 非反身性：∀x¬(x≺x)；

• 传递性: ∀x∀y∀z(x≺y∧y≺z→x≺z);

• 不对称性: ∀x∀y¬(x≺y∧y≺x);

• 反对称性: ∀x∀y(x≺y∧y≺x→x=y);

• 线性性（三分性，连通性）：∀x∀y（x=y∨x≺y∨y≺x）；

• 正向线性性：∀x∀y∀z（z≺x∧z≺y→（x=y∨x≺y∨y≺x））；

• 反向线性性：∀x∀y∀z（x≺z∧y≺z→（x=y∨x≺y∨y≺x））；

• 开始：∃x¬∃y(y≺x);

• 结束：∃x¬∃y(x≺y);

• 无始：∀x∃y(y≺x);

• 无终止（无界性）：∀x∃y(x≺y);

• 密度：∀x∀y(x≺y→∃z(x≺z∧z≺y));

• 正向离散性：∀x∀y(x≺y→∃z(x≺z∧z⪯y∧¬∃u(x≺u∧u≺z)));

• backward-discreteness: ∀x∀y(y≺x→∃z(z≺x∧y⪯z∧¬∃u(z≺u∧u≺x))).

注意，在线性模型中，这两个离散条件简化为

• ∀x∀y(x≺y→∃z(x≺z∧∀u(x≺u→z⪯u))) and

• ∀x∀y(y≺x→∃z(z≺x∧∀u(u≺x→u⪯z))), 分别。

时间的基于瞬间的模型的关键例子，这些模型的特性无法用一阶句子表达，而需要使用具有对集合的量化的二阶语言，包括连续性、良序性和有限区间性。连续性要求时间顺序中没有间隙。时间顺序不仅必须是稠密的，还必须是 Dedekind 完备的，即每个非空的时间瞬间集合都有一个最小上界。一个例子是实数的有序集合，而有理数的排序则不是：例如考虑所有平方小于 2 的有理数的集合。如果每个非空的线性时间瞬间集合都有一个最小元素，则基于瞬间的时间模型是良序的；如果在任意两个连续的时间瞬间之间最多有有限多个瞬间，则它具有有限区间性。自然数是良序的并具有有限区间性，负整数不是良序的但仍具有有限区间性，正有理数或实数既不是良序的也不具有有限区间性。正如我们将在第 3.6 节中看到的，这些二阶特性可以用命题时间语言来表达。

2.2 基于区间的时间模型

基于瞬间的时间模型通常不适用于推理持续时间事件，如果底层时间本体论使用时间间隔，即期间而不是瞬间作为原始实体进行建模，则更好。区间为基础的时间推理的根源可以追溯到泽诺和亚里士多德（Øhrstrøm 和 Hasle 1995）。在基于区间的设置中，泽诺著名的飞箭悖论（“如果在每个瞬间飞箭都静止不动，那么运动如何可能？”）不会出现。其他自然需要基于区间推理的例子包括：“昨晚爱丽丝写信时哭了很多，然后她平静下来了”和“比尔喝茶时邮递员来了”。

基于区间的模型通常假设线性时间。然而，它们本体论上比基于瞬间的模型更丰富，因为时间间隔之间可能存在的关系比时间瞬间之间的关系更多。例如，时间的基于区间的模型可以包括时间间隔集合 T 上的关系：时间先行 ≺，包含 ⊑ 和重叠 O，形式上表示为 T=⟨T,≺,⊑,O⟩。这种基于区间的关系和模型的一些自然属性包括：

• ⊑ 的自反性：∀x(x⊑x);

• ⊑ 的反对称性：∀x∀y(x⊑y∧y⊑x→x=y);

• ⊑ 的原子性（对于离散时间）：∀x∃y(y⊑x∧∀z(z⊑y→z=y));

• ≺ 相对于 ⊑ 的向下单调性：∀x∀y∀z(x≺y∧z⊑x→z≺y);

• O 的对称性: ∀x∀y(xOy→yOx);

• 重叠的时间间隔在一个子间隔中相交: ∀x∀y(xOy→∃z(z⊑x∧z⊑y∧∀u(u⊑x∧u⊑y→u⊑z)));

• ⊑ 相对于 O 的单调性：∀x∀y∀z(x⊑y∧xOz→z⊑y∨zOy)。

在 AI 中对基于区间的时间本体论和推理进行形式化研究的早期有影响力的作品中，Allen（1983）考虑了在线性顺序中两个区间之间可能出现的所有二元关系的集合，随后被称为 Allen 关系。这 13 个关系在表 1 中显示，它们是互斥且互为补集的，即在任何给定的严格区间对（不包括点区间）之间只有一个关系成立。此外，它们可以用其中的两个关系“相遇”和“被相遇”来定义（Allen 1983）。

区间关系	艾伦符号	HS notation
┣━━┫	equals{=}
├──┤ ┣┫	在之前 {<} / 在之后 {>}	⟨L⟩/⟨¯¯¯¯L⟩ 之后
├──╊┫	满足 {m} / 被满足于 {mi}	⟨A⟩/⟨¯¯¯¯A⟩ 之后
├─╊┿━┫	重叠 {o} / 被重叠于 {oi}	⟨O⟩/⟨¯¯¯¯O⟩ 重叠
├─╊┫	finished-by{fi} /finishes{f}	⟨E⟩/⟨¯¯¯¯E⟩ 结束
├╊╉┤	包含 {di} / 在 {d} 期间	⟨D⟩/⟨¯¯¯¯¯D⟩ 在期间
┣╉─┤	由 {si} 开始 / 开始 {s}	⟨B⟩/⟨¯¯¯¯B⟩ 开始

表 1：时间间隔之间的 Allen 关系及相应的 Halpern-Shoham 模态运算符（见第 6 节）。

给定由一定数量的时间间隔关系定义的抽象结构，这些关系需要满足一定的属性，问题是它是否可以通过线性时间上的具体基于间隔的模型来表示。各种表示定理提供了答案，例如参见 van Benthem（1983）；Ladkin（1987）；和 Venema（1990）。

2.3 基于瞬间和基于区间的时间模型

自从 Zeno 和 Aristotle 时代以来，选择瞬间和区间作为时间本体论的主要对象一直是一个备受争议的哲学主题。从技术上讲，这两种类型的时间本体论密切相关，并且它们可以相互归约：一方面，时间区间可以通过时间瞬间（开始和结束）的配对来定义；另一方面，时间瞬间可以被构造为退化的区间，即起始点和结束点重合的点区间。

然而，技术上的归约并不能解决语义问题，即句子是应该根据瞬间还是区间进行评估，人们可以争论瞬间和区间都是互补的。例如，Balbiani 等人（2011）研究了两类点区间模型，还研究了更复杂的时间模型，包括时间粒度模型（Euzenat 和 Montanari 2005），它允许不同分辨率级别的时间区间（例如分钟，小时，天，年等），度量和分层时间模型（Montanari 1996），等等。

在这里，我们讨论基于瞬间和基于区间的时间逻辑。关于时间逻辑中瞬间与区间的本体学优先性的进一步讨论，请参见 Hamblin（1972）；Kamp（1979）；Humberstone（1979）；Galton（1996）；以及 van Benthem（1983）对两种方法的详细比较探索。更多哲学和历史概述可参见 Øhrstrøm 和 Hasle（1995；2006）；Dyke 和 Bardon（2013）；以及 Meyer（2013）。

3. Prior 的基本时态逻辑 TL

在本节中，我们讨论了基于 Prior（1957；1967；1968）引入的基本时态逻辑 TL 的语言、语义和公理化。Prior 是时间逻辑的创始人，他发明时态逻辑的动机主要是哲学上的，他的思想受到了自然语言中时态的启发。Prior 方法的创新之处在于他将命题视为有时态而非无时态。从技术上讲，这是通过引入语言中的时间运算符，并赋予其模态逻辑类型的语义来实现的。鉴于时态在他的框架中所起的关键作用，Prior 自己将其解释称为时态逻辑，而现在更普遍的表达是时间逻辑。

3.1 Prior 的时间运算符

Prior 的时间逻辑学 TL 的基本语言扩展了标准命题语言（具有原子命题和真值功能连接词），通过四个时间运算符来表达其预期的含义如下：

• P：“在某个时间曾经是事实的是……”

• F：“在某个时间点上，将会发生……”

• H：“一直以来，都是如此……”

• G：“一直以来，都将会如此……”

例如，“Prior 发明了时间逻辑将永远成立”在时间逻辑中的翻译为 GP(Prior 发明 TL)，并且具有形式上的解释：“将永远成立的是，在某个时间点上，Prior 发明了时间逻辑”。

时间逻辑包括一对过去的时间运算符 P 和 H，以及一对未来的时间运算符 F 和 G。运算符 P 和 F 通常被称为“弱”时间运算符，而 H 和 G 被称为“强”时间运算符。相应的过去和未来运算符是对偶的，即它们可以通过以下等价关系相互定义：

Pφ≡¬H¬φ，Hφ≡¬P¬φ，Fφ≡¬G¬φ，Gφ≡¬F¬φ。

鉴于这些等价性，TL 的公式集可以根据给定的原子命题集 PROP 进行递归定义，如下所示：φ:=p∈PROP∣⊥∣¬φ∣(φ∧φ)∣Pφ∣Fφ。常见的真值联结词 ∨、→和 ↔ 可以像往常一样用 ¬ 和 ∧ 来定义。此外，我们可以定义 Aφ=Hφ∧φ∧Gφ，对偶地，Eφ=Pφ∨φ∨Fφ，在时间流的线性中分别表示“总是”和“有时”。

如前所述，普赖尔引入时间运算符最初是受到自然语言中时态的使用的启发，自然语言中的各种时态可以至少近似地在 TL 中捕捉到。例如：

• Pφ 对应于“φ 是事实”或“φ 一直是事实”。

• Fφ 对应于“φ 将会发生”。

• PPφ 对应于“φ 曾经发生过”。

• FPφ 对应于“φ 将会一直发生”。

• PFφ 对应于“φ 将会发生”或“φ 本来会发生”。

Hamblin 和 Prior 证明，在线性时间模型中，任何时间操作符的序列都可以简化为最多两个操作符的序列。总共，他们确定了 15 种不同的组合，也称为时态，可以在时间线性流中用 TL 表示（参见 Prior 1967，第 III.5 章）。尽管这些组合似乎超过了例如英语中的动词时态的数量，但自然语言中也有无法在 TL 中捕捉到的时间属性：例如，Prior 的时间操作符并不适合很好地模拟体貌的区别（例如“我写了一封信”和“我正在写一封信”之间的区别），这些区别可以在基于区间的框架中更好地处理。详见 Kuhn 和 Portner（2006）以及关于时态和体貌的条目。

3.2 TL 的语义学

TL 的标准语义本质上是一种 Kripke 风格的语义，这在模态逻辑中是常见的。在模态逻辑中，句子是在所谓的 Kripke 框架上进行评估的，该框架由一组非空的可能世界和它们之间的可达关系组成。在时间逻辑中，可能的世界是时间瞬间，并且可达关系在时间先后方面具有具体的解释。换句话说，句子是在基于瞬间的时间模型 T=⟨T,≺⟩ 上进行评估的，此后称为时间框架。请注意，到目前为止，没有对优先关系 ≺ 施加任何条件，如传递性、非自反性等。

对于 TL 的一组原子命题 PROP，TL 的时间模型是一个三元组 M=⟨T,≺,V⟩，其中 T=⟨T,≺⟩ 是一个时间框架，V 是一个赋值，将每个原子命题 p∈PROP 分配给被认为为真的时间瞬间集合 V(p)⊆T。（等价地，赋值可以通过函数 I:T×PROP→{true,false}给出，该函数在时间框架中的每个时间瞬间上为每个原子命题分配一个真值，或者通过标记或状态描述 L:T→P(PROP)给出，该函数将每个时间瞬间分配给被认为在该瞬间为真的原子命题集合。）

在给定的时间模型 M 中，在给定的时间瞬间 t 上，对于 TL 的任意公式 φ 的真值（表示为 M,t⊨φ），可以通过以下归纳方式定义：

• M,t⊨p 当且仅当 t∈V(p)，对于 p∈PROP;

• M,t⊭⊥ （即，不是这样的情况：M,t⊨⊥）;

• M,t⊨¬φ 当且仅当 M,t⊭φ;

• M,t⊨φ∧ψ 当且仅当 M,t⊨φ 且 M,t⊨ψ;

• M,t⊨Pφ 当且仅当 存在某个时间点 t′ 使得 M,t′⊨φ 且 t′≺t;

• M,t⊨Fφ 当且仅当 存在某个时间点 t′ 使得 M,t′⊨φ 且 t≺t′.

也就是说，给定一个时间模型 M，形式为 Pφ 的公式在时刻 t 上为真当且仅当 φ 在某个更早的时刻 t'上为真，而 Fφ 在 t 上为真当且仅当 φ 在某个更晚的时刻 t'上为真。因此，对于对偶的 H 和 G，成立的是 Hφ 在 t 上为真当且仅当 φ 在所有更早的时刻 t'上为真，而 Gφ 在 t 上为真当且仅当 φ 在所有更晚的时刻 t'上为真。

• M,t⊨Hφ 当且仅当对于所有时间时刻 t'，满足 t'≺t 时，M,t'⊨φ；

• M,t⊨Gφ 当且仅当对于所有时间时刻 t'，满足 t≺t'时，M,t'⊨φ。

注意，从模态逻辑的角度来看，从形式上讲，这里涉及到两个不同的可达关系：在过去运算符的情况下是“较早关系”，在未来运算符的情况下是“较晚关系”。在时间逻辑中，这两个关系都可以统一地由一个单一的优先关系来捕捉；毕竟，“较早”和“较晚”只是彼此的逆（即，如果 t 较早于 t'，则 t'较晚于 t）。

TL 的公式 φ 在时间模型 M 中是有效的（表示为 M⊨φ）当且仅当它在该模型的每个时间点都为真。此外，我们说 φ 在时间框架 T 中是有效的（表示为 T⊨φ）当且仅当它在该框架上的每个模型中都是有效的。因此，一个公式 φ 是有效的（表示为 ⊨φ）当且仅当它在所有时间框架中都是有效的，即在所有时间模型的所有时间点都为真。一个公式 φ 是可满足的当且仅当它的否定不是有效的，即如果 φ 在某个时间点的某个时间模型中为真。

TL 转化为一阶逻辑的标准翻译

正如模态逻辑的情况一样，TL 的语言和语义可以翻译成经典的一阶逻辑（参见 van Benthem 1983）。

假设 TL 的原子命题集合为 PROP={p0,p1,...}，并且让 L1 是一个带有=、二元谓词符号 R 和可数个一元谓词符号 P={P0,P1,...}的一阶语言，其中每个原子命题都有一个对应的一元谓词符号。TL 到 L1 的标准翻译 ST 定义如下，其中 θ[y/x]是将 θ 中所有自由出现的 x 替换为 y 的结果：

• ST(pi)=Pi(x);

• ST(⊥)=⊥;

• ST(¬φ)=¬ST(φ);

• ST(φ∧ψ)=ST(φ)∧ST(ψ);

• ST(Pφ)=∃y(yRx∧ST(φ)[y/x]), 其中 y 是一个新变量；

• ST(Fφ)=∃y(xRy∧ST(φ)[y/x]), 其中 y 是一个新变量。

由此可得，

• ST(Hφ)=∀y(yRx→ST(φ)[y/x]);

• ST(Gφ)=∀y(xRy→ST(φ)[y/x]).

例如：

ST(Gp1∨FHp2)=∀y(xRy→P1y)∨∃y(xRy∧∀z(zRy→P2z)).

并非每个一阶公式都在时间逻辑中有对应物。实际上，通过小心地重用个体变量，时间逻辑可以被翻译成一阶逻辑的双变量片段 FO2，这最终意味着时间逻辑的有效性可判定（因为 FO2 的有效性是可判定的，正如 Grädel 和 Otto 在 1999 年所示）。例如，上面的例子可以重写为

ST(Gp1∨FHp2)=∀y(xRy→P1y)∨∃y(xRy∧∀x(xRy→P2x)).

鉴于标准翻译，每个时间模型 M=⟨T,≺,V⟩ 可以被视为一个 L1-模型，通过将 R 解释为 ≺，将每个 Pi 解释为 V(pi)。然后：

M,t⊨φ 当且仅当 M⊨ST(φ)[x:=t]，M⊨φ 当且仅当 M⊨∀xST(φ)。

因此，在时间模型中，TL 公式的有效性是一个一阶性质。另一方面，时间框架中的有效性是一个二阶性质，因为它涉及对估值的量化。如果我们将 P 中的一元谓词视为二阶语言 L2 的谓词变量，那么每个时间框架 T=⟨T,≺⟩ 可以被视为一个 L2-模型，其中谓词变量表示相应原子命题的估值。令 ∀¯¯¯¯Pφ 表示 L2-公式 φ 在其中出现的所有谓词变量上的全称闭包。那么：

T⊨φ 当且仅当 T⊨∀¯¯¯¯P∀xST(φ)，⊨φ 当且仅当 ⊨∀¯¯¯¯P∀xST(φ).

将 TL 标准翻译为一阶逻辑，可以使用经典逻辑的工具和技术对时间逻辑的各个方面进行系统处理（参见 Blackburn 等人 2006 年）。然而，正如我们将在第 3.6 节中看到的，不是所有时间框架的一阶属性都可以由时间公式定义；反之亦然，不是所有可以由 TL 公式表达的时间框架属性都可以由一阶定义。时间逻辑和一阶逻辑之间的非平凡对应关系作为描述时间属性的替代语言逐渐显现出来。

3.4 时态逻辑、一阶逻辑和麦克塔格特的时间序列

在前一节讨论的标准翻译中，将 Prior 的基本时态逻辑的语义与一阶逻辑联系起来。然而，对于形式化时间逻辑的这两种方法之间存在重要差异。实际上，在时间逻辑的早期阶段，Prior 的方法被视为使用一阶逻辑的更传统方法的竞争对手。时态逻辑和一阶逻辑之间的竞争可以被看作是反映时间性质的基本区别，即 McTaggart（1908）引入的 A 系列和 B 系列之间的区别。

A 系列本质上是关于过去、现在和未来的时间和时间顺序的描述。相比之下，B 系列是基于“更早”和“更晚”的概念。因此，虽然 A 系列假设了一个特殊的现在，但 B 系列涉及对时间的全局、整体性的观点。McTaggart 认为 B 系列是不足的，因为它缺乏适当的变化概念，他也因为 A 系列的不一致性而拒绝了它，因为现在的未来将成为过去，这根据他的观点要求同一时间点具有不兼容的属性。基于此，他得出时间是虚幻的结论。有关 McTaggart 的解释及其哲学意义的详细讨论，请参见 Ingthorsson（2016）和时间条目。

时间的 A 系列和时态逻辑之间存在着密切的对应关系，与此同时，B 系列和一阶逻辑之间也存在着对应关系，正如 Prior（1967 年，第 1 章）本人已经指出的那样。例如，考虑句子“天黑了，天亮了，又会变亮。”这个句子可以在时间逻辑中形式化为 dark∧P(light)∧F(light)，而它的一阶逻辑表达式为 dark(t1)∧∃t0(t0≺t1∧light(t0))∧∃t2(t1≺t2∧light(t2))。时间逻辑公式由时态命题组成（不包含时间运算符的命题是现在时态的），并且它调用了现在的局部视角。相比之下，一阶逻辑公式中的命题是无时态或无时态的。在这里，我们提供的是时间瞬间的谓词，而不是时态，所涉及的视角是来自时间之外的全局视角。Prior 认为，并不是所有可以用时态语言表达的东西都可以用无时态语言表达，他的经典例子是：“谢天谢地，终于结束了！”（Prior 1959 年）。

3.5 时间逻辑的公理系统 Kt

像每个形式逻辑系统一样，时间逻辑有两个主要方面：语义和演绎。在本节中，我们介绍了一个关于时间逻辑有效性的演绎系统，即最小时间逻辑 Kt。逻辑 Kt 是一个公理系统，即由一系列公理和推理规则给出。该系统最早由 Lemmon 研究，之前由 Hamblin 和 Prior 提出了一些公理化的建议（参见 Rescher 和 Urquhart 1971 年，第 VI 章）。

最小时间逻辑 Kt 的公理列表通过以下四个公理模式扩展了经典命题逻辑的公理列表：

• (KG)G(φ→ψ)→(Gφ→Gψ)

• (KH)H(φ→ψ)→(Hφ→Hψ)

• (GP)φ→GPφ

• (HF)φ→HFφ

第一和第二个公理模式是所谓的模态逻辑的 K-公理的时间对应物，因此术语为 Kt。第三和第四个公理模式捕捉了过去和未来运算符的交互。在形式层面上，它们保证这些运算符对应于相应的逆向时间关系，即较早和较晚。

推理规则包括经典的假言演绎规则之外，还有两个时间运算符的必要性规则（其中 ⊢ 表示“可推导”）：

• (MP)如果 ⊢φ 且 ⊢φ→ψ，则 ⊢ψ。

• (NECG)如果 ⊢φ，则 ⊢Gφ。

• (NEGH)如果 ⊢φ，则 ⊢Hφ。

公理系统 Kt 在 TL 中对有效性是完备且正确的：只有那些在 TL 中有效的公式才能通过给定的推理规则从公理中推导出来。证明可参见 Rescher 和 Urquhart（1971）；Goldblatt（1992）；以及 Gabbay 等人（1994）。

3.6 在 TL 和 Kt 的扩展中表达时间属性

最小的时间逻辑 Kt 捕捉到那些不依赖于任何特定假设关于时间先后关系属性的 TL 的有效性。然而，许多时间框架的自然属性可以通过时间公式来表达，并且作为附加公理，这些公式可以用来表示关于时间结构的重要本体论假设。

如果 TL 的时间公式在所有具有该属性的框架中都是有效的，则该公式表达（定义或对应于）时间框架的属性。时间框架属性（见第 2.1 节中的列表）与 TL 公式之间最重要的对应关系包括：

(REF)	Gφ→φ、Hφ→φ、φ→Fφ 或 φ→Pφ 中的任何一个。 (反身性)
(TRAN)	Gφ→GGφ、Hφ→HHφ、FFφ→Fφ 或 PPφ→Pφ 中的任何一个 (传递性)
(LIN-F)	PFφ→(Pφ∨φ∨Fφ) (前向线性性)
(LIN-P)	FPφ→(Pφ∨φ∨Fφ) (逆线性)
(LIN)	(PFφ∨FPφ)→(Pφ∨φ∨Fφ) (线性)
(BEG)	H⊥∨PH⊥ (时间有一个开始（假设非自反性）)
(END)	G⊥∨FG⊥ (时间有一个结束（假设非自反性）)
(NOBEG)	P⊤ 或 Hφ→Pφ (时间没有开始)
(NOEND)	F⊤ 或 Gφ→Fφ (时间没有终点)
(DENSE)	GGφ→Gφ, HHφ→Hφ, Fφ→FFφ, 或 Pφ→PPφ 中的任何一个 (密度)
(DISCR-F)	(F⊤∧φ∧Hφ)→FHφ (正向离散性（假设线性）)
(DISCR-P)	(P⊤∧φ∧Gφ)→PGφ (后向离散性（假设线性）
(INDG)	Fφ∧G(φ→Fφ)→GFφ （前向归纳）
(INDH)	Pφ∧H(φ→Pφ)→HPφ （后向归纳）
(COMPL)	A(Hφ→FHφ)→(Hφ→Gφ) (Dedekind 完备性（回忆一下，Aφ=Hφ∧φ∧Gφ）)
	或者，Dedekind 完备性可以通过以下方式表达：(FG¬φ∧Fφ)→F(G¬φ∧HFφ)。
(WELLORD)	H(Hφ→φ)→Hφ （具有传递性的良序）
(FIN-INT)	（G(Gφ→φ)→(FGφ→Gφ)) ∧ (H(Hφ→φ)→(PHφ→Hφ)) （有限区间）
	注意，这个公式等同于（INDG）和（INDH）的合取。

原则（LIN）将正向线性（LIN-F）和反向线性（LIN-P）结合在一个条件中。然而，得到的公式并不足以保证时间顺序的连通性。换句话说，它不能排除不连续的线性时间线。值得注意的是，（INDG）意味着反向离散性，而（INDH）意味着正向离散性，但反之则不成立。例如，由自然数的一个副本后跟整数的一个副本组成的时间流是反向离散的，但它不满足（INDG）。

回想一下，上述提到的最后三个属性——戴德金完备性、良序性和有限区间性——不能通过一阶句子来定义，但它们可以通过时间公式来表达。另一方面，一些关于时间框架的非常简单的一阶可定义属性，如非自反性或反对称性，在 TL 中无法表达。有关表达时间属性的时间公理以及有关这些结果的详细信息，请参见 Segerberg（1970）；Rescher 和 Urquhart（1971）；Burgess（1979）；van Benthem（1983；1995）；Goldblatt（1992）；和 Hodkinson 和 Reynolds（2006）。

通过将 Kt 的公理列表扩展为上述原则之一或几个原则，可以捕捉到一些自然时间模型的有效性；也就是说，存在声音和完备的公理扩展，适用于相应的时间框架类。其中一些扩展在时间逻辑的早期已经被研究，Prior（1967）讨论了通过假设不同的公理组合而得到的各种系统。

K4t=Kt+(TRAN)：所有传递性框架。S4t=Kt+(REF) + (TRAN)：所有偏序。Lt=Kt+(TRAN) +(LIN)：所有严格线性排序。Nt=Lt+(NOEND) + (INDG) + (WELLORD)：⟨N,<⟩。Zt=Lt+(NOBEG) + (NOEND) + (INDG) + (INDH)：⟨Z,<⟩。Qt=Lt+(NOBEG) + (NOEND) + (DENSE)：⟨Q,<⟩。Rt=Lt+(NOBEG) + (NOEND) + (DENSE) + (COMPL)：⟨R,<⟩。

正如这些公理化所示，（LIN）不能保证严格意义上的连通性，或者 TL 中不可反驳性不可定义的事实，在这里并不构成任何严重的限制：连通性和不可反驳性并不产生任何新的有效性。

上述逻辑中的每一个都是可判定的（即具有可判定的有效性集合），这通常通过证明所谓的有限模型性质（“每个可满足的公式在一个有限模型中是可满足的”）来证明，在大多数情况下，是针对非标准有限模型。有关这些公理系统变体的完备性证明以及可判定性证明的详细证明，请参见 Segerberg（1970）；Rescher 和 Urquhart（1971）；Burgess（1979）；Burgess 和 Gurevich（1985）；Goldblatt（1992）；以及 Gabbay 等人（1994）。

4. TL 在线性时间上的扩展

时间的一种非常自然的基于瞬时的模型类是线性模型类，而且在 Prior 发明时态逻辑之后不久，就提出了 TL 在线性时间上的几个扩展。在本节中，我们讨论了 Prior 基本时间逻辑的两个扩展：在离散线性时间模型上通过 Next Time 运算符扩展 TL 和引入 Since 和 Until 运算符。这些运算符也构成了线性时间逻辑 LTL 的基础，该逻辑在计算机科学中有广泛的应用。

4.1 添加 Next Time 运算符

在线性、无界、向前离散的时间模型 M=⟨T,≺,V⟩ 中，其中每个瞬时 t 都有一个唯一的直接后继 s(t)，自然地可以添加一个新的时间运算符 X（“下一个时间”或“明天”），其语义为：[2]

M,t⊨Xφ 当且仅当 M,s(t)⊨φ.

也就是说，Xφ 在时间点 t 上为真当且仅当 φ 在 t 的直接后继 s(t) 上为真。Next Time 运算符已经在 Prior (1967, 第 IV.3 章) 中提到过，但它的重要性首次在 LTL 的背景下得到充分的认识。

运算符 X 满足 K 公理。

• (KX)X(φ→ψ)→(Xφ→Xψ);

和功能公理

• (FUNC)X¬φ↔¬Xφ.

它还使得 G（FPG）的递归，固定点定义成为可能，并且在自然数的排序上，运算符 X 和 G 满足归纳原理（IND）。假设时间先后关系 ≺ 是自反的，这是计算机科学中的一个标准假设，我们得到以下定义：

• (FPG)Gφ↔(φ∧XGφ);

• (IND)φ∧G(φ→Xφ)→Gφ.

在具有 G、H 和 X 的语言中：

Lt(X)=Lt + KX + FUNC + FPG 完全公理化了线性、无界、前向离散排序的时间逻辑，同时

Nt(X)=Nt + KX + FUNC + FPG + IND 其中 s(n)=n+1，完全公理化了 ⟨N,s,≤⟩ 的时间逻辑。

通常用 Y（“昨天”）表示 X 的过去类似物，可以类似地定义和公理化。更多细节请参见 Goldblatt（1992）和 Andréka 等人（1995）。

4.2 添加自从和直到

或许 Prior 的基本时态逻辑 TL 最重要的扩展是汉斯·坎普在他的博士论文（Kamp 1968）中引入了二元时间运算符 S（“自从”）和 U（“直到”）。它们的直观意义是[3]

• φSψ“自从 ψ 成立以来，φ 一直成立。”

• φUψ“直到 ψ 成立之前，φ 将一直成立。”

例如，句子“I will keep trying until I succeed”可以形式化为：tryUsucceed。另一个例子，“自从 Mia 离家以来，Joe 一直不开心，一直喝酒直到失去意识”可以使用 Since 和 Until 来形式化：

(Joe 不开心 ∧(Joe 喝酒 U¬(Joe 有意识)))S(Mia 离开)。

在时间模型 M=⟨M,≺,V⟩ 中，S 和 U 的形式语义由以下两个子句给出：

M,t⊨φSψ 当且仅当存在某个 s 使得 M,s⊨ψ 且 s≺t，并且对于每个满足 s≺u≺t 的 u，M,u⊨φ；M,t⊨φUψ 当且仅当存在某个 s 使得 t≺s 且 M,s⊨ψ，并且对于每个满足 t≺u≺s 的 u，M,u⊨φ。

这些是哲学中普遍存在的 S 和 U 的“严格”版本。在计算机科学中，通常考虑语义子句的自反版本。

先验的时间运算符 P 和 F 可以通过 S 和 U 来定义：

Pφ:=⊤Sφ 和 Fφ:=⊤Uφ。

在非自反、前向离散、线性时间序列上，S 和 U 还允许定义下一个时间运算符 X：

Xφ:=⊥Uφ.

注意，这个定义在反身性时间顺序上失败了，这表明 S 和 U 的非反身版本比它们的反身版本更具表达力。[4] 其他自然操作符也可以用 S 和 U 来定义，例如 Before，其定义为 φBψ:=¬((¬φ)Uψ)，直观地解释为“如果 ψ 将来会发生，那么 φ 将在 ψ 之前发生”。

Kamp（1968）证明了关于带有 Since 和 Until 的时间语言表达能力的以下重要结果：

在一阶逻辑中可定义的连续、严格线性排序类上的每个时间算子都可以用 S 和 U 来表达。

Stavi 随后提出了另外两个算子 S'和 U'，当它们与 S 和 U 一起添加时，可以使时间语言在所有线性框架上具有表达能力。然而，正如 Gabbay 所示，任何有限数量的新算子都无法使时间语言在所有偏序上具有功能完备性。有关这些结果的概述，请参阅 Gabbay 等人（1994）。

Burgess（1982a）在具有自反优先关系的所有线性排序类上提供了一个完备的 Since-Until 逻辑公理系统，该系统由 Xu（1988）进一步简化。Venema（1993）和 Reynolds（1994；1996）获得了严格线性排序的这种公理化的扩展。有关详细信息和相关结果，请参阅 Burgess（1984）；Zanardo（1991）；Gabbay 等人（1994）；Finger 等人（2002）；以及 Hodkinson 和 Reynolds（2006）。Burgess-Xu 公理系统及其一些扩展在附加文档中呈现：

伯吉斯-徐氏 Since 和 Until 公理系统及其扩展

4.3 线性时间逻辑 LTL

在计算机科学中，最流行和广泛使用的时间逻辑是线性时间逻辑 LTL，它是在 Pnueli（1977）的开创性论文中提出的，并且在 Gabbay 等人（1980）中首次明确地进行了公理化和研究。在 LTL 中，时间被构想为一系列线性离散的时间瞬间，并且语言涉及运算符 G、X 和 U（没有过去运算符）。LTL 在 ⟨N,≤⟩ 上进行解释，其中时间排序被假定为是自反的，这在计算机科学中很常见。

逻辑学 LTL 对于在反应式系统中表达无限计算的属性非常有用，例如安全性、活性和公平性，如第 11.1 节所述。例如，规范“每次发送消息时，最终都会返回一个收据确认，并且在收据确认返回之前，消息不会被标记为'已发送'”可以在 LTL 中形式化为：

G(Sent→(¬MarkedSent U AckReturned)).

LTL 的公理系统通过 G 的 K 公理、X 的 K 公理和功能公理，以及提供 G 和 U 的自反版本的不动点特征的公理来扩展经典命题逻辑。

• (KG)G(φ→ψ)→(Gφ→Gψ)

• (KX)X(φ→ψ)→(Xφ→Xψ)

• (FUNC)X¬φ↔¬Xφ

• (FPG)Gφ↔(φ∧XGφ)

• (GFPG)ψ∧G(ψ→(φ∧Xψ))→Gφ

• (FPU)φUψ↔(ψ∨(φ∧X(φUψ)))

• (LFPU)G((ψ∨(φ∧Xθ))→θ)→(φUψ→θ)

推理规则仅涉及经典的假言演绎和 G 的必要性规则。从技术角度来说，公理(FPG)表明 Gφ 是由 ΓG 定义的算子 ΓG(θ)=φ∧Xθ 的不动点，而(GFPG)表明 Gφ 是 ΓG 的（在其扩展方面，集合论上）最大的后不动点。同样，公理(FPU)表明 φUψ 是由 ΓU 定义的算子 ΓU(θ)=ψ∨(φ∧Xθ)的不动点，而(LFPU)表明 φUψ 是 ΓU 的最小的前不动点。这个公理系统的一些变体在附加文档中提出：

LTL 的公理系统的一些变体

早期对线性时间的时间逻辑的研究可以在 Rescher 和 Urquhart（1971）以及 McArthur（1976）中找到。上述公理系统的变体的完备性证明可以在 Gabbay 等人（1980; 1994）；Goldblatt（1992）；以及 Finger 等人（2002）中找到。本节提到的所有逻辑都具有有限模型性质（通常是针对非标准模型），因此是可判定的。有关可判定性的证明，请参阅完备性的参考文献。

5. 分支时间逻辑

Prior 的时间逻辑学研究的很大一部分最初是受到 Diodorus Chronus 的 Master Argument 引发的关于时间和模态之间关系的问题的驱动，并由其宿命论的结论所引起的。Prior 对不确定性和开放未来等主题有着真正的兴趣。他在这里的一个主要关注点是允许人类的自由。为了捕捉 Diodorus 论证中潜在的历史必然性概念，他选择了时间和模态相互关系的分支表示，这个概念最早是由 Kripke 在 1958 年的一封信中向他提出的（参见 Ploug 和 Øhrstrøm 2012）。Diodorus 对模态的理解，即对线性时间的量化，被放弃并被一棵树的图像所取代，树枝代表未来的替代可能性。Prior（1967 年，第 7 章）考虑了两个不同版本的分支时间逻辑，分别与 Peirce 和 Ockham 的历史观点相关联。对这些思想的早期形式化处理见 Thomason（1970；1984）和 Burgess（1978）。自那时以来，已经提出了许多技术结果和进一步的发展，我们在下面提到了最重要的几个。关于 Prior 对不确定性和人类自由的动机观点，请参阅 Øhrstrøm 和 Hasle（1995 年，第 2.6 章和第 3.2 章）和 Øhrstrøm（2019 年）。关于分支时间理论的哲学方面的详细讨论，请参阅 Belnap 等人（2001 年）和 Correia 和 Iacona（2013 年）。

5.1 Prior 的分支时间理论

Prior 理论中核心的图片让人想起了博尔赫斯的《分岔路径花园》中所描绘的那幅画。时间和模态的相互关系被表示为一棵由线性向过去延伸并分支成多个可能未来的替代历史树。向后的线性性捕捉了过去是固定的这一观念；向前的分支反映了未来的开放性。在每个时间点上，可能有多条通向未来的路径，而每条路径代表着一种未来的可能性。

形式上，一棵树（或分支时间结构）是一个时间框架 T=⟨T,≺⟩，其中时间先后关系 ≺ 是对时间瞬间集合 T 上的向后线性偏序关系，使得任意两个瞬间在 T 中有一个公共的 ≺-前身。也就是说，树中的每个时间瞬间都有一个线性有序的 ≺-前身集合，并且任意两个瞬间共享一些共同的过去。前者的条件排除了向后分支，而后者确保了“历史上的连通性”。在哲学文献中，时间先后关系 ≺ 通常被假定为非自反的，即严格偏序关系，而在计算机科学中，通常研究的是自反结构。

一棵树 T=⟨T,≺⟩ 在一个统一的结构中描绘了未来的替代、相互不兼容的可能性，并且可以被划分为多个历史。T 中的一个历史是一个由 ≺ 线性有序的最大（即不可扩展）时间瞬间集合，即树中的整个路径；它代表了一种完整的可能事件过程。我们用 H(T)表示 T 中所有历史的集合，并且用 H(t)表示通过给定时间瞬间 t 的历史集合。

一些哲学家批评“分支时间”这个标签是一个误称，认为时间并不分支，而是线性演化。早期的这种批评可以在 Rescher 和 Urquhart（1971）中找到，Belnap 等人（2001）也提出了类似的观点，他们建议使用“分支历史”这个标签。这种批评还对这里用来指代树的原始点的术语“时间瞬间”是否恰当提出了质疑。出于统一性的原因，我们坚持使用这个术语。在分支时间的文献中，更中立的表达“时刻”更为普遍，在 Belnap 等人（2001）中，时间瞬间和时刻之间的区别得到了正式的阐述：分支时间结构与一个线性有序的时间瞬间集相关联，其中一个瞬间被定义为包含在不同历史中的同时发生的时刻的集合。

5.2 皮尔斯分支时间逻辑

Prior 的基本时态逻辑 TL 对时间的结构持中立态度。在具有未来可能性的分支时间设置中，未来运算符 F 的原始语义已不再足以捕捉未来的真实性。在这样的设置中，未来运算符 F 仅表示“可能会发生...”。因此，Prior（1967 年，第 7 章）考虑了分支时间中未来运算符的两种替代语义，分别产生了皮尔斯分支时间逻辑和奥卡姆分支时间逻辑。

在 Peircean 分支时间逻辑 PBTL 中，未来运算符 F 的直观含义是“必然会发生...”。也就是说，未来的真值被构想为在所有可能的未来中都是真的。在这种新的解释下，未来运算符 F 不再是强未来运算符 G 的对偶，现在需要将 G 作为附加的原始运算符包含到语言中。给定原子命题 PROP 的集合，PBTL 的公式集可以递归地定义如下：

φ:=p∈PROP∣⊥∣¬φ∣(φ∧φ)∣Pφ∣Fφ∣Gφ.

PBTL 的公式在一个称为 Peircean 树模型的树 T=⟨T,≺⟩ 上的时间模型 M=⟨T,≺,V⟩ 中进行评估。如常，V 是一个赋值，它将每个原子命题 p∈PROP 分配给被认为是真的时间瞬间的集合 V(p)⊆T，并且在 Peircean 树模型 M 中，对于给定的时间瞬间 t，任意公式 φ 的真值是通过归纳定义的。真值功能连接词和过去运算符 P（及其对偶 H）的语义子句与 TL 中的相同（参见第 3.2 节），我们在这里只提供未来运算符 F 和 G 的语义子句：

M,t⊨Fφ 当且仅当对于所有历史 h∈H(t)，存在某个时间点 t′∈h，使得 t≺t′且 M,t′⊨φ；M,t⊨Gφ 当且仅当对于所有历史 h∈H(t)和所有时间点 t′∈h，使得 t≺t′，M,t′⊨φ。

因此，根据皮尔斯语义学，形如 Fφ 的公式在时间点 t 上为真当且仅当通过 t 的每个历史都包含某个后续时间点 t′，在该时间点上 φ 为真。强未来运算符 G 基本保留其原始语义，但现在读作“将必然始终如此…”。请注意，在这种情况下，对历史的普遍量化是多余的，可以省略而不失意义。G 的对偶是 TL 的弱未来运算符，现在用 f 表示，而皮尔斯的 F 的对偶通常写作 g（参见 Burgess 1980）。所有未来运算符都涉及（隐式或显式）对历史的量化，并且是模态化的：它们捕捉了关于未来的可能性和必要性。实际上没有未来，因此也没有纯粹未来真理的概念。这与皮尔斯的观点相吻合，因此普赖尔称此系统为“皮尔斯式”。

请注意，在皮尔斯式时间逻辑中，公式 φ→HFφ 不再成立，这阻止了 Diodorus Chronus 的主要论证：现在的情况不一定在过去是必然的。此外，尽管皮尔斯主义保留了双值性和排中律 φ∨¬φ，但它使所有表达未来可能性的公式都为假，从而使未来排中律 Fφ∨F¬φ 无效。该原则表明最终 φ 或 ¬φ 将成为事实，并且通常被认为是直观上有效的（参见 Thomason 1970）。

伯吉斯（1980）使用所谓的加贝非反身性规则的版本，给出了皮尔斯分支时间时间逻辑的完整有限公理化。扎纳多（1990）提供了一种替代的公理化方法，其中加贝非反身性规则被无限列表的公理所取代。

5.3 奥卡姆分支时间时间逻辑

尽管普赖尔本人更倾向于皮尔斯主义，但他开发的奥卡姆分支时间时间逻辑作为一种可能的替代方案，在分支时间的文献中获得了更多的影响力。在奥卡姆分支时间逻辑 OBTL 中，真值不仅相对于树中的时间点进行相对化，而且还相对于通过该时间点的历史进行相对化，并且未来运算符 F 现在沿着给定的历史进行评估。因此，F 的直观含义变为“关于给定的历史，将会发生...”。除了时间运算符 F 和 P 之外，OBTL 的语言还包含一个模态运算符 ◊ 和其对偶 □，它们被解释为历史上的量词。给定一组原子命题 PROP，OBTL 的公式集可以通过递归定义来确定。

φ:=p∈PROP∣⊥∣¬φ∣(φ∧φ)∣Pφ∣Fφ∣◊φ.

在奥卡姆主义语义中，公式在树模型 T=⟨T,≺⟩ 上进行解释，该模型由时间瞬间 t∈T 和包含该瞬间的历史 h∈H(t)组成的对(t,h)。有时，瞬间-历史对(t,h)被构想为从瞬间 t 开始并跨越由历史 h 指定的可能未来的“初始分支”（参见例如 Zanardo 1996）。

自然而然地，问题就出现了如何在模型中评估原子命题：原子命题的真值仅取决于时间瞬间，还是也取决于历史？对这个问题的答案关键取决于原子命题是否可能包含“未来的痕迹”（Prior 1967, 124）。关于原子命题的处理在文献中没有共识（参见 Zanardo 1996），Prior 本人曾提出过一种具有两种不同类型的原子命题的双排序语言的想法，每种类型的原子命题都需要不同的处理（Prior 1967, 第 7.4 章）。在这里，我们将允许原子命题的真值取决于时间瞬间和历史。基于瞬间的命题的更具体情况可以通过对 p∈PROP 施加额外要求，使得公式 p↔□p 对其成立。

因此，奥卡姆主义树模型是一个三元组 M=⟨T,≺,V⟩，其中 T=⟨T,≺⟩ 是一棵树，V 是一个赋值，它将每个原子命题 p∈PROP 分配给一组瞬时历史对 V(p)⊆T×H(T)，在这些对中 p 被认为是真的。在奥卡姆主义树模型 M 中，任意公式 φ 的真值在瞬时历史对(t,h)上的定义如下：

• M,t,h⊨p 当且仅当 (t,h)∈V(p)，对于 p∈PROP；

• M,t,h⊭⊥；

• M,t,h⊨¬φ 当且仅当 M,t,h⊭φ;

• M,t,h⊨φ∧ψ 当且仅当 M,t,h⊨φ 且 M,t,h⊨ψ;

• M,t,h⊨Pφ 当且仅当 存在时间瞬间 t′∈h 使得 M,t′,h⊨φ 且 t′≺t;

• M,t,h⊨Fϕ 当且仅当 M,t′,h⊨ϕ 对于某个时间点 t′∈h，其中 t≺t′；

• M,t,h⊨◊φ 当且仅当 M,t,h′⊨φ 对于某个历史 h′∈H(t)；

时间运算符的解释基本上与线性时间逻辑中的解释相同：评估的时刻在给定的历史上向前和向后移动。请注意，在过去运算符 P 的语义子句中，“t′∈h”的要求是多余的，因为没有向后分支。然而，在未来运算符 F 的子句中，这一点至关重要。通常，强时间运算符 H 和 G 被定义为 P 和 F 的对偶。模态运算符量化通过当前时刻的历史集合。运算符 ◊ 是对该集合的存在量化，并捕捉可能性，而它的对偶 □ 包含全称量化，并表达“必然性”或“历史必然性”。

我们说 OBTL 的一个公式是 Ockhamist 有效的，当且仅当它在所有 Ockhamist 树模型的所有时刻-历史对中都为真。显然，在时间的线性模型中有效的所有时间公式也是 Ockhamist 有效的。因此，Ockhamism 验证了未来排中律原则 Fφ∨F¬φ（在时间不结束的假设下）以及公式 φ→HFφ。然而，它无效化了过去的必然性原则 Pφ→□Pφ，从而阻止了 Diodorus 的主要论证。

在 Peircean 分支时间逻辑 PBTL 中，未来真理被模态化，而在 Ockhamist 分支时间逻辑 OBTL 中，未来真理和模态性分离。Peircean 的公式 Fφ 和 Gφ 等价于 Ockhamist 的 □Fφ 和 □Gφ。实际上，PBTL 可以被看作是 OBTL 的一个适当片段，即仅包括那些通过使用真值功能连接词和组合模态性 □F、□G 及其对偶 ◊F 和 ◊G 从（基于时刻的）原子命题递归构建的公式。然而，Peircean 语言比 Ockhamist 语言表达能力较弱，例如缺乏等价于 ◊GFφ 的表达方式（证明见 Reynolds 2002）。

通过将瞬时的真理相对化为树中的历史，奥卡姆派分支时间逻辑提供了一个明确的未来真理概念。然而，从哲学角度来看，对历史的相对化并非完全没有问题。对于奥卡姆派历史参数，基本上有两种不同的解释方式：首先，可以将历史参数视为指涉可能性树中事件的实际发展过程，由于这个想法与奥卡姆对未来的观点相吻合，普赖尔选择了“奥卡姆主义”这个标签。实在主义立场引发了各种分支时间逻辑学，通常被总结为“薄红线”理论（有关讨论，请参见 Belnap 和 Green 1994；Belnap 等人 2001；和 Øhrstrøm 2009）。其次，可以将历史参数视为真理的辅助参数，该参数无法在上下文中初始化：可以争论的是，话语的上下文唯一确定了话语的时间瞬间，但如果未来真正是开放的，它不能确定通过该瞬间的历史中的哪一个。这种思路引发了“后语义”解释，旨在通过引入超真理的概念来弥合递归语义机制和上下文之间的差距，尤其是汤姆森的超价论（Thomason 1970）和麦克法兰的评估敏感的后语义学（MacFarlane 2003；2014）。这些解释放弃了双值性，但保留了排中律 φ∨¬φ 和未来排中律 Fφ∨F¬φ 的原则。

从逻辑学的角度来看，奥卡姆主义对分支时间的处理方式与 T×W 框架的概念以及更一般的坎普框架的概念有很强的相似之处，这些概念在 Thomason（1984）中进行了讨论；后者在技术上等同于 Zanardo（1996）中引入的奥卡姆主义框架的概念。这些框架建立在一组不同的可能世界上，每个可能世界都具有内部线性时间结构，并假设可能世界之间存在一种时间相对的历史可达关系。也就是说，历史的重叠被可达性所取代，而可能世界被视为原始元素，而在分支时间中，历史是根据瞬间来定义的。因此，如果我们将由历史相关的可能世界组成的框架合并为一棵树（用身份替代可达性），可能会出现一些不对应任何可能世界的新历史（有关构建，请参见 Reynolds 2002）。

从技术上讲，基于可能世界的方法和基于分支时间的方法之间的区别可以通过为分支时间结构配备一个足够丰富的原始历史集合来克服，这个集合可以覆盖整个结构，被称为束。束树被定义为三元组 ⟨T,≺,B⟩，其中 T=⟨T,≺⟩ 是一棵树，束 B⊆H(T)是一个非空的历史集合，使得 T 中的每个瞬间都属于 B 中的某个历史（Burgess 1978; 1980）。奥卡姆分支时间逻辑直接推广到束树：唯一的区别是语义现在限制在束中的历史上。束树的有效性等价于 Kamp 有效性（Zanardo 1996; Reynolds 2002），但比完全的奥卡姆有效性要弱。Reynolds (2002)提供了以下一个公式的例子，该公式在奥卡姆分支树中是有效的，但在束树中是可证伪的（在 Burgess 1978 和 Nishimura 1979 中还提供了更多反例）：□G(□p→◊F□p)→◊G(□p→F□p)。这个公式的前提直观上允许构造一个“极限历史”，其中从一个无限的不同历史束中始终成立 □p。这样的极限历史可能在束树中被省略，这引发了关于这些框架的充分性的哲学讨论（参见 Nishimura 1979; Thomason 1984; 和 Belnap et al. 2001）。

在 Zanardo（1985）和 Reynolds（2002）中给出了捆绑树有效性的完整公理化。发现 Ockhamist 有效性的完整公理化更加困难。已经证明 Ockhamist 树的类在捆绑树的类中是不可定义的（Zanardo 等，1999）。在 Reynolds（2003）中，声称有关 Ockhamist 有效性的完整公理化，并进行了概述性证明。在这个系统中，通过一个基于上述公式的无限公理方案来处理新兴历史的问题，并被认为能够保证“极限闭包性质”。然而，完整的证明尚未出现。所提出的公理系统可以在附加文档中找到：

Reynolds 的 OBTL 公理系统

5.4 Peirceanism 和 Ockhamism 的扩展

过去几年中，已经提出并研究了几种对 Peircean 和 Ockhamist 分支时间逻辑的扩展和变体，包括统一这两个框架的逻辑，我们在这里简要提及其中一些。

Brown 和 Goranko（1999）提出了一种结合了 Peircean 和 Ockhamist 思想的逻辑的公理化。Ockhamist 分支时间逻辑的语言通过一种用于替代分支的形式和一种特殊类型的扇形变量进行扩展，用于表示通过一个瞬间的所有历史。

Zanardo（1998）发展了具有不可区分性函数的分支时间逻辑，统一了 Peirceanism 和 Ockhamism。该语言通过模态运算符扩展了 Peircean 时间逻辑，并且公式在所谓的 I 树上进行评估，这些 I 树是具有不可区分性函数 I 的树 T = ⟨T,≺⟩，该函数将 T 中的每个时间瞬间分配给通过该瞬间的历史的集合的一个划分。而在 Ockhamist 语义中，瞬间上的真值相对于历史进行相对化，而在 I 树上的语义中，瞬间上的真值相对于该瞬间的不可区分性等价类，即一组历史进行相对化。Peirceanism 和 Ockhamism 对应于划分是平凡的极限情况，即单例集或单例集的集合。有关详细信息，请参见 Zanardo（1998），以及 Zanardo（2013）和 Ciuni 和 Zanardo（2010），其中将该思想与 stit 代理逻辑的元素相结合。

一个在精神上相似且同样统一了皮尔斯主义和奥卡姆主义的解释是 Rumberg（2016）提出的转换语义。该框架的新特点是，可能的事件过程是从局部未来可能性逐步建立起来的：它们被视为可能的非最大、向下封闭的转换链，其中每个转换在分支点指定了可能的方向。不完整的可能事件过程也变得可用，可以向未来延伸，而语言中除了时间和模态运算符外，还包含了所谓的稳定性运算符，它允许捕捉关于未来在某一瞬间的公式的真值随时间变化的方式。通过将可接受的事件过程范围限制为转换的空集和最大链，皮尔斯主义和奥卡姆主义分别得出。有关详细信息，请参阅 Rumberg（2016；2019）和 Rumberg 和 Zanardo（2019）。在附加文档中提供了简要概述：

转换语义

5.5 计算树逻辑 CTL 和 CTL*

分支时间逻辑在计算机科学中被广泛使用。最流行的是计算树逻辑 CTL 和 CTL ，它们是 Peircean 和 Ockhamist 分支时间逻辑的变体。它们在所谓的计算树类上进行解释，其中每个历史都具有自然数的排序类型。这些树是离散转换系统的树展开自然获得的，并表示在这些系统中出现的可能无限计算。虽然 CTL 在历史上先于 CTL，但现在 CTL 通常被视为 CTL*的一个片段，我们在这里遵循这个惯例。

• 完整的计算树逻辑 CTL_是 Ockhamism 的计算变体，由 Emerson 和 Halpern（1985）引入。CTL_的语言包含（反身版本的）未来运算符 G 和 U（直到）以及下一个时间运算符 X（没有过去运算符），现在在计算树上进行解释。与一般的 Ockhamist 分支时间逻辑一样，评估是相对于即时（这里称为状态）和历史（这里称为路径）进行的。我们注意，在计算机科学中通常假设基于即时的原子命题，即原子命题的赋值仅取决于状态。

• 计算树逻辑 CTL 是 Peirceanism 的计算变体，由 Emerson 和 Clarke（1982）引入。CTL 是 CTL*的片段，其中每个时间运算符 G、U 和 X 都紧接着一个模态运算符 □ 或 ◊，通常表示为路径量词 ∀ 和 ∃。也就是说，CTL 的语言是使用组合的模态性质 ∀Gφ、∀(φUψ)、∀Xφ 和 ∃Gφ、∃(φUψ)、∃Xφ 递归构建的。CTL 的前身是由 Ben-Ari 等人（1983）引入的逻辑 UB，其中不包含 U。

逻辑学 CTL 由于其在模型检查方面具有良好的计算性能而被广泛使用，其在输入公式的大小和输入模型的大小（作为有限转换系统）方面具有线性复杂度。然而，CTL 的表达能力不太强，这导致了其扩展 CTL_的出现。逻辑学 CTL_在表达能力上更加强大，包含了线性时间逻辑 LTL，但其模型检查的复杂度较高（PSPACE），以及决定可满足性的复杂度（2EXPTIME）。有关参考文献和详细信息，请参阅 Emerson（1990）和 Stirling（1992）。

通过将 LTL 的公理替换为其路径量化版本，可以获得 CTL 的完整公理化。有关完整性的证明，请参阅 Emerson（1990）和 Goldblatt（1992）。对于 CTL _，必须添加更多的公理来解释时间和模态运算符的组合，并强制树的极限闭包属性。CTL_的完整公理化是由 Reynolds（2001）获得的，而对于带有过去运算符的 CTL*的扩展，完整性结果是由 Reynolds（2005）建立的。CTL 的公理系统的概要可以在附加文档中找到：

CTL 的公理系统

我们注意到，皮尔逊和奥卡姆分支时间逻辑，以及它们的计算变体，具有有限模型属性并且是可决定的。有关相应逻辑的可决定性证明可以在 Burgess（1980）; Emerson 和 Sistla（1984）; Gurevich 和 Shelah（1985）; Emerson 和 Halpern（1985）; Emerson（1990）; Goldblatt（1992）; Gabbay 等（1994）; Finger 等（2002）; 和 Demri 等（2016）中找到。

6. 时间间隔逻辑

基于瞬间和基于时间间隔的时间模型是两种不同类型的时间本体论，尽管它们在技术上可以彼此还原，但这并不能解决在开发用于捕捉时间推理的逻辑形式主义时出现的主要语义问题：关于时间的命题，以及因此给定逻辑语言中的公式，应该被解释为指向时间瞬间还是时间间隔？

在哲学逻辑文献中，关于基于区间的时间逻辑的提案和发展有很多。重要的早期贡献包括 Hamblin（1972）；Humberstone（1979）；Röper（1980）；和 Burgess（1982b）。后者提供了一个基于区间的时间逻辑的公理化，涉及有理数和实数上的区间之间的时间优先关系。基于区间的时间推理方法在人工智能领域非常突出。一些值得注意的作品包括 Allen 的规划逻辑（Allen 1984），Kowalski 和 Sergot 的事件演算（Kowalski and Sergot 1986），以及 Halpern 和 Shoham 的模态区间逻辑（Halpern and Shoham 1986）。但是，它也在计算机科学的一些应用中出现，例如实时逻辑和硬件验证，特别是 Moszkowski 的区间逻辑（Moszkowski 1983）和 Zhou，Hoare 和 Ravn 的持续时间演算（参见 Hansen and Zhou 1997）。

在这里，我们将简要介绍 Halpern 和 Shoham（1986）提出的命题模态区间逻辑，以下简称 HS。HS 的语言包括一系列形式为 ⟨X⟩ 的一元区间运算符，每个运算符对应于 Allen 在线性时间上的区间关系。相应的符号列在表 1（第 2.2 节）中列出。给定一组原子命题 PROP，通过以下语法递归地定义公式：φ:=p∈PROP∣⊥∣¬φ∣(φ∧φ)∣⟨X⟩φ。

时间间隔逻辑 HS 从基于瞬时的线性时间模型开始，间隔被视为定义的元素。因此，设 T=⟨T,≺⟩ 为一个时间框架，并假设时间优先关系 ≺ 在时间瞬间集合 T 上引出了一个严格的线性顺序。在 T 中，间隔被定义为一个有序对[a,b]，其中 a,b∈T 且 a≤b。T 中所有间隔的集合用 I(T)表示。请注意，该定义允许存在“点间隔”，即起始点和结束点重合的情况，这是 Halpern 和 Shoham（1986）最初提出的建议。有时，只考虑“严格”间隔，排除点间隔。

在基于间隔的时间逻辑中，公式是相对于时间间隔而不是瞬时进行评估的。一个间隔模型是一个三元组 M=⟨T,≺,V⟩，其中包括一个时间框架 T=⟨T,≺⟩ 和一个赋值 V，它将每个原子命题 p∈PROP 赋予在 p 被认为为真的时间间隔集合 V(p)⊆P(I(T))。关于给定间隔[a,b]在间隔模型 M 中的任意公式 φ 的真值是通过对公式的结构归纳定义的，如下所示：

• M,[a,b]⊨p 当且仅当 [a,b]∈V(p)，对于 p∈PROP；

• M，[a，b] ⊭ ⊥；

• M，[a，b] ⊨ ¬φ 当且仅当 M，[a，b] ⊭ φ；

• M，[a，b] ⊨ φ ∧ ψ 当且仅当 M，[a，b] ⊨ φ 并且 M，[a，b] ⊨ ψ；

• M，[a，b] ⊨ ⟨X⟩φ 当且仅当 M，[c，d] ⊨ φ 对于某个区间 [c，d]，使得 [a，b]RX[c，d]，其中 RX 是与模态运算符 ⟨X⟩ 相对应的 Allen 的区间关系（参见表 1）。

也就是说，新的区间运算符在相关的 Allen 关系上具有 Kripke 风格的语义。例如，对于 Allen 关系“meets”，我们有：

M，[t0，t1] ⊨ ⟨A⟩φ 当且仅当 M，[t1，t2] ⊨ φ 对于某个区间 [t1，t2]。

对于每个钻石模态 ⟨X⟩，相应的方框模态被定义为其对偶：[X]φ≡¬⟨X⟩¬φ。有时候，将一个额外的模态常量 π 用于点区间是有用的，其被表示为以下真值定义：

M,[a,b]⊨π 当且仅当 a=b。

一些 HS 模态可以通过其他模态来定义，并且对于严格和非严格语义，已经确定了足够表达所有其他运算符的最小片段。允许通过其他模态来定义某些 HS 模态的完整等价集合在附加文档中呈现：

时间逻辑的互定义性

时间逻辑（HS）具有一千多个表达上非等价的片段，其中仅涉及一些模态运算符，这些片段已经得到了广泛研究（参见 Della Monica 等人 2011 年的最新调查）。HS 及其大部分片段都非常表达力强，相应的有效性概念通常是不可判定的（在一些额外假设下甚至是高度不可判定的，即 Π11-完备）。然而，已经确定了一些相当非平凡的可判定片段。可能最好研究的是邻域区间逻辑，它涉及运算符 ⟨A⟩ 和 ⟨¯¯¯¯A⟩（Goranko 等人 2003 年）。⟨A⟩（以及对称地 ⟨¯¯¯¯A⟩）的一个具体公理是 ⟨A⟩⟨A⟩⟨A⟩p→⟨A⟩⟨A⟩p，即任意两个连续的右邻区间可以合并为一个右邻区间。

除了与 Allen 的二元区间关系相关的一元 HS 区间模态之外，还存在一种自然且重要的操作，即将一个区间分割为两个子区间，从而产生了三元区间关系“chop”，该关系在 Moszkowski（1983 年）中提出并进行了研究。该框架后来在 Venema（1991 年）中扩展为包括“chop”（C）以及两个剩余的“chop”运算符 D 和 T 的逻辑 CDT。逻辑 CDT 在 Venema（1991 年）中完全公理化；另请参见 Goranko 等人（2004 年）和 Konur（2013 年）。

存在一种自然的空间解释，用于间隔时间逻辑，基于这样一个想法：在线性序 L 上定义间隔的点对可以被视为 L×L 平面上的点的坐标。然后，间隔之间的关系被解释为相应点之间的空间关系。这种解释已经成功地用于在空间和间隔逻辑之间转移各种技术结果，例如不可判定性，参见 Venema（1990）和 Marx 和 Reynolds（1999）。

最后，关于间隔时间逻辑和一阶逻辑之间的关系，有几点需要说明。Prior 的基本时态逻辑 TL 到一阶逻辑的标准翻译（在第 3.3 节中介绍）自然地扩展到间隔逻辑，其中原子命题在一阶语言中由二元关系表示。事实证明，HS 的一些片段可以翻译成一阶逻辑的双变量片段 FO2，这最终意味着它们是可判定的。表达能力最强的间隔逻辑是邻域间隔逻辑，已经证明它对于 FO2 是完全表达的（Bresolin 等，2009）。HS 的其他片段需要至少三个不同的变量进行标准翻译。然而，即使是完整的逻辑 HS 的表达能力也不如一阶逻辑的三变量片段 FO3，Venema（1991）证明了逻辑 CDT 的表达能力是完全的。

有关间隔时间逻辑的更多信息，请参见 Halpern 和 Shoham（1986）；Venema（1990）；Goranko 等（2003；2004）；Della Monica 等（2011）；调查 Konur（2013）以及其中的参考文献。

7. 时间逻辑的其他变体

到目前为止，我们已经讨论了传统的时间逻辑家族，但是存在许多变体和替代发展，为各种应用提供了有用的形式化工具。我们在这里简要介绍一些：混合时间逻辑、度量和实时时间逻辑以及量化命题逻辑。

7.1 混合时间逻辑

一个显著的时间逻辑家族，丰富了传统框架，是混合时间逻辑，它将命题时间逻辑与一阶逻辑的元素结合起来，从而大大增加了语言的表达能力。

混合时间逻辑中最重要的概念是名词。名词是特殊的原子命题，因为它们被认为在时间模型的一个瞬间为真。因此，人们可以将名词 a 理解为“现在是 o 点钟”。因此，名词有时也被称为“时钟变量”。名词的概念可以追溯到普赖尔（Prior）（1967 年，第 V 章；1968 年，第 XI 章），他考虑了将瞬间与瞬间命题进行标识的可能性：一个瞬间可以被看作是在该瞬间为真的所有命题的合取。混合时间逻辑的第一个系统性处理是由布尔（Bull）（1970 年）给出的。除了名词，混合语言通常还通过其他句法机制进行扩充，例如满足运算符、名词量词和引用指针，我们在下面简要讨论。前两种机制已经在普赖尔的工作中找到（参见 Blackburn 2006），并且在 Passy 和 Tinchev（1985）中独立重新发明。引用指针直到 Goranko（1996）才被引入，而类似的引用机制在 Alur 和 Henzinger（1994）中找到。

• 满足运算符：满足运算符@i 允许表达一个给定的公式在模型中在由名词 i 表示的时间瞬间为真。也就是说，M,t⊨@iφ 当且仅当 M,V(i)⊨φ，其中 V(i)是名词 i 为真的唯一瞬间。时间模型中一个瞬间的真实性概念被引入到客体语言中。

• 对名词的量词：通过名词量词 ∀i，可以表达在时间模型中，在将时间瞬间分配给 i 的每个可能情况下，给定公式在给定时间瞬间是真实的。更正式地说，对于 M,t⊨∀iφ，当且仅当对于 M 中的任何瞬间 s，M[i→s],t⊨φ，其中 M[i→s]是通过重新分配 i 的指示为 s 而得到的模型。第一阶量化的全部能力被引入到时间语言中，同时保留了它的命题优点的许多特性。

• 引用指针：引用指针 ↓i 通常也被称为“绑定器”，因为它们将名词 i 的值绑定到当前评估的瞬间。在时间模型中，当且仅当名词 i 表示 t 时，公式 ↓iφ 在给定瞬间 t 是真实的，当且仅当 φ 在 t 是真实的。也就是说，对于 M,t⊨↓iφ，当且仅当 M[i→t],t⊨φ。引用指针提供了一种引用当前时间瞬间的机制，即说“现在”。有关“现在”的系统逻辑处理，请参见 Kamp（1971）。

可以被视为混合时间逻辑运算符的其他运算符包括全局性态度、差异性态度和命题量词。全局性态度 A 表示给定公式在时间模态的每个瞬间都是真实的，从而捕捉了模型中真实性的全局概念：对于 M,t⊨Aφ，当且仅当 M⊨φ。另一方面，差异性态度 D 表示给定公式在某个其他瞬间是真实的。请注意，这两种模态都抽象了底层的可达性关系。命题量词 ∀p 将第二阶量化引入命题语言中，我们将在下面的第 7.3 节中讨论它们。

混合语言非常表达力强。以下只是两个例子：

• 在 TL 中无法表达的优先关系的非自反性可以在具有名词和满足运算符@i 的语言中表示为@iG¬i。

• 运算符 S 和 U 可以在具有名词和绑定器的语言中定义为 φUψ:=↓iF(ψ∧H(Pi→φ))，S 也是如此。

虽然混合逻辑的较弱版本——带有名称、满足操作符、全域模态和差异模态——仍然是可决定的，但更具表达力的版本——带有名称或参考指针的量词——通常是不可决定的。有关详细信息，请参阅 Goranko（1996）；和 Areces 和 ten Cate（2006）。

分支时间版本的混合时间逻辑也得到了研究。有关混合时间逻辑的各种类型及其历史发展的概述，请参阅 Blackburn 和 Tzakova（1999）以及有关混合逻辑的条目。

7.2 度量和实时时间逻辑

有关度量时间逻辑的研究可以追溯到普赖尔（Prior）（参见普赖尔 1967 年第六章）。他使用符号 Pnφ 表示“在 n 个时间单位之前， φ 是成立的”（即 φ 在 n 个时间单位之前是成立的），使用符号 Fnφ 表示“在 n 个时间单位之后， φ 将成立”（即 φ 将在 n 个时间单位之后成立）。这些运算符假设时间具有一定的度量结构，并且可以被划分为时间单位，这些单位可以与时钟时间（例如小时、天、年等）相关联。例如，如果相关单位是天，则运算符 F1 表示“明天”。

普赖尔指出 Pnφ 可以定义为 F(−n)φ。当 n=0 时，相应地表示现在时态。度量运算符验证了如下的组合原则：

FnFmφ→F(n+m)φ。

时间运算符的度量和非度量版本之间的相互关系可以通过以下等价关系来捕捉：

Pφ≡∃n(n <0∧Fnφ)Fφ≡∃n(n> 0∧Fnφ)Hφ≡∀n(n <0→Fnφ)Gφ≡∀n(n> 0→Fnφ)。

关于度量时间的基于瞬间的时间逻辑的研究可参考 Rescher 和 Urquhart（1971 年，第 X 章）；Montanari（1996 年）；以及 Montanari 和 Policriti（1996 年）。关于度量区间逻辑，请参见 Bresolin 等人（2013 年）。

在实数结构上，已经提出了各种度量扩展的时间逻辑，从而产生了所谓的实时逻辑。这些逻辑引入了额外的运算符，例如以下运算符，允许对示例句子“每当 p 在未来成立时，q 将在三个时间单位后成立”的不同形式化：

• 有时间限制的运算符，例如：G(p→F≤3q);

• 冻结量词（类似于混合逻辑的引用指针），例如：Gx.(p→Fy.(q∧y≤x+3));

• 时间变量上的量词，例如：∀xG(p∧t=x→F(q∧t≤x+3)).

这种实时扩展通常非常表达力，经常导致具有不可判定决策问题的逻辑学。通过放宽涉及精确时间持续的“准时性”要求，以涉及时间间隔的要求来恢复可判定性。有关详细信息，请参见例如 Koymans（1990）；Alur 和 Henzinger（1992；1993；1994）以及 Reynolds（2010；2014）关于实时线性时间逻辑 RTL，以及调查 Konur（2013）。

7.3 量化命题时间逻辑

命题时间逻辑可以通过对原子命题进行量词扩展（参见 Rescher 和 Urquhart 1971 年，第 XIX 章）。从语义上讲，这些量词涵盖了各个原子命题的所有赋值，因此等同于一阶单调量词。由此产生的语言非常表达力强，相应的逻辑通常是不可判定的（通常甚至不可递归公理化）。值得注意的扩展包括 QPTL 逻辑，即 LTL 的量化命题版本（虽然可判定，但复杂度非元素级别），以及 CTL*的扩展（参见 French 2001 年）。关于量化命题时间逻辑 QPTL（带有或不带有过去运算符）的完备公理系统和可判定性结果已在 Kesten 和 Pnueli（2002 年）以及 French 和 Reynolds（2003 年）中提出。

8. 一阶时间逻辑

对象存在于时间中，并且它们随时间改变其属性。命题时间逻辑不足以捕捉世界的这种动态方面，因为命题时间逻辑模型中与时间瞬间相关的一切只是一组被声明为真的抽象原子命题。相反，需要的是一个完整的世界时间历史模型，其中的对象可能具有某些属性并且处于某些关系中。因此，语言应包含对象的名称、变量和量词范围，以及用于表示属性和关系的谓词，以充分描述世界在给定时间瞬间的状态 - 除了用于推理世界随时间变化的时间运算符。这就是一阶时间逻辑所提供的。

8.1 存在与时间的量化

存在于时间是时间哲学中的一个重要主题。通常，物体在某个时间点产生，并在以后的某个时间点消失。但是，物体在时间中存在是什么意思？只有当前存在的物体存在吗，就像现在主义者所认为的那样，还是存在应该以更广泛的意义来理解，包括过去和未来的物体，就像永恒主义者所主张的那样？现在主义和永恒主义之间的争议伴随着对持续性的辩论，即物体如何在时间中存在的问题。物体在每个存在的瞬间都完全存在吗？这被称为持续论的观点，还是通过在不同的时间瞬间具有不同的时间阶段来持续存在？这被称为持续论的观点。有关这些辩论的详细概述，请参见 Dyke 和 Bardon（2013），Meyer（2013），以及有关时间，时间部分和时间内身份的条目。

在一阶时间逻辑的背景下，关于物体在时间中的存在和它们随时间的身份的类似问题以不同的方式出现。当涉及到时间性和量化的相互作用时，这些问题变得尤为重要。例如，“一个哲学家将成为国王”的句子可以有几种不同的解释方式，例如[5]

• ∃x(哲学家(x)∧F 国王(x)) 现在是哲学家的人将来会成为国王。

• ∃xF(哲学家(x)∧ 国王(x)) 现在存在着一个人，将来某个时候他既是哲学家又是国王。

• F∃x(哲学家(x)∧F 国王(x)) 将来会有一个人，他是一个哲学家，然后会成为一个国王。

• F∃x(哲学家(x)∧ 国王(x)) 将会存在一个人，他同时是一个哲学家和一个国王。

上述给出的解释假设量化的领域始终相对于一个时间点，并且同一个个体可能存在于多个时间点。为了实现这些解释，我们需要在模型中引入一个本地对象域 D(t)用于每个时间点 t，将量词的范围限制在该域内，并且在不同的时间点上识别相同的对象。

此外，上述例子表明，在给定的时间点上，局部领域确切包含那些在该时间点实际存在的个体。然而，从逻辑学的角度来看，与时间点相关联的局部领域有不同的思考方式，这反映了时间存在的不同概念。这里有四个自然的选择：

1. 对象在某个时间点产生，并在以后的时间点消失，即它们实际上只在一定的时间段内存在。这个想法可以通过假设在给定的时间点上，局部领域包括那些当前存在于该时间点的对象来形式化捕捉。因此，对象属于那些它们实际存在的时间点的局部领域，并且局部领域随时间而变化。

2. 对象实际上在一段时间内存在，但一旦它们停止实际存在，它们仍然存在于世界的时间历史中。根据这种观点，一个时间点的局部领域不仅包括当前存在的对象，还包括所有过去的对象。也就是说，随着时间的推移和新对象的产生，局部领域增加。

3. 或者，人们可以认为所有将来存在的对象最初都是世界的时间历史的一部分，但一旦它们停止实际存在，就会退出。从技术上讲，这意味着在某一瞬间，局部领域包括所有现在和未来的对象。因此，随着时间的推移和对象的消失，局部领域会减少。

4. 过去、现在和未来的对象同样存在。这是永恒主义意义上存在的概念。一个形式上捕捉这个想法的方法是要求与时间瞬间相关联的局部领域包含世界时间历史的所有对象。因此，局部领域随时间保持不变。

一个在概念上不同但在技术上密切相关的问题涉及量化的范围。在时间设置中，我们量化什么？

• 只针对当前时间瞬间存在的对象，如上述例子所假设的吗？

• 针对世界的时间历史中所有当前、过去和未来的对象吗？

采用菲廷和门德尔松（1998）对时间情况下的术语“实在主义量化”和“可能主义量化”，我们可以将第一种量化称为现在主义量化，并将后者称为永恒主义量化。根据这些选项之间的选择，例如句子“每个人都是在 1888 年之后出生的”可以是真或假。如果我们只对当前活着的人进行量化，那么它是真的；但如果我们对世界的时间历史中的所有人进行量化，包括曾经存在的人，那么它是假的。在这里还涉及到另一个问题，即虚构实体，如圣诞老人或皮皮龙斯托金，它们在任何时间瞬间实际上并不存在。然而，从更广义上来说，它们可以说是存在的，并且人们可能希望将它们纳入量化的范围之内。我们在这里搁置这个问题，并将读者引向关于自由逻辑的条目，自由逻辑允许引用不存在的实体（另见第 8.6 节）。

这里涉及到存在和量化的相互关系的许多问题与模态一阶逻辑中的众所周知的问题相对应，这些问题的讨论早在弗雷格和罗素开始，并在 20 世纪 40 年代至 50 年代达到高峰，由 R. Barcan-Marcus、R. Carnap、W. Quine、R. Montague 等人的作品引起（参见模态逻辑条目）。一阶模态逻辑中的一个核心问题与所谓的巴尔坎公式的有效性或无效性有关，这个公式的时间版本直观地说：“如果将来的某个时刻将会有某个是 Q 的东西，那么现在将会有某个将来的某个时刻是 Q 的东西。”这个陈述是否保证为真关键取决于如何构建时间的各个瞬间的局部域以及我们的量词范围。更重要的是，时间逻辑产生了巴尔坎公式的两个版本，一个是针对未来的，一个是针对过去的。

8.2 FOTL 的语言和模型

一阶时间逻辑（FOTL）的基本语言本质上是给定的一阶语言的扩展，通过运算符 P 和 F。在命题时间逻辑中，原子命题是非结构化的实体，而在一阶时间逻辑中，原子公式是由表示个体的项和表示关系的谓词符号构建的，并且该语言配备了范围为个体的量词。（一阶逻辑的简要概述在附加文档《一阶关系结构和语言》中提供。）在接下来的内容中，我们考虑带有相等性的关系型一阶语言（无函数符号）上的 FOTL。公式集的定义如下：

φ := R(τ1,…,τn) | τ1=τ2 | ⊥ | ¬φ | (φ∧φ) | ∀xφ | Pφ | Fφ,

其中 R(τ1,…,τn)和 τ1=τ2 是原子公式。真值功能连接词 ∨、→和 ↔，以及时间操作符 H 和 G 可以按照通常的方式定义。此外，∀ 的对偶 ∃ 由 ∃xφ:=¬∀x¬φ 定义。

FOTL 的模型基于时间框架，其中每个时间点与一个一阶关系结构相关联。形式上，一阶时间模型是一个五元组：M=(T,≺,U,D,I)，其中：

• T=⟨T,≺⟩ 是一个时间框架；

• U 是模型的全局域（宇宙）；

• D:T→P(U) 是一个域函数，将每个时间点 t∈T 分配给一个局部域 Dt⊆U，使得 U=⋃t∈TDt。[ 6]

• 我是一个解释函数，为每个 t∈T 分配：

  • 对于每个常量符号 c，分配一个对象 It(c)∈U；

  • 对于每个 n 元谓词符号 R，分配一个 n 元关系 It(R)⊆Un。

注意，常量和谓词符号的解释是局部定义的，即相对于给定的时间点，而相应的扩展范围涵盖全局域。这种方法允许引用当前不存在的对象，并能够正确处理跨时间关系，例如在句子“我的一个朋友是威廉征服者的追随者的后代”中。

四元组 F=(T,≺,U,D)被称为模型 M 的增强时间框架。由于该模型被认为代表了世界的时间演化，底层增强时间框架中不同时间点的局部域必须适当连接。对于基于增强时间框架的任何一阶时间模型，有四种自然情况需要区分：

1. 变化的域：没有限制适用；

2. 扩展（增加）领域：对于所有的时间 t，t′∈ 时间，如果 t≺t′，那么 Dt⊆Dt′；

3. 收缩（减少）领域：对于所有的时间 t，t′∈ 时间，如果 t≺t′，那么 Dt′⊆Dt；

4. 局部恒定领域：对于所有的时间 t，t′∈ 时间，如果 t≺t′，那么 Dt=Dt′。

因此，一个增强的时间框架 F 在本地具有恒定的域，当且仅当它具有扩展和收缩的域。特别地，我们说 F 具有恒定的域，如果所有的本地域与全局域相同。由于全局域需要是所有本地域的并集，具有本地恒定域意味着在时间瞬间集合形成一个时间上连通的整体的情况下具有恒定的域。

在这里区分的四种情况的自然解释是通过讨论 8.1 节中的时间存在的四个概念来实现的。

8.3 FOTL 的语义

正如命题时间逻辑中一样，FOTL 的公式在一阶时间模型中在时间瞬间局部进行评估。然而，由于 FOTL 的公式可能包含变量，真值的概念不仅相对于模型和时间瞬间，还相对于变量赋值。我们用 VAR 表示 FOTL 的个体变量集合，用 TERM 表示个体项（即变量和常量）的集合。

给定一个一阶时间模型 M=(T,≺,U,D,I)，M 中的变量赋值是一个映射 v:VAR→U，它将 VAR 中的每个变量 x∈VAR 映射到模型的全局域 U 中的一个元素 v(x)。这样的赋值 v 可以唯一地扩展为一个项估值 v:T×TERM→U，具体定义如下：vt(x):=v(x)，vt(c):=It(c)。请注意，变量赋值是全局定义的，而常量符号的估值取决于相应的时间瞬间。

在给定的一阶时间模型 M 中，对于变量赋值 v，在给定的时间瞬间 t 上，FOTL 的任意公式 φ 的真值（表示为 M,t⊨vφ）可以按如下递归方式定义：

• M,t⊨vR(τ1,…,τn) 当且仅当 (vt(τ1),…,vt(τn))∈It(R), 对于任意的 n 元谓词符号 R 和项 τ1,…,τn∈TERM;

• M,t⊨vτ1=τ2 当且仅当 vt(τ1)=vt(τ2), 对于任意的项 τ1,τ2∈TERM;

• M,时间 ⊭v⊥;

• M,时间 ⊨v¬φ 当且仅当 M,时间 ⊭vφ;

• M,时间 ⊨vφ∧ψ 当且仅当 M,时间 ⊨vφ and M,时间 ⊨vψ;

• M,t⊨vPφ 当且仅当 存在 t′∈T，使得 t′≺t，M,t′⊨vφ；

• M,t⊨vFφ 当且仅当 存在 t′∈T，使得 t≺t′，M,t′⊨vφ；

• M,t⊨v∀xφ 当且仅当 …

  • 现时主义量化：对于每个 a∈Dt，…M,t⊨v[a/x]φ；

  • 永恒主义量化：对于每个 a∈U，…M,t⊨v[a/x]φ；

其中 v[a/x]是变量赋值 v 的变体，使得 v a/x=a。

正如我们之前提到的，时间逻辑中有两种自然的量化方法：现在主义量化和永恒主义量化。从技术上讲，现在主义量化意味着在给定的时间点上对局部域进行量化，而永恒主义量化被解释为对全局域进行量化。相应的语义子句对于 ∀ 的双重量化如下所示：

• M,t⊨v∃xφ 当且仅当…

  • 现在主义量化：…M,t⊨v[a/x]φ，其中 a∈Dt。

  • 永恒主义量化：…M,t⊨v[a/x]φ，其中 a∈U。

需要注意的是，现在主义量化自然地与具有变化域的一阶时间模型相关联，而基于永恒主义量化的语义中，局部域并不起任何重要作用。实际上，从技术角度来看，永恒主义量化等同于假设模型具有恒定域，即所有局部域等于全局域。此外，在恒定域模型中，基于现在主义量化的语义与基于永恒主义量化的语义相一致。因此，现在主义量化暗示了一个变化域语义，而与永恒主义量化相关的语义是一个恒定域语义，在接下来的内容中，我们将这些表达式互换使用。

在这些语义中，对于模型 M，FOTL 公式 φ 在该模型的每个时间点上对于每个变量赋值都为真时，被称为在该模型中有效；在增强的时间框架中，如果在该框架上的每个模型中都有效，则被称为在该增强的时间框架中有效；如果在每个模型中都有效，则被称为有效。

采用一种或另一种量化方法会影响有效性的概念，即使对于非时间性原则也是如此。例如，句子 ∃x(x=c)在一阶逻辑中是有效的，在常量域语义中也是有效的，但在变动域语义中不再有效，因为分配给常量 c 的对象可能不属于局部域。另一个区分这两种语义的来自纯一阶逻辑的原则是全称实例化方案（其中 τ 是任意自由替代 x 在 φ 中的项）：∀xφ(x)→φ(τ)，同样，在常量域语义中是有效的，但在变动域语义中是无效的，原因类似。然而，这两种语义之间的主要区别在于涉及时间运算符和量化的相互作用的原则，例如 Barcan 公式方案及其逆。在接下来的两节中，我们将更详细地研究各自语义中一些重要的有效性和非有效性。

8.4 永恒主义量化和常量域语义

让我们在常量域语义中（即具有永恒主义量化的语义）看一些 FOTL 的有效性和非有效性。我们用 ⊨CD 表示在常量域语义中的有效性。

• 所有有效的一阶公式的 FOTL 实例都是 CD-有效的。

• 特别地，全称实例化原则是 CD-有效的： ⊨CD∀xφ(x)→φ(τ)，对于任何在 φ 中自由替换 x 的项 τ。

• 未来的巴尔坎公式[7]方案，BFG，是 CD-有效的： ⊨CD∀xGφ(x)→G∀xφ(x) 或者，等价地， ⊨CDF∃xφ(x)→∃xFφ(x)。

• 逆向未来巴尔坎公式方案，CBFG，是 CD-有效的： ⊨CDG∀xφ(x)→∀xGφ(x) 或者，等价地， ⊨CD∃xFφ(x)→F∃xφ(x)。

• 一些重要的非有效性包括： ⊭CD∀xFφ(x)→F∀xφ(x)和 ⊭CDG∃xφ(x)→∃xGφ(x)。

对于上述方案的过去版本，类似的主张也成立，其中用 H 和 P 代替 G 和 F。关于具有恒定域语义的最小 FOTL 的公理系统以及其中的一些重要定理，可以在附加文档中找到。

极小常量域语义下的 FOTL(CD)公理系统

8.5 现时主义量化和变动域语义

在变动域语义中，自由变量范围是全局域，而量词则具有现时主义的解释，即它们仅量化局部域。因此，在变动域语义中，一些在常量域语义中成立的公式不再成立。最重要的是，变动域语义使得全称实例化 ∀xφ(x)→φ(τ) 以及未来和过去的 Barcan 公式模式及其逆否命题无效。我们用 ⊨VD 表示在变动域语义中的有效性。

实际上，巴尔坎公式模式 BFG 和 BFH 及其逆向模式 CBFG 和 CBFH 对应于对本地域的条件。对于任何增强的时间框架 F，以下条件成立：

• F 具有扩展域当且仅当 F⊨VDBFH 当且仅当 F⊨VDCBFG；

• F 具有收缩域当且仅当 F⊨VDBFG 当且仅当 F⊨VDCBFH。

注意，未来的巴尔坎方案 BFG 在语义上对应于相反的过去巴尔坎方案 CBFH，反之亦然。由上述可知，增强的时间框架 F 在本地具有恒定的域，当且仅当以下任一公式在 F 中是 VD-有效的：BFG∧BFH，CBFG∧CBFH，BFG∧CBFG 或 BFH∧CBFH。

在补充文件中提供了一个具有变域语义的最小 FOTL 的公理系统：

用于具有变域语义的最小 FOTL 的公理系统 FOTL(VD)

8.6 存在谓词

虽然现在主义和永恒主义是时间哲学中的两种替代理论，但它们各自的技术表现是相互不可约的。一方面，通过强加过去和未来巴尔坎公式模式及其逆命题有效的约束条件，可以从具有现在主义量化的变域语义中获得具有永恒主义量化的恒定域语义。另一方面，通过在 FOTL 语言中添加一个“存在于当前时间瞬间”的存在谓词，可以在恒定域语义中模拟变域语义，该谓词可以在变域语义中通过 E(τ):=∃x(x=τ)来定义。

有了存在谓词，句子“存在一个签署《独立宣言》的人”可以以两种不同的方式形式化：∃x(man(x)∧P(signs(x)))和 ∃x(E(x)∧man(x)∧P(signs(x)))。前者在具有永恒主义量化的恒定域语义中在当前瞬间为真，而后者在该语义中目前为假，但在 1777 年是真的。

概括而言，对于 FOTL 的每个公式 φ，其在扩展语言中的 E 相对化可以通过将 φ 中的每个 ∀x 的出现替换为“∀x(E(x)→...)”，并将每个 ∃x 的出现替换为“∃x(E(x)∧...)”来获得。然后有以下结论：对于任何不包含 E 的 FOTL 句子 φ，如果 φ 在变动域语义中有效，则其 E 相对化在恒定域语义中也有效。从哲学角度来看，仍然存在一个问题，即存在是否是一个合法的谓词。可以沿着自由逻辑的思路，按照补充文件中的概述，获得带有存在谓词的最小 FOTL 的公理系统：

带有 E 的最小 FOTL 的公理：自由逻辑版本

8.7 专有名词和确定描述

在一阶时间逻辑中出现的另一个问题与个体术语的解释有关。根据我们处理的术语类型，我们可能希望允许它们的解释随时间变化，也可能不希望。

在上述概念中，变量赋值是全局定义的，因此各个变量在任何时间都指代同一对象。另一方面，常量符号的解释是局部指定的，相对于一个时间点，尽管其扩展范围涵盖全局域。从哲学角度来看，将常量符号视为适当的名称或刚性指示符似乎是自然的，即对它们的解释在不同时间上是恒定的附加要求。然后，常量符号可以用于在时间上标识一个对象。例如，将 a 视为亚里士多德的名称，句子“亚里士多德存在但不再存在”可以在变动域语义中形式化为 P∃x(x=a)∧¬∃x(x=a)。

如果常量被视为刚性指示符，则恒等性必要性原则 τ1=τ2→A(τ1=τ2)对变量和常量都有效（回想一下 Aφ=Hφ∧φ∧Gφ）。然而，语言中可能还包含使该原则失效的个别术语。一个核心例子是确定描述，例如“教皇”，它可能在不同的时间指代不同的对象。重要的是，专有名词和确定描述需要不同的语义处理，并且不能自由地互相替换。例如，“教皇自 1929 年以来一直是梵蒂冈城的主权者”是真实的，而“豪尔赫·马里奥·贝尔戈里奥自 1929 年以来一直是梵蒂冈城的主权者”是错误的。此外，在时间设置中，问题是如何处理指称不再存在或尚未存在的确定描述，例如“2050 年在南非出生的第一个孩子”。在分支时间设置中，时间和模态性结合在一起，问题变得更加复杂。请注意，例如，一些在时间上刚性的确定描述可能在模态上是非刚性的。有关在时间逻辑背景下的确定描述的更多信息，请参见 Rescher 和 Urquhart（1971 年，第 XIII 章和第 XX 章）以及 Cocchiarella（2002 年）。

处理明确描述的一种方法是从外延的角度转向内涵的解释个体术语。也就是说，不是在每个时间点为每个术语分配一个外延，即域中的一个对象，而是为每个术语分配一个内涵，即从时间点到对象的函数。一个通用的框架，其中个体术语被分配外延和内涵，是 Belnap 和 Müller（2014a; 2014b）提出的 Case Intensional First-Order Logic（CIFOL）。在 CIFOL 中，身份是外延的，断言是内涵的，并且个体可以在时间上被识别而不使用刚性指定。该框架还与关于持续性的辩论背景下的具体对象的精确性质保持形而上学中立。

8.8 关于一阶时间逻辑的一些技术结果

一阶时间逻辑非常表达力强，但这通常伴随着高昂的计算代价：这些逻辑在推理上非常复杂，并且通常高度不可判定（参见 Merz 1992; Gabbay 等人 1994; Hodkinson 等人 2002）。例如，具有常量域语义的一阶时间逻辑，仅具有两个变量和一元关系符号，不仅是不可判定的，而且甚至不可递归公理化（参见 Börger 等人 1997; Hodkinson 等人 2000）。

迄今为止，已经确定和研究了很少的可公理化和可决定的自然的一阶时间逻辑片段。这些片段包括具有 Since 和 Until 的一阶时间逻辑，适用于所有线性时间流和有理数序（Merz 1992; Reynolds 1996），FOTL 的 T（FOs）片段，其中时间运算符可能不出现在量词的范围内（Gabbay 等人 1994 年，第 14 章），以及单调片段，只允许在时间运算符的范围内具有最多一个自由变量的公式（参见 Hodkinson 等人 2000 年; 2001 年; 2002 年和 Wolter 和 Zakharyaschev 2002 年）。然而，正如后一篇论文所示，具有相等性的单调片段已不再是递归可公理化的。有关 FOTL 适当限制片段的决定性结果，请参见 Hodkinson 等人（2000 年）。有关技术参考文献，请参见 Gabbay 等人（1994 年，第 14 章）和 Kröger 和 Merz（2008 年）。有关一阶模态逻辑的完备性结果，还请参见 Fitting 和 Mendelsohn（1998 年）和模态逻辑的条目。

有关一阶模态和时间逻辑的进一步哲学讨论，请参见 Rescher 和 Urquhart（1971 年，第 XX 章）; McArthur（1976 年）; Garson（1984 年）：Linsky 和 Zalta（1994 年）; van Benthem（1995 年，第 7 节）; Fitting 和 Mendelsohn（1998 年）; Wölfl（1999 年）; Cocchiarella（2002 年）; 以及 Lindström 和 Segerberg（2006 年）。

9. 结合时间和其他逻辑

逻辑学可以用来推理世界中动态变化的方面，时间在许多领域中起着重要作用。例如，在认知逻辑中研究的知识概念，代理逻辑中的行动概念，或者空间逻辑中的物理概念都与时间有着密切的关系。因此，将时间维度添加到这些逻辑中，并为相应的语言配备适合捕捉相关变化概念的时间运算符是自然而然的。

从技术角度来看，有几种组合模型和逻辑系统的方法：乘积、融合等（参见有关组合逻辑的条目）。这些构造为逻辑添加了不同的时间化机制，并引发了关于逻辑属性的传递的通用问题，例如公理化、完备性、可决定性。例如，可决定性通常在融合中保留，而在逻辑系统的乘积中通常会丧失。有关时间化逻辑系统和时间化逻辑属性的一般讨论，请参见 Finger 和 Gabbay（1992；1996）；Finger 等人（2002）；以及 Gabbay 等人（2003）。在这里，我们只介绍并简要讨论一些最受欢迎的时间化逻辑系统的案例。

9.1 时间-认知逻辑

时间-认识逻辑将时间逻辑和（多智能体）知识逻辑结合在一起。通过将认识模态 K（“智能体知道”）与时间运算符相结合，可以自然地表达一些有趣的属性，例如完美回忆：Kφ→GKφ（如果智能体现在知道 φ，那么智能体将永远知道 φ）和无学习：FKφ→Kφ。

在 20 世纪 80 年代，开发了各种时间-认识逻辑，Halpern 和 Vardi（1989）进行了一项统一研究。他们在所谓的解释系统上考虑了 96 种时间-认识逻辑，即在每个智能体的状态空间上具有认识不可区分关系的转换系统中的运行集合。这种多样性基于几个参数：智能体数量（一个或多个），语言（有或没有共同知识），时间的形式模型（线性或分支时间），回忆能力（无回忆，有界回忆或完美回忆），学习能力（学习或无学习），同步性（同步或异步），唯一初始状态。根据这些参数的具体选择，这些逻辑的决策问题的计算复杂性范围非常广泛，从 PSPACE-complete 到高度不可判定（Π11-complete）。有关详细信息，请参见 Halpern 和 Vardi（1989）；Fagin 等人（1995）；以及更近期的 van Benthem 和 Pacuit（2006），该文献调查了一些时间-认识逻辑的可判定性和不可判定性结果，并说明了时间与其他模态的组合对计算复杂性的影响。

9.2 时间逻辑和代理逻辑

时间推理是关于代理人及其行为的推理的重要方面。在哲学研究中，最有影响力的代理逻辑家族是所谓的 stit 逻辑家族，起源于 Belnap 和 Perloff（1988）的工作。这些逻辑包含了 stitφ 形式的公式，读作“代理人确保 φ”，它允许我们推理代理人的行为选择如何影响世界。stit 逻辑的最初版本不涉及时间运算符。然而，它们的语义是基于 Ockhamist 分支时间模型，其中代理人在给定时间点的选择集由通过该时间点的历史的划分表示。直观地说，对于给定的时间点 t 和给定的历史 h，如果在时间点 t 相对于所有在相应选择单元中的历史中 φ 都为真，则 stitφ 在该时间点 t 上为真，这意味着代理人在时间点 t 相对于历史 h 的选择保证了 φ 的真实性。有关 stit 逻辑的各种形式及其历史发展的详细讨论，请参见 Belnap 等人（2001）和有关行动逻辑的条目。Broersen（2011）和 Lorini（2013）提出了 stit 逻辑的时间扩展：在 Broersen（2011）中，stit 运算符与 Next Time 运算符 X 结合成一个单一运算符，要求在下一步中实现目标，而在 Lorini（2013）中，stit 运算符和时间运算符是分开处理的。

另一个重要的时间逻辑学家族是交替时间逻辑 ATL 和 ATL _，由 Alur 等人（2002 年）引入。ATL 和 ATL_是计算树逻辑 CTL 和 CTL_的多智能体扩展，它们已成为多智能体系统中战略推理的流行逻辑框架。交替时间逻辑通过战略路径量词 ⟨⟨C⟩⟩φ 丰富了语言，直观地表示“联盟 C 有一种集体策略，保证在该集体策略启用的每条路径上实现目标 φ”，其中目标 φ 是一个时间公式。尽管 stit 逻辑建立在相当抽象的历史概念上，ATL 和 ATL_是在所谓的并发博弈结构上解释的，其中路径被视为由所有智能体的集体行动引起的离散转换生成的后继状态序列。ATL 和 stit 理论的组合在 Broersen 等人（2006 年）中得到了发展。分支时间逻辑 CTL 和 CTL_可以看作是 ATL 和 ATL_的单智能体版本。尽管后者更具表达能力，但它们通常保留了前者的良好计算性质。有关更多详细信息，请参阅 Alur 等人（2002 年），以及 Goranko 和 van Drimmelen（2006 年），其中为 ATL 建立了完整的公理化和可决定性结果。Demri 等人（2016 年，第 9 章）提供了一个从时间逻辑角度对 ATL 的一般介绍。

9.3 空间-时间逻辑

空间和时间在物理世界中密切相关，并且在现代物理理论中它们已经变得不可分割。早期的物理理论，以牛顿的经典力学为高潮，假设时间是独立于空间的绝对概念，而爱因斯坦的相对论理论将时间和空间视为密不可分，正如 Minkowski 的四维时空流形所建模的那样。

关于时空的综合逻辑推理在 Rescher 和 Urquhart（1971 年，第 XVI 章）中进行了讨论。在 Goldblatt（1980 年）中，研究了闵可夫斯基时空的 Diodorean 模态逻辑，并证明了它正好是模态逻辑 D4.2；Uckelman 和 Uckelman（2007 年）提供了进一步的结果。对相对论理论的逻辑研究也进行了，例如 Andréka 等人（2007 年）。

在人工智能领域，时空推理在过去几十年中一直在积极发展，特别是在时空数据库、本体论和约束网络的背景下。这里的主要关注点是时空模型的逻辑特征化、表达能力和计算复杂性（Gabelaia 等人，2005 年；Kontchakov 等人，2007 年）。

另一个有趣的研究方向是由 Belnap（1992 年）提出的分支时空理论引发的。这个理论与 Prior 的分支时间理论与线性时间的关系类似；也就是说，它将时空推理与不确定性相结合。参见 Müller（2013 年）和 Placek（2014 年），其中研究了分支时空的拓扑结构与相对论理论的背景。关于分支时空的广泛概述可以在 Belnap 等人（2022 年）中找到。

9.4 时间描述逻辑学

描述逻辑学本质上是模态逻辑学的变体。它们涉及概念（一元谓词）和角色（二元谓词），用于描述各种本体论和其中概念之间的关系（参见例如 Baader 和 Lutz 2006）。描述逻辑可以以各种方式进行时间化。详细信息请参见 Artale 和 Franconi（2000）；Wolter 和 Zakharyaschev（2000）；以及 Lutz 等人（2008）。

9.5 时间逻辑学和其他非经典逻辑学

时间推理可以自然地与各种非经典逻辑系统相结合，例如产生了多值时间逻辑（Rescher 和 Urquhart 1971，第十八章），直觉主义时间逻辑（Ewald 1986），建设性和抗矛盾时间逻辑（Kamide 和 Wansing 2010; 2011），概率时间逻辑（Hart 和 Sharir 1986; Konur 2013）等等。

逻辑推理和决策方法适用于时间逻辑

在过去的 50 年里，广泛的研究和大量的出版物已经为这里提到的时间逻辑以及更多的时间逻辑开发了各种逻辑推理系统和决策方法。希尔伯特风格的公理系统是时间逻辑最常见的逻辑推理系统，但也有许多完备的语义表格、序列演算和基于解析的系统被提出。关于时间逻辑的推理系统的一些通用参考资料（除了本文其他地方提到的更具体的参考资料）包括：Rescher 和 Urquhart（1971）；McArthur（1976）；Burgess（1984）；Emerson（1990）；Goldblatt（1992）；Gabbay 等人（1994）；van Benthem（1995）；Bolc 和 Szalas（1995）；Gabbay 和 Guenthner（2002）；Gabbay 等人（2003）；Fisher 等人（2005）；Blackburn 等人（2006）；Baier 和 Katoen（2008）；Kröger 和 Merz（2008）；Fisher（2011）；Demri 等人（2016）。

在确定给定逻辑的给定公式是否在为该逻辑提供的语义中有效（或可满足）时，最重要的逻辑决策问题之一是。对于决定可满足性而言，基于表格的方法特别高效且实用，这些方法源自 Beth、Hintikka、Smullyan 和 Fitting 的开创性工作。如果提供了一个被测试可满足性的输入公式，这些方法基于对满足模型（或证伪反模型）的系统搜索，并且它们保证在存在这样的模型时找到这样的模型。基于表格的方法已成功地用于各种时间逻辑的构造性可满足性测试。有关许多时间逻辑的表格系统，请参见 Goré（1999）的调查，更具体地说：Ben-Ari 等人（1983）的分支时间逻辑 UB；Emerson 和 Halpern（1985）的计算树逻辑 CTL；Wolper（1985）的线性时间时间逻辑 LTL；Kontchakov 等人（2004）关于时间化表格；Reynolds（2007）关于带捆绑树语义的 CTL；Goranko 和 Shkatov（2010）关于 ATL；Reynolds（2011）关于完整的计算树逻辑 CTL*；Reynolds（2014）关于实时时间逻辑 RTL 等。

其他在计算机科学中被证明在决定可满足性以及模型检查时间逻辑方面实际上是有效的方法是基于自动机的方法，这些方法自从 1990 年代初以来一直在积极发展。这些方法将时间公式转化为无限字（用于线性时间逻辑）或无限树（用于分支时间逻辑）上的自动机，并将逻辑的模型表示为输入对象（无限字或树）用于它们关联的自动机。因此，公式的可满足性等价于关联自动机的语言非空。这些方法基于关于自然数的单调二阶理论（由 Büchi 提出）和无限二叉树的可判定性的经典结果（由 Rabin 提出）。例如，在 Emerson 和 Sistla（1984）中，使用无限树上的自动机和 Rabin 定理获得了 CTL*的决策过程。有关更多详细信息，请参阅 Vardi（2006）。

关于各种时间逻辑的可判定性结果和决策过程的重要参考文献包括：Burgess（1980）和 Gurevich 和 Shelah（1985）关于分支时间逻辑；Burgess 和 Gurevich（1985）关于线性时间逻辑；Goldblatt（1992）关于线性和分支时间逻辑；Montanari 和 Policriti（1996）关于度量和分层时间逻辑；French（2001）关于一些量化命题分支时间逻辑。

虽然大多数命题时间逻辑是可判定的，但添加一些语法或语义特征可能会使它们在计算上爆炸并变得不可判定。除了与其他表达逻辑的组合之外，导致时间逻辑不可判定的最常见原因包括：类似网格的模型；沿多个时间线的时间运算符；时间逻辑的乘积；没有局部性假设的基于区间的逻辑；时间参考机制，例如混合参考指针和冻结量词；算术特征，例如时间加法，精确时间约束等。然而，有各种方法可以驯服时间逻辑并恢复可判定性，例如添加语法和参数限制（例如对命题变量数量或嵌套深度的限制），施加适当的语义限制（例如区间逻辑的局部性），识别可判定的片段（例如经典一阶逻辑的两变量片段 FO2，受限片段，单调片段）等。

11. 时间逻辑的应用

时间逻辑是一个发展受到哲学考虑驱动的领域。与此同时，多年来开发的逻辑形式和技术系统在各个不同学科中找到了应用，包括计算机科学、人工智能、语言学，以及自然科学、认知科学和社会科学。在本节中，我们简要讨论了时间逻辑在计算机科学、人工智能和语言学中的一些相关应用。

11.1 计算机科学中的时间逻辑

将时间推理应用于确定性和随机转换系统的分析的想法已经存在于 Rescher 和 Urquhart（1971 年，第 XIV 章）的过程和事件理论中。然而，正是在 Pnueli（1977 年）的开创性论文中，时间逻辑在计算机科学中真正突出起来。Pnueli 提出了将时间逻辑应用于反应式和并发程序和系统的规范和验证。为了确保反应式程序的正确行为（例如操作系统），其中计算是非终止的，有必要正式指定和验证该程序的可接受无限执行。此外，为了确保并发程序的正确性，其中两个或多个处理器并行工作，有必要正式指定和验证它们的交互和同步。

可以通过时间模式捕捉到的无限计算的关键属性包括活性、安全性和公平性（参见 Manna 和 Pnueli 1992 年）：

• 活力性质或最终性质涉及形式为 Fp、q→Fp 或 G(q→Fp)的时间模式，这些模式确保如果特定的前提条件(q)最初得到满足，则在计算过程中最终将达到一个理想状态(满足 p)。例如：“如果发送了一条消息，它最终将被传递”和“每当激活打印作业，它最终将被完成”。

• 安全性或不变性属性涉及形式为 Gp、q→Gp 或 G(q→Gp)的时间模式，这些模式确保如果特定的前提条件(q)最初得到满足，则不会发生不良状态(违反安全条件 p)。例如：“任何时刻最多只有一个进程处于其临界区”，“一个资源永远不会被两个或更多进程同时使用”，或者更实际的例子：“交通信号灯永远不会同时显示绿色”，“火车永远不会通过红色信号”。

• 公平性属性涉及形式为 GFp（“无限次 p”）或 FGp（“最终总是 p”）的时间模式的组合。直观地说，公平性要求在同时运行共享资源的多个进程时，操作系统、调度程序等必须对它们进行“公平”处理。一个典型的公平性要求是，如果一个进程在发送请求方面足够持久（例如，一遍又一遍地发送请求），它的请求最终将被授予。

一个无限计算通过线性时间逻辑 LTL 的模型来形式化表示。非确定性系统通过分支时间结构进行建模。因此，LTL 和计算树逻辑 CTL 和 CTL*对于反应式和并发系统的规范和验证非常重要。

以下示例结合了单个计算的活性和安全性属性：“每当达到警报状态时，警报被激活并保持激活状态，直到最终达到安全状态”。这个属性可以用 LTL 表示为

G(alert→(alarm U safe)).

另一个例子，涉及系统中的所有计算，是：“如果进程 σ 从当前状态开始的某个计算上最终启用，则在每个从那里开始的计算中，只要 σ 启用，它将保持启用，直到进程 τ 被禁用”。这个属性可以在 CTL*中形式化为

◊Fenabledσ→□G(enabledσ→(enabledσUdisabledτ)).

LTL 的一个变体，对于指定和推理并发系统具有有用的应用是 Lamport（1994）的动作时态逻辑 TLA。计算机科学中时间逻辑的其他应用包括：时间数据库，实时进程和系统，硬件验证等。关于这些应用的更多信息可以在例如 Pnueli（1977）；Emerson 和 Clarke（1982）；Moszkowski（1983）；Galton（1987）；Emerson（1990）；Alur 和 Henzinger（1992）；Lamport（1994）；Vardi 和 Wolper（1994）；Bolc 和 Szalas（1995）；Gabbay 等（2000）；Baier 和 Katoen（2008）；Kröger 和 Merz（2008）；Fisher（2011）；Demri 等（2016）中找到。

11.2 人工智能中的时间逻辑

人工智能（AI）是时间逻辑的主要应用领域之一。早在麦卡锡和海耶斯（1969）对人工智能的早期哲学讨论中，就提出了将时间推理与人工智能联系起来的建议；Rescher 和 Urquhart（1971，第 XIV 章）的过程和事件理论以及 Hamblin（1972）的基于时期的理论；请参阅 Øhrstrøm 和 Hasle（1995）以了解这些早期发展的概述。在 20 世纪 80 年代，时间表示和推理逐渐成为人工智能中一个越来越重要的主题，出现了几部有影响力的作品，包括 McDermott 关于过程和计划推理的时间逻辑（McDermott 1982）；Allen 关于行动和时间的一般理论（Allen 1984）；Kowalski 和 Sergot 的事件演算（1986）；Shoham 的具体化时间逻辑（1987）；Ladkin 的时间表示逻辑（1987）；以及 Dean 和 McDermott 关于时间数据库管理的工作（1987）。Galton（1987）对这一时期的这些和其他重要发展进行了系统的解释；另请参阅 Vila（1994）和 Pani 和 Bhattacharjee（2001）进行全面的评论。20 世纪 90 年代的有影响力的作品包括 Halpern 和 Shoham（1991）以及 Allen 和 Ferguson（1994）引入了基于区间的时间逻辑，包括行动和事件的表示；Pinto 和 Reiter 的情境演算（1995）；以及 Lamport 的行动理论（Lamport 1994）等。此后，与时间推理和人工智能相关的进一步重要发展包括：自然语言中的时间推理，时间本体论，时间数据库和约束求解，时间规划，可执行的时间逻辑，时空推理，基于代理系统的时间推理等。这个领域逐渐变得如此丰富和广泛-如 Fisher 等人编辑的 20 章手册所证明的那样。 (2005) — 这里不可能对其进行简要概述，因此我们只对与时间推理和逻辑在人工智能中具有哲学相关性的一些主要问题进行书签标记。

• 在人工智能中，尤其是在 20 世纪 80 年代至 90 年代，关于时间表示和推理的主流逻辑方法通常是基于一阶逻辑的时间化变体，而不是基于 Prior 风格的时间逻辑。这种方法最好通过所谓的时间论证方法来说明（McCarthy 和 Hayes 1969; Shoham 1987; Vila 1994）。根据这种方法，通过给命题和谓词添加“时间戳”参数来捕捉时间维度，例如“Publish(A. Prior, Time and Modality, 1957)”。另一种替代但密切相关的方法是具体化的时间逻辑（McDermott 1982; Allen 1984; Shoham 1987; 参见 Ma 和 Knight 2001 进行调查）。这种方法使用具体化的元谓词，例如“TRUE”和“FALSE”，还有“HOLDS”，“OCCURS”，“BEFORE”，“AFTER”，以及诸如“MEETS”，“OVERLAPS”等的区间关系，这些关系应用于某种标准逻辑语言（例如经典一阶逻辑）的命题上。具体化表达式的一个例子是“OCCUR(Born(A. Prior), 1914)”。时间理论与时间发生理论相关（参见 Vila 2005）。尽管基于模态逻辑的方法一直很重要，并且最近在基于代理的时间推理的背景下再次兴起（参见 Fisher 和 Wooldridge 2005）。

• 人工智能中的时间推理理论区分了流变和事件，流变是描述可能随时间变化的世界状态的命题，而事件则代表世界中发生的事情并导致状态之间的变化。在这里引发的哲学问题涉及流变和事件的本质，瞬时事件的含义，均匀状态和非均匀事件的区别，分割瞬时问题，框架问题等。有关进一步讨论，请参见 Shoham（1987）；Galton（1990）；和 Vila（2005）。另请参阅有关逻辑和人工智能条目第 4 节中关于行动和变化推理的相关讨论。

• 流变和事件都可以在离散或连续的时间中考虑，并且它们可以是瞬时的或持续的。这使得基于瞬时和基于区间的时间形式模型的辩论仍然存在，各种理论都在追随和比较这两种方法，包括 van Benthem（1983）；Allen（1983）；Allen 和 Hayes（1989）；Allen 和 Ferguson（1994）；Galton（1995）；Vila（2005）；等等。

有关人工智能中时间推理和逻辑的进一步阅读和讨论，请参见 Vila（1994）；Galton（1995）；综合手册 Fisher 等（2005）；以及更简洁的手册章节 Fisher（2008）。

11.3 语言学中的时间逻辑

时态是自然语言中的一个重要特征。它是一种语言工具，允许人们在时间上指定事件的相对位置，通常是相对于说话时间。在大多数语言中，包括英语，在动词时态系统中体现出时态的不同形式。英语允许区分过去、现在和将来时（“将来”时态），传统上，相应的完成时和进行时形式也被称为时态。

如上所述，普赖尔发明时态逻辑的主要动机是自然语言中时态的使用。Reichenbach（1947）提供了一种早期的逻辑方法来处理时态，他建议用三个时间点来分析英语的动词时态：说话时间、事件时间和参考时间，其中参考时间是一个在语境中显著的时间点，直观地捕捉到了事件被观察的视角。通过使用参考时间的概念，Reichenbach 能够区分简单过去时（“我写了一封信”）和现在完成时（“我已经写了一封信”），而这两种情况在普赖尔的解释中被混淆了。在简单过去时和现在完成时的情况下，事件时间都在说话时间之前；但是，在前一种情况下，参考时间与事件时间重合，而在后一种情况下，参考时间与说话时间同时发生。

既不是 Prior 的框架，也不是 Reichenbach 的框架能够解释简单过去时（“我写了一封信”）和过去进行时（“我正在写一封信”）之间的差异。这里的相关区别是方面而不是时态，自然需要一个基于区间或事件的设置来进行充分的处理。有关这些观点的解释，请参见 Dowty（1979）；Parsons（1980）；Galton（1984）；和 van Lambalgen 和 Hamm（2005）。

而 Reichenbach 的分析提到了一个在语境中显著的时间点，根据 Prior 的观点，时态被解释为时间运算符，这些运算符被解释为时间瞬间的量词。这引发了一个普遍的问题：自然语言中的时态是要被视为量词，还是指特定的时间点？在一篇有影响力的论文中，Partee（1973）提供了以下反例来反对时态的量词处理：句子“我没有关火炉”既不意味着（1）存在一个早于此时刻的时间瞬间我没有关火炉，也不意味着（2）不存在一个早于此时刻的时间瞬间我关火炉。第一个要求太弱，第二个要求太强。Partee 提出了时态和指代性代词之间的类比。根据这个提议，时态指的是特定的、在语境中给定的时间点（例如今天早上 8 点），这些时间点被预设为与话语时间适当地存在时间关系。随后，将量化限制在一个语境中给定的时间区间（例如今天早上）的解释变得流行起来。根据这些解释，Partee 的例句具有直观的含义：在语境中显著的时间区间内没有早于此时刻的时间瞬间我关火炉。从形式上讲，这个想法既符合量词处理，也符合指代性处理；有关详细信息，请参见 Kuhn 和 Portner（2002）和 Ogihara（2011）。

语言学中与时间相关的其他相关问题涉及时间副词和连接词的含义，时态和量化的相互作用，嵌入时态和时态顺序的解释，以及时态和语气的相互关系。有关在语言学中应用时间逻辑的概述和进一步讨论，请参见例如 Steedman（1997）；Kuhn 和 Portner（2002）；Mani 等（2005）；ter Meulen（2005）；Moss 和 Tiede（2006）；Ogihara（2007；2011）；Dyke（2013）；以及关于时态和体貌的条目。

进一步阅读

有关时间逻辑的进一步参考，请参见 Venema（2001）和 Müller（2011）中的概述，以及 Rescher 和 Urquhart（1971）中的详细参考书目；Øhrstrøm 和 Hasle（1995）；Gabbay 等（1994）；Fisher 等（2005）；Baier 和 Katoen（2008）；以及 Demri 等（2016）中的详细参考书目。

Bibliography

• Allen, J.F., 1983, “Maintaining Knowledge about Temporal Intervals”, Communications of the ACM, 26(11): 832–843.

• –––, 1984, “Towards a General Theory of Action and Time”, Artificial Intelligence, 23: 123–154.

• Allen, J.F., and G. Ferguson, 1994, “Actions and Events in Interval Temporal Logic”, Journal of Logic and Computation, 4(5): 531–579.

• Allen, J.F., and P. Hayes, 1989, “Moments and Points in an Interval-Based Temporal Logic”, Computational Intelligence, 5(4): 225–238.

• Alur, R., and T. Henzinger, 1992, “Logics and Models of Real-Time: A Survey”, in Real-Time: Theory in Practice, Proceedings of the REX Workshop 1991 (Lecture Notes in Computer Science: Volume 600), Berlin: Springer, pp. 74–106.

• –––, 1993, “Real-Time Logics: Complexity and Expressiveness”, Information and Computation, 104: 35–77.

• –––, 1994, “A Really Temporal Logic”, Journal of the ACM, 41: 181–204.

• Alur, R., T. Henzinger, and O. Kupferman, 2002, “Alternating-Time Temporal Logic”, Journal of the ACM, 49(5): 672–713.

• Andréka, H., V. Goranko, S. Mikulas, I. Németi, and I. Sain, 1995, “Effective First-Order Temporal Logics of Programs”, in Bolc and Szalas (1995), pp. 51–129.

• Andréka, H., J. Madarász, and I. Németi, 2007, “Logic of Space-Time and Relativity Theory”, in M. Aiello, J. van Benthem, and I. Pratt-Hartmann (eds.), Handbook of Spatial Logics, Dordrecht: Springer, pp. 607–711.

• Areces, C., and B. ten Cate, 2006, “Hybrid Logics”, in Blackburn et al. (2006), pp. 821–868.

• Aristotle, Organon, II - On Interpretation, Chapter 9. See https://archive.org/stream/AristotleOrganon/AristotleOrganoncollectedWorks.

• Artale, A., and E. Franconi, 2000, “A Survey of Temporal Extensions of Description Logics”, Annals of Mathematics and Artificial Intelligence, 30: 171–210.

• Baader, F., and C. Lutz, 2006, “Description Logic”, in Blackburn et al. (2006), pp. 757–819.

• Baier, C., and J.P. Katoen, 2008, Principles of Model Checking, Cambridge, Massachusetts: MIT Press.

• Balbiani, P., V. Goranko, and G. Sciavicco, 2011, “Two-Sorted Point-Interval Temporal Logics”, in Proceedings of the 7th International Workshop on Methods for Modalities (Electronic Notes in Theoretical Computer Science: Volume 278), pp. 31–45.

• Belnap, N., 1992, “Branching Space-Time”, Synthese, 92(3): 385–434.

• Belnap, N., and M. Green, 1994, “Indeterminism and the Thin Red Line”, Philosophical Perspectives, 8: 365–388.

• Belnap, N., and T. Müller, 2014a, “CIFOL: Case-Intensional First Order Logic (I): Toward a Theory of Sorts”, Journal of Philosophical Logic, 43(2–3): 393–437.

• –––, 2014b, “BH-CIFOL: Case-Intensional First Order Logic (II): Branching Histories”, Journal of Philosophical Logic, 43(5): 835–866.

• Belnap, N., T. Müller, and T. Placek, 2022, Branching Space-Times: Theory and Applications, Oxford: Oxford University Press.

• Belnap, N., and M. Perloff, 1988, “Seeing to it that: A Canonical Form for Agentives”, Theoria, 54: 175–199, reprinted with corrections in H. E. Kyberg et al. (eds.), Knowledge Representation and Defeasible Reasoning, Dordrecht: Kluwer, 1990, pp. 167–190.

• Belnap, N., M. Perloff, and M. Xu, 2001, Facing the Future: Agents and Choices in Our Indeterminist World, Oxford: Oxford University Press.

• Ben-Ari, M., A. Pnueli, and Z. Manna, 1983, “The Temporal Logic of Branching Time”, Acta Informatica, 20(3): 207–226.

• van Benthem, J., 1983, The Logic of Time, Dordrecht, Boston, and London: Kluwer Academic Publishers. [Second edition: 1991.]

• –––, 1995, “Temporal Logic”, in D.M. Gabbay, C.J. Hogger, and J.A. Robinson (eds.), Handbook of Logic in Artificial Intelligence and Logic Programming (Volume 4), Oxford: Clarendon Press, pp. 241–350.

• van Benthem, J., and E. Pacuit, 2006, “The Tree of Knowledge in Action: Towards a Common Perspective”, in Advances in Modal Logic (Volume 6), London: College Publications, pp. 87–106.

• Blackburn, P., 2006, “Arthur Prior and Hybrid Logic”, Synthese, 150: 329–372.

• Blackburn, P., J. van Benthem, and F. Wolter, 2006, Handbook of Modal Logics, Amsterdam: Elsevier.

• Blackburn, P., P. Hasle, and P. Øhrstrøm (eds.), 2019, Logic and Philosophy of Time: Further Themes from Prior (Volume 2), Aalborg: Aalborg University Press.

• Blackburn, P., and M. Tzakova, 1999, “Hybrid Languages and Temporal Logic”, Logic Journal of the IGPL, 7: 27–54.

• Bolc, L., and A. Szalas (eds.), 1995, Time and Logic: A Computational Approach, London: UCL Press.

• Börger, E., E. Grädel, and Y. Gurevich, 1997, The Classical Decision Problem, Berlin, Heidelberg: Springer.

• Boyd, S., 2014, “Defending History: Temporal Reasoning in Genesis 2:7–3:8”, Answers Research Journal, 7: 215–237.

• Bresolin, D., V. Goranko, A. Montanari, and G. Sciavicco, 2009, “Propositional Interval Neighborhood Logics: Expressiveness, Decidability, and Undecidable Extensions”, Annals of Pure and Applied Logic, 161(3): 289–304.

• Bresolin, D., D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco, 2013, “Metric Propositional Neighborhood Logics on Natural Numbers”, Software and Systems Modeling, 12(2): 245–264.

• Broersen, J., 2011, “Deontic Epistemic Stit Logic Distinguishing Modes of Mens Rea”, Journal of Applied Logic, 9: 137–152.

• Broersen, J., A. Herzig, and N. Troquard, 2006, “A STIT-Extension of ATL”, in Proceedings of JELIA 2006 (Lecture Notes in Artificial Intelligence: Volume 4160), Berlin: Springer, pp. 69–81.

• Brown, M., and V. Goranko, 1999, “An Extended Branching-Time Ockhamist Temporal Logic”, Journal of Logic, Language and Information, 8(2): 143–166.

• Bull, R., 1970, “An Approach to Tense Logic”, Theoria, 36: 282–300.

• Burgess, J., 1978, “The Unreal Future”, Theoria, 44(3): 157–179.

• –––, 1979, “Logic and Time”, Journal of Symbolic Logic, 44: 566–582.

• –––, 1980, “Decidability for Branching Time”, Studia Logica, 39: 203–218.

• –––, 1982a, “Axioms for Tense Logic I: ‘Since’ and ‘Until’”, Notre Dame Journal of Formal Logic, 23: 367–374.

• –––, 1982b, “Axioms for Tense Logic II: Time Periods”, Notre Dame Journal of Formal Logic, 23: 375–383.

• –––, 1984, “Basic Tense Logic”, in D.M. Gabbay, and F. Guenthner (eds.), Handbook of Philosophical Logic (Volume 2), Dordrecht: Reidel, pp. 89–133. [New edition in Gabbay and Guenthner (2002), pp. 1–42.]

• Burgess, J., and Y. Gurevich, 1985, “The Decision Problem for Linear Temporal Logic”, Notre Dame Journal of Formal Logic, 26(2): 115–128.

• Ciuni, R., and A. Zanardo, 2010, “Completeness of a Branching-Time Logic with Possible Choices”, Studia Logica, 96: 393–420.

• Cocchiarella, N., 2002, “Philosophical Perspectives on Quantification in Tense and Modal Logic”, in Gabbay and Guenthner (2002), pp. 235–276.

• Correia, F., and F. Iacona (eds.), 2013, Around the Tree: Semantic and Metaphysical Issues Concerning Branching and the Open Future (Synthese Library: Volume 361), Dordrecht: Springer.

• Dean, T., and D.V. McDermott, 1987, “Temporal Data Base Management”, Artificial Intelligence, 32:1–55.

• Della Monica, D., V. Goranko, A. Montanari, and G. Sciavicco, 2011, “Interval Temporal Logics: A Journey”, Bulletin of the European Association for Theoretical Computer Science, 105: 73–99.

• Demri, S., V. Goranko, and M. Lange, 2016, Temporal Logics in Computer Science, Cambridge: Cambridge University Press.

• Dowty, D., 1979, Word Meaning and Montague Grammar, Dordrecht: Reidel.

• Dyke, H., 2013, “Time and Tense”, in Dyke and Bardon (2013), pp. 328–344.

• Dyke, H., and A. Bardon (eds.), 2013, A Companion to the Philosophy of Time (Blackwell Companions to Philosophy), Oxford: Wiley-Blackwell.

• Emerson, E.A., 1990, “Temporal and Modal Logics”, in J. van Leeuwen (ed.), Handbook of Theoretical Computer Science (Volume B: Formal Models and Semantics), Amsterdam: Elsevier, pp. 995–1072.

• Emerson, E.A., and E.C. Clarke, 1982, “Using Branching Time Temporal Logic to Synthesise Synchronisation Skeletons”, Science of Computer Programming, 2: 241–266.

• Emerson, E.A., and J. Halpern, 1985, “Decision Procedures and Expressiveness in the Temporal Logic of Branching Time”, Journal of Computer and Systems Science, 30: 1–24.

• Emerson, E.A., and A. Sistla, 1984, “Deciding Full Branching Time Logic”, Information and Control, 61: 175–201.

• Euzenat, J., and A. Montanari, 2005, “Time Granularity”, in Fisher et al. (2005), pp. 59–118.

• Ewald, W., 1986, “Intuitionistic Tense and Modal Logic”, Journal of Symbolic Logic, 51(1): 166–179.

• Fagin, R., J. Halpern, Y. Moses, and M. Vardi, 1995, Reasoning about Knowledge, Boston: MIT Press.

• Finger, M., and D.M. Gabbay, 1992, “Adding a Temporal Dimension to a Logic System”, Journal of Logic, Language and Information, 1(3): 203–233.

• –––, 1996, “Combining Temporal Logic Systems”, Notre Dame Journal of Formal Logic, 37(2): 204–232.

• Finger, M., D.M. Gabbay, and M. Reynolds, 2002, “Advanced Tense Logic”, in Gabbay and Guenthner (2002), pp. 43–204.

• Fisher, M., 2008, “Temporal Representation and Reasoning”, in F. van Harmelen, V. Lifschitz, and B. Porter (eds.), Handbook of Knowledge Representation, Amsterdam: Elsevier, pp. 513–550.

• –––, 2011, An Introduction to Practical Formal Methods Using Temporal Logic, New York: Wiley.

• Fisher, M., D.M. Gabbay, and L. Vila, 2005, Handbook of Temporal Reasoning in Artificial Intelligence, Amsterdam: Elsevier.

• Fisher, M., and M. Wooldridge, 2005, “Temporal Reasoning in Agent-Based Systems”, in Fisher et al. (2005), pp. 469–495.

• Fitting, M., and R. Mendelsohn, 1998, First Order Modal Logic, Dordrecht: Kluwer.

• French, T., 2001, “Decidability of Quantified Propositional Branching Time Logics”, Advances in AI (Lecture Notes in Computer Science: Volume 2256), Berlin: Springer, pp. 165–176.

• French, T., and M. Reynolds, 2003, “A Sound and Complete Proof System for QPTL”, in Balbiani et al. (eds.), Advances in Modal Logic (Volume 4), London: College Publication, pp. 127–148.

• Gabbay, D.M., and F. Guenthner (eds.), 2002, Handbook of Philosophical Logic (Volume 7), Second Edition, Dordrecht: Kluwer.

• Gabbay, D.M., I. Hodkinson, and M. Reynolds, 1994, Temporal Logic: Mathematical Foundations and Computational Aspects (Volume 1), Oxford: Clarendon Press.

• Gabbay, D., A. Kurucz, F. Wolter, and M. Zakharyaschev, 2003, Many-Dimensional Modal Logics: Theory and Applications, Amsterdam: Elsevier.

• Gabbay, D.M., A. Pnueli, S. Shelah, and J. Stavi, 1980, “On the Temporal Basis of Fairness”, in Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 163–173.

• Gabbay, D.M., M. Reynolds, and M. Finger, 2000, Temporal Logic: Mathematical Foundations and Computational Aspects (Volume 2), Oxford: Oxford University Press.

• Gabelaia, D., R. Kontchakov, A. Kurucz, F. Wolter, and M. Zakharyaschev, 2005, “Combining Spatial and Temporal Logics: Expressiveness vs. Complexity”, Journal of Artificial Intelligence Research, 23: 167–243.

• Galton, A.P., 1984, The Logic of Aspect, Oxford: Clarendon Press.

• –––, 1990, “A Critical Examination of Allen’s Theory of Action and Time”, Artificial Intelligence, 42: 159–188.

• –––, 1987, Temporal Logics and their Applications, London: Academic Press.

• –––, 1995, “Time and Change for AI”, in D.M. Gabbay, C.J. Hogger, and J.A. Robinson, Handbook of Logic in Artificial Intelligence and Logic Programming (Volume 4), Oxford: Clarendon Press, pp. 175–240.

• –––, 1996, “Time and Continuity in Philosophy, Mathematics, and Artificial Intelligence”, Kodikas/Code, 19 (1–2): 101–119.

• –––, 2008, “Temporal Logic”, in E.N. Zalta (ed.), The Stanford Encyclopedia of Philosophy (Fall 2008 Edition), URL = https://plato.stanford.edu/archives/fall2008/entries/logic-temporal/.

• Garson, J., 1984, “Quantification in Modal Logic”, in D.M. Gabbay, and F. Guenthner (eds.), Handbook of Philosophical Logic, Dordrecht: Reidel, pp. 249–307.

• Goldblatt, R., 1980, “Diodorean Modality in Minkowski Spacetime”, Studia Logica, 39: 219–236. [Reprinted in Mathematics of Modality (CSLI Lecture Notes 43), Stanford: CSLI Publications, 1993.]

• –––, 1992, Logics of Time and Computation (CSLI Lecture Notes 7), Second Edition, Stanford: CSLI Publications.

• Goranko, V., 1996, “Hierarchies of Modal and Temporal Logics with Reference Pointers”, Journal of Logic, Language and Information, 5(1): 1–24.

• Goranko, V., and G. van Drimmelen, 2006, “Complete Axiomatization and Decidablity of the Alternating-Time Temporal Logic”, Theoretical Computer Science, 353: 93–117.

• Goranko, V., A. Montanari, and G. Sciavicco, 2003, “Propositional Interval Neighborhood Logics”, Journal of Universal Computer Science, 9(9): 1137–1167.

• –––, 2004, “A Road Map of Propositional Interval Temporal Logics and Duration Calculi”, Journal of Applied Non-Classical Logics (Special Issue on Interval Temporal Logics and Duration Calculi), 14(1–2): 11–56.

• Goranko, V., and D. Shkatov, 2010, “Tableau-Based Decision Procedures for Logics of Strategic Ability in Multi-Agent Systems”, ACM Transactions of Computational Logic, 11(1): 3–51.

• Goré, R., 1999, “Tableau Methods for Modal and Temporal Logics”, in M. D’Agostino, D.M. Gabbay, R. Hahnle, and J. Posegga (eds.), Handbook of Tableau Methods, Dordrecht: Kluwer, pp. 297–396.

• Grädel, E., and M. Otto, 1999, “On Logics With Two Variables”, Theoretical Computer Science, 224(1–2), pp. 73–113.

• Gurevich, Y., and S. Shelah, 1985, “The Decision Problem for Branching Time Logic”, Journal of Symbolic Logic, 50: 668–681.

• Halpern, J., and Y. Shoham, 1986. “A Propositional Modal Logic of Time Intervals”, in Proceedings of the 2nd IEEE Symposium on Logic in Computer Science, pp. 279–292. [Reprinted in Journal of the ACM, 38(4): 935–962, 1991.]

• Halpern, J., and M. Vardi, 1989, “The Complexity of Reasoning about Knowledge and Time I: Lower Bounds”, Journal of Computer and System Sciences, 38(1): 195–237.

• Hamblin, C.L., 1972, “Instants and Intervals”, in J.T. Fraser, F. Haber, and G. Müller (eds.), The Study of Time, Berlin/Heidelberg: Springer, pp. 324–331.

• Hansen, M.R., and C. Zhou, 1997, “Duration Calculus: Logical Foundations”, Formal Aspects of Computing, 9: 283–330.

• Hart, S., and M. Sharir, 1986, “Probabilistic Propositional Temporal Logics”, Information and Control, 70(2–3): 97–155.

• Hasle, P., P. Blackburn, and P. Øhrstrøm (eds.), 2017, Logic and Philosophy of Time: Themes from Prior (Volume 1), Aalborg: Aalborg University Press.

• Hodkinson, I., and M. Reynolds, 2006, “Temporal Logic”, in Blackburn et al. (2006), pp. 655–720.

• Hodkinson, I., F. Wolter, and M. Zakharyaschev, 2000, “Decidable Fragments of First-Order Temporal Logics”, Annals of Pure and Applied Logic, 106(1–3): 85–134.

• –––, 2001, “Monodic Fragments of First-Order Temporal Logics: 2000-2001 A.D.”, in Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings of the 8th International Conference LPAR 2001, Springer, pp. 1–23.

• –––, 2002, “Decidable and Undecidable Fragments of First-Order Branching Temporal Logics”, in Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, pp. 393–402.

• Humberstone, I.L., 1979, “Interval Semantics for Tense Logic: Some Remarks”, Journal of Philosophical Logic, 8: 171–196.

• Ingthorsson, R.D., 2016, McTaggart’s Paradox, New York: Routledge.

• Kamide, N., and H. Wansing, 2010, “Combining Linear-Time Temporal Logic with Constructiveness and Paraconsistency”, Journal of Applied Logic, 6: 33–61.

• –––, 2011, “A Paraconsistent Linear-Time Temporal Logic”, Fundamenta Informaticae, 106: 1–23.

• Kamp, J., 1968, Tense Logic and the Theory of Linear Order, PhD Thesis, University of California, Los Angeles.

• –––, 1971, “Formal Properties of ‘Now’”, Theoria, 37: 227–273.

• –––, 1979, “Events, Instants and Temporal Reference”, in R. Bäuerle, U. Egli, and A. von Stechow (eds.), Semantics from Different Points of View, Berlin: Springer, pp. 376–417.

• Kesten, Y., and A. Pnueli, 2002, “Complete Proof System for QPTL”. Journal of Logic and Computation, 12(5): 701–745.

• Kontchakov, R., A. Kurucz, F. Wolter, and M. Zakharyaschev, 2007, “Spatial Logic + Temporal Logic = ?”, in M. Aiello, J. van Benthem, and I. Pratt-Hartmann (eds.), Handbook of Spatial Logics, Berlin: Springer, pp. 497–564.

• Kontchakov, R., C. Lutz, F. Wolter, and M. Zakharyaschev, 2004, “Temporalising Tableaux”, Studia Logica, 76(1): 91–134.

• Konur, S., 2013, “A Survey on Temporal Logics for Specifying and Verifying Real-Time Systems”, Frontiers of Computer Science, 7(3): 370–403.

• Koymans, R., 1990, “Specifying Real-Time Properties with Metric Temporal Logic”, Real-Time Systems, 2(4): 55–299.

• Kowalski, R.A., and M.J. Sergot, 1986, “A Logic-Based Calculus of Events”, New Generation Computing, 4: 67–95.

• Kröger, F., and S. Merz, 2008, Temporal Logic and State Systems (EATCS Texts in Theoretical Computer Science Series), Berlin: Springer.

• Kuhn, S.T., and P. Portner, 2002, “Tense and Time”, in Gabbay and Guenthner (2002), pp. 277–346.

• Ladkin, P., 1987, The Logic of Time Representation, PhD Thesis, University of California, Berkeley.

• van Lambalgen, M., and F. Hamm, 2005, The Proper Treatment of Events, Malden: Blackwell.

• Lamport, L., 1994, “The Temporal Logic of Actions”, ACM Transactions on Programming Languages and Systems, 16(3): 872–923.

• Lindström, S., and K. Segerberg, 2006, “Modal Logic and Philosophy”, in Blackburn et al. (2006), pp. 1149–1214

• Linsky, B., and E. Zalta, 1994, “In Defense of the Simplest Quantified Modal Logic”, Philosophical Perspectives, 8: 431–458.

• Lorini, E., 2013, “Temporal STIT Logic and Its Application to Normative Reasoning”, Journal of Applied Non-Classical Logics, 23(4): 372–399.

• Lutz, K., F. Wolter, and M. Zakharyaschev, 2008, “Temporal Description Logics: A Survey”, Proceedings of TIME 2008, pp. 3–14.

• Ma, J., and B. Knight, 2001, “Reified Temporal Logics: An Overview”, Artificial Intelligence Review, 15(3): 189–217.

• MacFarlane, J., 2003, “Future Contingents and Relative Truth”, The Philosophical Quarterly, 53(212): 321–336.

• –––, 2014, Assessment Sensitivity: Relative Truth and Its Applications, Oxford: Oxford University Press.

• Manna, Z., and A. Pnueli, 1992, The Temporal Logic of Reactive and Concurrent Systems (Specification: Volume 1), Springer: New York.

• Mani, I., J. Pustejovsky, and R. Gaizauskas, 2005, The Language of Time: A Reader, Oxford: Oxford University Press.

• Marx, M., and M. Reynolds, 1999, “Undecidability of Compass Logic”, Journal of Logic and Computation, 9(6): 897–914.

• McArthur, R., 1976, Tense Logic, Synthese Library, Springer.

• McCarthy, J., and P.J. Hayes, 1969, “Some Philosophical Problems from the Standpoint of Artificial Intelligence”, in D. Michie, and B. Meltzer (eds.), Machine Intelligence 4, Edinburgh: Edinburgh University Press, pp. 463–502.

• McDermott, D., 1982, “A Temporal Logic for Reasoning about Processes and Plans”, Cognitive Science, 6: 101–155.

• McTaggart, E.J., 1908, “The Unreality of Time”, Mind, 17(68): 457–472.

• Merz, S., 1992, “Decidability and Incompleteness Results for First-Order Temporal Logics of Linear Time”, Journal of Applied Non-Classical Logic, 2(2): 139–156.

• ter Meulen, A., 2005, “Temporal Reasoning in Natural Language”, in Fisher et al. (2005), pp. 559–585.

• Meyer, U., 2013, The Nature of Time, Oxford: Oxford University Press.

• Montanari, A., 1996, Metric and Layered Temporal Logic for Time Granularity, PhD Thesis (Institute for Logic, Language, and Computation Dissertation Series, Volume: 1996–02), University of Amsterdam.

• Montanari, A., and A. Policriti, 1996, “Decidability Results for Metric and Layered Temporal Logics”, Notre Dame Journal Formal Logic, 37(2): 260–282.

• Moss, S.L., and H.J. Tiede, 2006, “Applications of Modal Logic in Linguistics”, in Blackburn et al. (2006), pp. 1003–1076.

• Moszkowski, B., 1983, Reasoning about Digital Circuits, PhD Thesis (Technical Report STAN-CS-83–970), Department of Computer Science, Stanford University.

• Müller, T., 2011, “Tense or Temporal Logic”, in R. Pettigrew (ed.), The Continuum Companion to Philosophical Logic, London: Continuum, pp. 324–350.

• –––, 2013, “A Generalized Manifold Topology for Branching Space-Times”, Philosophy of Science, 80: 1089–1100.

• ––– (ed.), 2014, Nuel Belnap on Indeterminism and Free Action (Outstanding Contributions to Logic: Volume 2), Springer.

• Nishimura, H., 1979, “Is the Semantics of Branching Structures Adequate for Non-Metric Ockhamist Tense Logics?”, Journal of Philosophical Logic, 8: 477–478.

• Ogihara, T., 2007, “Tense and Aspect in Truth-Conditional Semantics”, Lingua, 117:392–418.

• –––, 2011, “Tense”, in C. Maienborn, K. von Heusinger, and P. Portner (eds.), Semantics: An International Handbook of Natural Language Meaning, de Gruyter, pp. 1463–1484.

• Øhrstrøm, P., 2009, “In Defense of the Thin Red Line: A Case for Ockhamism”, Humana Mente, 8: 17–32.

• –––, 2019, “A Critical Discussion of Prior’s Philosophical and Tense-Logical Analysis of the Ideas of Indeterminism and Human Freedom”, Synthese, 196(1): 69–85.

• Øhrstrøm, P., and P. Hasle, 1995, Temporal Logic: From Ancient Ideas to Artificial Intelligence, Dordrecht: Kluwer Academic Publishers.

• –––, 2006, “Modern Temporal Logic: The Philosophical Background”, in Handbook of the History of Logic (Volume 7), pp. 447–498.

• –––, 2019, “The Significance of the Contributions of A.N. Prior and Jerzy Łoś in the Early History of Modern Temporal Logic”, in Blackburn et al. (2019), pp. 31–40.

• Pani, A.K., and G.P. Bhattacharjee, 2001, “Temporal Representation and Reasoning in Artificial Intelligence: A Review”, Mathematical and Computer Modelling, 34: 55–80.

• Parsons, T., 1990, Events in the Semantics of English: A Study in Subatomic Semantics, Cambridge: MIT Press.

• Partee, B., 1973, “Some Structural Analogies between Tenses and Pronouns in English”, The Journal of Philosophy, 70(18): 601–609.

• Passy, S., and T. Tinchev, 1985. “Quantifiers in Combinatory PDL: Completeness, Definability, Incompleteness”, in Fundamentals of Computation Theory FCT 85 (Lecture Notes in Computer Science: Volume 199), Berlin: Springer, pp. 512–519.

• Pinto, J., and R. Reiter, 1995, “Reasoning about Time in the Situation Calculus”, Annals of Mathematics and Artificial Intelligence, 14(2–4): 251–268.

• Placek, T., 2014, “Branching for General Relativists”, in Müller (2014), pp. 191–221.

• Ploug, T., and P. Øhrstrøm, 2012, “Branching Time, Indeterminism, and Tense Logic: Unveiling the Prior-Kripke Letters”, Synthese, 188(3): 367–379.

• Pnueli, A., 1977, “The Temporal Logic of Programs”, Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46–67.

• Prior, A.N., 1957, Time and Modality, Oxford: Oxford University Press.

• –––, 1959, “Thank Goodness that’s over”, Philosophy, 34(128): 12–17.

• –––, 1967, Past, Present and Future, Oxford: Oxford University Press.

• –––, 1968, Papers on Time and Tense, Oxford: Oxford University Press. [New edition: P. Hasle et al. (eds.), Oxford: Oxford University Press, 2003.]

• Reichenbach, H., 1947, Elements of Symbolic Logic, New York: Macmillan.

• Rescher, N., and A. Urquhart, 1971, Temporal Logic, Berlin: Springer.

• Reynolds, M., 1994, “Axiomatizing U and S over Integer Time”, in D.M. Gabbay, and H.J. Ohlbach (eds.), Temporal Logic, Proceedings of the First International Conference ICTL 1994 (Lecture Notes in Artificial Intelligence: Volume 828), Berlin/Heidelberg: Springer, pp. 117–132.

• –––, 1996, “Axiomatising First-Order Temporal Logic: Until and Since over Linear Time”, Studia Logica, 57(2–3): 279–302.

• –––, 2001, “An Axiomatization of Full Computation Tree Logic”, Journal of Symbolic Logic, 66: 1011–1057.

• –––, 2002, “Axioms for Branching Time”. Journal of Logic and Computation, 12(4): 679–697.

• –––, 2003, “An Axiomatization of Prior’s Ockhamist Logic of Historical Necessity”, in Balbiani et al. (eds.), Advances in Modal Logic (Volume 4), London: College Publications, pp. 355–370.

• –––, 2005, “An Axiomatization of PCTL*”, Information and Computation, 201(1): 72–119.

• –––, 2007, “A Tableau for Bundled CTL”, Journal of Logic and Computation, 17(1): 117–132.

• –––, 2010, “The Complexity of Temporal Logic over the Reals”, Annals of Pure and Applied Logic, 161(8): 1063–1096.

• –––, 2011, “A Tableau-Based Decision Procedure for CTL*”, Formal Aspects of Computing, 23(6): 739–779.

• –––, 2014, “A Tableau for Temporal Logic over the Reals”, in Goré et al. (eds.), Advances in Modal Logic (Volume 10), London: College Publications, pp. 439–458.

• Röper, P., 1980, “Intervals and Tenses”, Journal of Philosophical Logic, 9: 451–469.

• Rumberg, A., 2016, “Transition Semantics for Branching Time”, Journal of Logic, Language and Information, 25(1): 77–108.

• –––, 2019, “Actuality and Possibility in Branching Time: The Roots of Transition Semantics”, in Blackburn et al. (2019), pp. 145–161.

• Rumberg, A., and A. Zanardo, 2019, “First-Order Definability of Transition Structures”, Journal of Logic, Language and Information, 28(3): 459–488.

• Segerberg, K., 1970, “Modal Logics with Linear Alternative Relations”, Theoria, 36: 301–322.

• Shoham, Y., 1987, “Temporal Logic in AI: Semantical and Ontological Considerations”, Artificial Intelligence, 33: 89–104.

• Steedman, M., 1997, “Temporality”, in J. van Benthem, and A. ter Meulen (eds.), Handbook of Logic and Language, Amsterdam: Elsevier, pp. 925–969.

• Stirling, C., 1992, “Modal and Temporal Logics”, in Handbook of Logic in Computer Science (Computational Structures: Volume 2), Oxford, Clarendon Press, pp. 477–563.

• Thomason, R.H., 1970, “Indeterminist Time and Truth-Value Gaps”, Theoria, 36(3): 264–281.

• –––, 1984, “Combinations of Tense and Modality”, in D.M. Gabbay, and F. Guenther (eds.), Handbook of Philosophical Logic (Extensions of Classical Logic: Volume 2), Dordrecht: Reidel, pp. 135–165. [New edition in Gabbay and Guenthner (2002), pp. 205–234.]

• Tkaczyk, M., and T. Jarmużek, 2019, “Jerzy Łoś Positional Calculus and the Origin of Temporal Logic”, Logic and Logical Philosophy, (28): 259–276.

• Uckelman, S.L., and J. Uckelman, 2007, “Modal and Temporal Logics for Abstract Space-Time Structures”, in Studies in History and Philosophy of Science (Part B: Studies in History and Philosophy of Modern Physics), 38(3): 673–681.

• Vardi, M., 2006, “Automata-Theoretic Techniques for Temporal Reasoning”, in Blackburn et al. (2006), pp. 971–989.

• Vardi, M., and P. Wolper, 1994, “Reasoning about Infinite Computations”, Information and Computation, 115: 1–37.

• Venema, Y., 1990, “Expressiveness and Completeness of an Interval Tense Logic”, Notre Dame Journal of Formal Logic, 31: 529–547.

• –––, 1991, “A Modal Logic for Chopping Intervals”, Journal of Logic and Computation, 1(4): 453–476.

• –––, 1993, “Completeness via Completeness: Since and Until”, in M. de Rijke (ed.), Diamonds and Defaults, Dordrecht: Kluwer, pp. 279–286.

• –––, 2001, “Temporal Logic”, in L. Goble (ed.), Blackwell Guide to Philosophical Logic, Oxford: Blackwell Publishers.

• Vila, L., 1994, “A Survey on Temporal Reasoning in Artificial Intelligence”, AI Communications, 7: 4–28.

• –––, 2005, “Formal Theories of Time and Temporal Incidence”, in Fisher et al. (2005), pp. 1–24.

• Wölfl, S., 1999, “Combinations of Tense and Modality for Predicate Logic”, Journal of Philosophical Logic, 28: 371–398.

• Wolper, P., 1985, “The Tableau Method for Temporal Logic: An Overview”, Logique et Analyse, 28(110–111): 119–136.

• Wolter F., and M. Zakharyaschev, 2000, “Temporalizing Description Logics”, in D.M. Gabbay, and M. de Rijke (eds.), Frontiers of Combining Systems II, New York: Wiley, pp. 379–401.

• –––, 2002, “Axiomatizing the Monodic Fragment of First-Order Temporal Logic”, Annals of Pure and Applied Logic, 118(1–2): 133–145.

• Xu, M., 1988, “On some U,S-Tense Logics”, Journal of Philosophical Logic, 17: 181–202.

• Zanardo, A., 1985, “A Finite Axiomatization of the Set of Strongly Valid Ockhamist Formulas”, Journal of Philosophical Logic, 14: 447–468.

• –––, 1990, “Axiomatization of ‘Peircean’ Branching-Time Logic”, Studia Logica, 49: 183–195.

• –––, 1991, “A Complete Deductive System for Since-Until Branching Time Logic”, Journal of Philosophical Logic, 20: 131–148.

• –––, 1996, “Branching-Time Logic with Quantification over Branches: The Point of View of Modal Logic”, Journal of Symbolic Logic, 61: 1–39.

• –––, 1998, “Undivided and Indistinguishable Histories in Branching-Time Logics”, Journal of Logic, Language and Information, 7(3): 297–315.

• –––, 2013, “Indistinguishability, Choices, and Logics of Agency”, Studia Logica, 101(6): 1215–1236.

• Zanardo, A., B. Barcellan, and M. Reynolds, 1999, “Non-Definability of the Class of Complete Bundled Trees”, Logic Journal of the IGPL (Special Issue on Temporal Logic), 7(1): 125–136.

Academic Tools

	How to cite this entry.
	Preview the PDF version of this entry at the Friends of the SEP Society.
	Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
	Enhanced bibliography for this entry at PhilPapers, with links to its database.

Other Internet Resources

• A Research Site for Prior Studies and Temporal Logic

• TIME International Symposium on Temporal Representation and Reasoning

• The Temporal Logic of Actions (TLA) Home Page

• Galton, A., “Temporal Logic”, The Stanford Encyclopedia of Philosophy (Fall 2008 Edition).

Related Entries

artificial intelligence: logic-based | Diodorus Cronus | frame problem | future contingents | identity: over time | logic: action | logic: combining | logic: free | logic: hybrid | logic: intensional | logic: modal | McTaggart, John M. E. | Ockham [Occam], William | Prior, Arthur | temporal parts | tense and aspect | time

Acknowledgments

The first version of this entry was written by Antony Galton in 1999, later revised in Galton (2008). In 2015 the entry was substantially re-written and extended by the first author of the present version, which is itself a major revision and further extension of the 2015 version. We acknowledge Galton’s contribution to the previous versions, and we retained one example from Galton (2008) in Section 8.1, as indicated there. We are grateful to Johan van Benthem, Rob Goldblatt, Angelo Montanari, Yde Venema, Michael Zakharyaschev, Ed Zalta, and Alberto Zanardo for some helpful suggestions and corrections on the 2015 version.

Copyright © 2020 by Valentin Goranko <[e-mail]> Antje Rumberg <[e-mail]>