时间逻辑

在逻辑上，时间逻辑是代表和推理的任何规则和象征的系统，在时间上有资格的命题（例如，“我总是饿”，“我最终会饿”，或者“我将饿了直到我吃点东西”）。它有时也用于参考时态逻辑，这是Arthur Prior在1950年代后期引入的基于模态逻辑的时间逻辑系统，并由Hans Kamp提出了重要贡献。计算机科学家，尤其是Amir Pnueli和逻辑学家进一步开发了它。

时间逻辑已在正式验证中找到了重要的应用，该应用程序用于说明硬件或软件系统的要求。例如，人们可能希望说，每当提出请求时，最终都会授予对资源的访问，但是从未同时授予两个请求者。这样的语句可以方便地以时间逻辑表达。

动机

考虑一下“我饿”的说法。尽管其含义是持续时间的，但陈述的真实价值可能会随着时间而变化。有时这是真的，有时是错误的，但绝不是正确和错误的。在时间逻辑中，语句可以具有随时间变化的真实价值，与暂时性逻辑相反，该逻辑仅适用于其真实价值在时间上恒定的陈述。随着时间的流逝，对真实价值的这种处理将时间逻辑与计算动词逻辑区分开。

时间逻辑始终具有推理时间表的能力。所谓的“线性时间”逻辑仅限于这种推理。但是，分支时间逻辑可以理解多个时间表。这允许特别处理可能无法预测的环境。为了继续一个例子，在分支时间逻辑中，我们可能会说“有可能永远饿着饿”，并且“最终有可能我不再饿了”。如果我们不知道我是否会被喂食，那么这些陈述都可能是正确的。

历史

尽管亚里士多德的逻辑几乎完全关注分类三段论的理论，但他的作品中有一些段落现在被视为对时间逻辑的期望，并且可能意味着一种早期的，部分发展的一阶暂时性二价逻辑的形式。亚里士多德特别关注未来特遣队的问题，在那里他不能接受双重原则适用于关于未来事件的陈述，即我们目前可以决定有关未来事件的陈述是真实的还是错误的，例如”明天将是一场海战。”

查尔斯·桑德斯·皮尔斯（Charles Sanders Peirce）在19世纪指出，几千年来几乎没有发展：

逻辑学家通常认为时间是所谓的“外部”问题。我从未分享过这一观点。但是我认为逻辑尚未达到发展的状态，在这种发展状态下，引入其形式的时间修改不会引起极大的困惑。我是这样的思维方式。

令人惊讶的是，对于Peirce来说，据我们所知，在20世纪上半叶，建造了第一系统的时间逻辑系统。尽管亚瑟·普里尔（Arthur Prior）被广泛称为《时间逻辑》的创始人，但波兰逻辑学家Jerzyoloś在1947年提供了这种逻辑的第一个形式化。在他的作品中，他在作品中， MetodologiciCznejKanonówMilla （对Mill方法的方法分析的基础）提出了对Mill Canons的形式化。在“ ”方法中，重点放在了时间因素上。因此，为了实现自己的目标，他必须创建一种逻辑，该逻辑可以为时间功能的形式化提供手段。该逻辑可以看作是奥洛斯的主要目的的副产品，尽管这是第一个位置逻辑，作为框架，后来被用于认知逻辑的发明。逻辑本身的语法与使用模态运算符的时态逻辑大不相同。 loś逻辑的语言而不是使用特定于位置逻辑的实现操作员，该操作员将表达式与考虑其真实值的特定上下文结合。在“工作”中，这种考虑的上下文只是时间上的，因此表达式与特定的时刻或时间间隔结合。

在接下来的几年中， Arthur Prior对时间逻辑的研究开始了。他关心自由意志和预定的哲学含义。根据他的妻子的说法，他首先考虑在1953年正式化时间逻辑。他的研究结果首次在1954年在惠灵顿举行的会议上提出。在Prior的正式逻辑中的附录1的最后一部分中，要进行工作。

先前在1955 - 6年在牛津大学进行了关于该主题的讲座，并在1957年出版了一本书，时间和模式，其中他介绍了一个带有两个时间连接剂（模态运算符）F和P的命题模态逻辑，该逻辑对应于“将来的某个时候”和“过去的某个时候”。在这项早期工作中，事先认为是线性的。然而，在1958年，他收到了索尔·克里普克（Saul Kripke）的来信，后者指出，这一假设也许是没有根据的。在预示了计算机科学领域类似的发展的发展中，先前对此进行了建议，并开发了两种分支时间的理论，他称之为“ Ockhamist”和“ Peircean”。在1958年至1965年之间，Prior也与查尔斯·伦纳德·汉布林（Charles Leonard Hamblin）相对应，并且该领域的许多早期发展可以追溯到这种通信，例如汉堡的影响。 Prior在1967年发表了他关于该主题，过去，现在和未来的最成熟的作品。他两年后去世。

与时态逻辑一起， Prior构建了一些位置逻辑系统，这些系统从oloś继承了他们的主要思想。尼古拉斯·雷舍尔（Nicholas Rescher）在60年代和70年代继续进行定位时间逻辑的工作。在《时间顺序逻辑》 （1966年）的注释中，关于年代命题的逻辑（1968） ，拓扑逻辑（1968年）和《时间逻辑》 （1971年），他研究了oś和先前的系统之间的联系。此外，他证明了可以使用特定位置逻辑中的实现操作员来定义先前的时态运算符。 Rescher在他的工作中也创建了更一般的位置逻辑系统。尽管第一个是为纯粹的时间用途而构建的，但他提出了旨在包含实现操作员但没有特定时间公理的逻辑术语拓扑逻辑，例如时钟公理。

从那以后，二进制临时运营商并被汉斯·坎普（Hans Kamp）在1968年的博士学位上引入。论文，其中还包含有关时间逻辑与一阶逻辑的重要结果 - 现在称为Kamp定理的结果。

正式验证中的两个早期竞争者是线性时间逻辑， Amir Pnueli的线性时间逻辑和计算树逻辑（CTL）， Mordechai Ben-Ari的分支时间逻辑， Zohar Manna和Amir Pnueli。 Em Clarke和Ea Emerson在同一时间提出了几乎同等的形式主义。可以比第一个逻辑更有效地确定第二个逻辑的事实并不能反映出一般而言的分支和线性时间逻辑，正如有时所争论的那样。相反，Emerson和Lei表明，任何线性时间逻辑都可以扩展到分支时间逻辑，该逻辑可以以相同的复杂性来确定。

loś的位置逻辑

loś的逻辑被出版为他的1947年硕士论文podstawy anatizymetodogologicznejnonówmilla （对米尔方法的方法学分析的基础）。他的哲学和正式概念可以看作是Lviv – Warsaw逻辑学校的持续，因为他的主管是Jan lukasiewicz的门徒JerzySłupecki 。该论文直到1977年才翻译成英文，尽管亨利克·希（Henryk Hi别说）在1951年发表了简短但内容丰富的象征逻辑杂志。这篇评论包含了工作的核心概念，足以在逻辑社区中普及他的结果。这项工作的主要目的是在形式逻辑的框架内介绍磨坊的规范。为了实现这一目标，作者研究了时间功能在米尔概念结构中的重要性。有了这一点，他提供了他的公理逻辑系统，该系统适合Mill Canons及其时间方面的框架。

句法

首次发表在Podstawy AnalizyMetodologiciCznejKanonówMilla （ Mill's方法分析的基础）中的逻辑语言包括：

一阶逻辑运算符'€'，'∧'，'''→'，'程度'，'∀'和'∃''
实现操作员u
功能符号δ
命题变量p ₁ ，p ₂ ，p ₃ ，...
变量表示时间矩t ₁ ，t ₂ ，t ₃ ，...
变量表示时间间隔n ₁ ，n ₂ ，n ₃ ，...

术语集（由s表示）如下：

变量表示时间矩或间隔是术语
如果 $\text{[math]}$ 和 $\text{[math]}$ 是时间间隔变量，然后 $\text{[math]}$

一组公式（由for表示）如下：

所有一阶逻辑公式都是有效的
如果 $\text{[math]}$ 和 $\text{[math]}$ 是一个命题变量，然后 $\text{[math]}$
如果 $\text{[math]}$ ，然后 $\text{[math]}$
如果 $\text{[math]}$ 和 $\text{[math]}$ ，然后 $\text{[math]}$
如果 $\text{[math]}$ 和 $\text{[math]}$ 然后是命题，力矩或间隔变量，然后 $\text{[math]}$

原始的公理系统

$U_{t_{1}}\neg p_{1}\equiv \neg U_{t_{1}}p_{1}$
$U_{t_{1}}(p_{1}\rightarrow p_{2})\rightarrow (U_{t_{1}}p_{1}\rightarrow U_{t_{1}}p_{2})$
$U_{t_{1}}((p_{1}\rightarrow p_{2})\rightarrow ((p_{2}\rightarrow p_{3})\rightarrow (p_{1}\rightarrow p_{3})))$
$U_{t_{1}}(p_{1}\rightarrow (\neg p_{1}\rightarrow p_{2}))$
$U_{t_{1}}((\neg p_{1}\rightarrow p_{1})\rightarrow p_{1})$
$\forall _{t_{1}}U_{t_{1}}p_{1}\rightarrow p_{1}$
$\forall _{t_{1}}\forall _{n_{1}}\exists _{t_{2}}\forall _{p_{1}}(U_{\delta (t_{1},n_{1})}p_{1}\equiv U_{t_{2}}p_{1})$
$\forall _{t_{1}}\forall _{n_{1}}\exists _{t_{2}}\forall _{p_{1}}(U_{\delta (t_{2},n_{1})}p_{1}\equiv U_{t_{1}}p_{1})$
$\forall _{t_{1}}\exists _{p_{1}}\forall _{t_{2}}(U_{t_{2}}p_{1}\equiv \forall _{p_{2}}(U_{t_{1}}p_{2}\equiv U_{t_{2}}p_{2}))$

Prior的时态逻辑（TL）

时间和模态引入的句子时态逻辑具有四个（非真实性）模态运算符（除了一阶命题逻辑中的所有常规真实功能运算符外）。

P ：“是……”（P代表“过去”）
F ：“将是……”（F代表“未来”）
G ：“总是这样……”
H ：“总是这样……”

如果我们让π是无限的路径，则可以将这些组合在一起：

$\text{[math]}$ ：“在某个时刻， $\text{[math]}$ 在路径的所有未来状态下都是真实的”
$\text{[math]}$ ：” $\text{[math]}$ 在路径上无限的许多状态下是正确的”

从p和f可以定义g和h ，反之亦然：

${\begin{aligned}F&\equiv \lnot G\lnot \\P&\equiv \lnot H\lnot \end{aligned}}$

语法和语义

用以下BNF语法指定了TL的最小语法：

其中一个是某种原子公式。

Kripke模型用于评估TL中句子的真相。集合T和二进制关系< t （称为“优先”）的一对（ t ，<）称为帧。模型由帧的三重（ t ，<， v ）和一个称为估值的函数V给出，该估值分配给原子公式的每个对（ A ， u ），并且时间值有些真实值。概念“在u =（ t ，<， v ）在时间u上是true ”的概念是缩写的u⊨ϕ [ u ]。有了这个符号，


陈述	...是真的
`u⊨a` [ `u` `]`	`v` （ `a` ， `u` ）= true
`u⊨ϕ` `[` `u` ]	不是`u⊨ϕ` `[` `u` ]
`u⊨` （ `ϕ∧ψ` `）` [ `u` ]	`u⊨ϕ` `[` `u` ]和`u⊨ψ` `[` `u` ]
`u⊨` （ `ϕ∨ψ` ） `[` `u` ]	`u⊨ϕ` `[` `u` ]或`u⊨ψ` `[` `u` ]
`u⊨` （ `ϕ` → `ψ` ）[ `u` ]	`u⊨ψ` `[` `u` ]如果`u⊨ϕ` `[` `u` ]
`u⊨gϕ` `[` `u` ]	`u⊨ϕ` [ `v` ]对于所有`v` `，` `u` < `v`
`u⊨hϕ` `[` `u` ]	`u⊨ϕ` `[` `v` ]对于`v` < `u`的所有`v`

给定帧F类，TL的句子是

对于F，如果对于F中的每个模型u =（ t ， <， v ），则有效。
如果F中有u =（ t ，<， v ）在f中有（ t ，<），则可以满足F ，以使得对t ， t ， uu⊨d [ u ]中的某些u
如果每个模型u = （ t ，<， v ）在f中，则f in f in f in f in f in f in f in f in f in f in f in f in的结果ψ ，则在F中使用（ t ，<）和t中的每个u ，如果u⊨ψ [ u ] [ u ]

许多句子仅适用于有限类别的帧。通常，将框架的类别限制在具有及时性，反对称性，反射性，三分法，无反射性，总，密集或某些组合的相关性<的框架类别中。

最小的公理逻辑

Burgess概述了一种逻辑，该逻辑没有对关系<，但允许根据以下公理模式进行有意义的扣除：

一个是a是一阶逻辑的重言式
g（ a → b ）→（g a →g b ）
H（ A → B ）→（H A →H B ）
A →GP A
A →HF A

具有以下扣除规则：

给定A → B和A ，推断B （ Modus Ponens ）
鉴于重言术，推断
鉴于重言式，推断

可以得出以下规则：

贝克尔的规则：给定A → B ，推断t a →t b ，其中t是一个tense ，由G，H，F和P制成的任何序列。
镜像：给定一个定理A ，推断出其镜像a条^§ ，通过用h（s so f by p）替换g获得，反之亦然。
二元性：给定定理A ，推断出其双重语句A *，通过与f与F和H与P互换∧获得。

翻译成谓词逻辑

伯吉斯（Burgess）将TL语句的梅雷迪思（Meredith）翻译成具有一个自由变量x ₀ （代表当前时刻）的一阶逻辑中的语句。该翻译M递归地定义如下：

${\begin{aligned}&M(a)&&=a^{*}x_{0}\\&M(\lnot \phi )&&=\lnot M(\phi )\\&M(\phi \land \psi )&&=M(\phi )\land M(\psi )\\&M({\mathsf {G}}\phi )&&=\forall x_{1}(x_{0}<x_{1}\rightarrow M(A^{+}))\\&M({\mathsf {H}}\phi )&&=\forall x_{1}(x_{1}<x_{0}\rightarrow M(A^{+}))\end{aligned}}$

在哪里 $\text{[math]}$ 是句子 $\text{[math]}$ 所有可变索引的增量为1和 $\text{[math]}$ 是由 $\text{[math]}$ 。

临时操作员

时间逻辑有两种运算符：逻辑运算符和模态运算符。逻辑运营商是通常的真理功能运营商（ $\text{[math]}$ ）。线性时间逻辑和计算树逻辑中使用的模态运算符定义如下。

文字	象征	定义	解释
二进制操作员
$φuψ$ _ $_$	$\phi ~{\mathcal {U}}~\psi$	$(B\,{\mathcal {U}}\,C)(\phi )=\ (\exists i:C(\phi _{i})\land (\forall j<i:B(\phi _{j})))$	u ntil： $ψ$ 保持在当前或将来的位置，并且 $必须$ 保持直到该位置为止。在该位置， $φ$ 不必再保持。
$φrψ$ _ $_$	$\phi ~{\mathcal {R}}~\psi$	$(B\,{\mathcal {R}}\,C)(\phi )=\ (\forall i:C(\phi _{i})\lor (\exists j<i:B(\phi _{j})))$	r力布： $φ$ 将 $ψ$ 释放，如果 $ψ$ 是真实的，直到 $φ$ 为真实的第一个位置（或者如果不存在这种位置）。
一般操作员
nφ $_$	$\bigcirc \phi$	${\mathcal {N}}B(\phi _{i})=B(\phi _{i+1})$	n ext： $φ$ 必须在下一个状态下保持。（ x是同义词。）
fφ $_$	$\Diamond \phi$	${\mathcal {F}}B(\phi )=(true\,{\mathcal {U}}\,B)(\phi )$	f uture： $φ$ 最终必须保持（在后续路径上的某个地方）。
gφ $_$	$\Box \phi$	${\mathcal {G}}B(\phi )=\neg {\mathcal {F}}\neg B(\phi )$	g散发： $φ$ 必须保持在整个后续路径上。
φ $_$	$\forall \phi$	$({\mathcal {A}}B)(\psi )=\ (\forall \phi :\phi _{0}=\psi \to B(\phi ))$	ll ： $φ$ 必须在从当前状态开始的所有路径上保持。
eφ $_$	$\exists \phi$	$({\mathcal {E}}B)(\psi )=\ (\exists \phi :\phi _{0}=\psi \land B(\phi ))$	e xists：至少存在从 $当前$ 状态开始的一条路径。