人工智能——时间逻辑
介绍：
短语时间逻辑是指任何使用规则和符号表示和推理有时间限制的命题的系统。时态逻辑是一个偶尔用来描述它的术语。
更准确地说，时间逻辑关注时态，并使用与时间概念相关的模态运算符，例如有时、总是、先于、成功等。 Arthur Prior 在 1960 年代引入了时间逻辑的特殊模态逻辑系统。
除了普通的逻辑运算符之外，时序逻辑还包含四个具有以下预期含义的模态运算符：Symbols Expression Symbolized G It will always be the case that… F It will sometimes be the case that… H It has always been the case that… P It has at some time operators the case that…
为了创建命题时态逻辑，运算符G 和 F 用于指代未来，而运算符H 和 P 用于指代过去。运算符P & F 称为弱时态运算符，而运算符H 和 G 称为强时态运算符。由于等价性，这两个配对通常被视为可相互定义的。假设 Q 是传统逻辑中的一些封闭公式。两个公理支配过去和未来运算符之间的相互作用：
FQ ≅ ~G~Q
PQ ≅ ~H~Q注意：如果变量出现在量化中或在该变量的量化范围内，则它是绑定的。否则，该变量是免费的。封闭公式是没有自由变量的公式；否则，它是一个开放公式。
Arthur 使用运算符创建公式，这些公式可以表达时间概念，这些概念已被视为基于这些预期含义的形式系统的公理。
分布公理：
分布公理是：
G(Q -> R) -> (GQ -> GR) interpreted as:
If it will always be the case that Q implies R, then
if Q will always be the case,then R will be always be so.
H ( Q->R) -> (HQ -> HR) interpreted as:
If Q has implies R, then
if Q has always been the case,then R will be always be so.时间逻辑中的一般公理：
根据我们对时间结构所做的假设，可以将更多公理添加到时间逻辑中。一组普遍采用的公理是：
GQ -> FQ and HQ -> PQ过去和将来时态运算符的某些组合可用于表达英语中的复杂时态。示例：FPQ 对应于将来完成时的句子 Q。 PPQ 表示过去完成时。
时序逻辑中的有用公理：
(i) Q 为真的情况总是等价于Q 为假的不是过去。
HQ ≅ ~P~Q(ii) Q 为真的情况总是等价于Q 不会在将来为假。
GQ ≅ ~F~Q(iii) 将来 Q 为真的情况总是等价于Q 并不总是为假的。
FQ ≅ ~G~Q(iv) Q 为真的情况等价于Q 为假的情况在过去并不总是如此。
PQ ≅ ~H~Q(v) Q 为真并不总是等价于将来 Q 为假的情况。
~GQ ≅ F~Q(vi) Q 为真在过去并不总是等价于 Q 为假在过去的情况。
~HQ ≅ P~Q时序逻辑中的推理规则：
时序逻辑中的以下推理规则可用于从现有知识中推断出新信息：
- 如果将来为真，则 Q 在将来为真，那么我们推断 Q 在将来为真。 FFQ -> FQ
- 如果 Q 现在为真，那么我们推断将来 Q 在过去为真。 Q -> FPQ
- 如果 Q 在过去一直是真的，那么我们推断 Q 是真的 HQ -> Q
- 如果 Q 在未来永远为真，那么我们推断 Q 为真。 GQ -> Q
- 分布公理：
– G(Q -> R) -> (GQ -> GR) 解释为如果 Q 总是这样蕴含 R，那么如果 Q 总是这样，那么 R 总是这样。
– H ( Q->R) -> (HQ -> HR) 解释为如果 Q 隐含了 R，那么如果 Q 一直如此，那么 R 将一直如此。