时态逻辑演算(数据库)

时间：2022-11-10 14:30:01 | 来源：信息时代

时间：2022-11-10 14:30:01 来源：信息时代

    时态逻辑演算 : 时态元素(例如时间点和时间区间)和时态信息的逻辑演算体系。
通常,对时态信息及知识的表达和推理,需要通过时态逻辑演算来实现。时态知识是指具有时态约束和时间属性的知识。典型的时态逻辑演算方法有Allen时态演算、时态操作符、TANDTL方法、时态逻辑和有效时间约束规则等。
1. Allen时态演算
Allen在1983年提出了一种基于时间段的时态逻辑方法,提出了13种时间区间关系,其中,有如下7对关系可以互相转换:
before(t₁,t₂₎＝after(t₂,t₁);
during(t₁,t₂₎＝contains(t₂,t₁);
overlaps(t₁,t₂₎＝overlapped-by(t₂,t₁);
meets(t₁,t₂₎＝met-by(t₂,t₁);
starts(t₁,t₂₎＝started-by(t₂,t₁);
finishes(t₁,t₂₎＝finished-by(t₂,t₁);
equals(t₁,t₂₎＝equals(t₂,t₁)。
为了表示原子执行于时间段T内,Allen使用了两个谓词: HOLDS(p,T)和IN(t,T)。HOLDS(p,T)表示原子p执行于时间段T内,而IN(t,T)表示时间子段t蕴涵在时间段T内。
2.时态操作符
时态操作符(temporal operator)又称为时态算子方法,与Allen的方法不同之处在于它是基于时间点的逻辑演算模型。有如下的标准时态算子:
(1)next A: 在随后的下一时间点,A为true。
(2)last A: 在上一时间点,A为true。
(3)always in the future A:从时间点T开始,A一直为true。
(4)always in the past A:在时间点T以前的时间,A一直为true。
(5)sometimes in the future A:在时间点T以后的某个时间点T₁,A为true。
(6)sometimes in the past A:在时间点T以前的某个时间点T₁,A为true。
(7)A until B: 当且仅当A与B分别在时间点t和T₁为true,且时序关系满足T<t<T₁时,A until B在时间点T为true。
(8)A since B:当且仅当A与B分别在时间点t和T₁为true,且时序关系满足T₁<t<T时,A since B在时间点T为true。
3. 时态逻辑
模态逻辑为计算机科学的研究提供了一种非真值系统,并成为一种形式化的途径,模态词可用来表示“知道”、“相信”等概念。Arthur Prior在1960年提出了时态逻辑(原名为: tense logic),将时间因素引入模态逻辑,从而将模态算子□解释为“将永远”(henceforth),◇解释为“将会”(eventully)。以后的逻辑学家和计算机科学家在此基础上进一步发展了时态逻辑(temporal logic)。Tense Logic的逻辑语言包括四个模态算子: P、F、H和G。其含义如下:
(1)P: 过去的某个时间是……
(2)F: 未来的某个时间是……
(3)H: 过去一直是……
(4)G: 未来一直是……
4. TANDTL方法
TANDTL是在the and then (TAND) connective基础上发展起来的一种时态逻辑语言,一是它在时态运算符方面做了简化,二是在处理实时并发事件时,对传统时态逻辑进行了改进,并配备了专用开发语言GSL。
在and_then(TAND)中,就算两个事件发生在两个不同区间,一旦它们用逻辑连接词AND(∧)连接,则被当作发生在同一区间。其基于时间点的语义描述如下:
(1)在任何时间里T都是真的。
(2)在任何时间里F都是假的。
(3)A成真, 当且仅当A在任意给定的时间里都成假。
(4)A∧B是真的当且仅当A和B在任意给定的时间里,都同时为真。
(5)A∨B是真的当且仅当A和B在任意给定的时间里,至少有一个为真。
(6)A∏B为真,当且仅当A在t时刻为真而B在t+1时刻为真。
(7)A=>B,当且仅当A为假或B为真。
(8)A=B,为真当且仅当他们有共同的真值表。
5.有效时间约束规则
产生式规则是经典知识表达方法之一,适合表达“前提-结论”型规则知识。由于许多知识具有不确定性,传统产生式规则采用可信度、概率等方法约束不确定性。时态性知识在“有效时间”区间内具有确定性,其推理需要考虑“时态”。采用有效时间约束的产生式规则称为有效时间约束规则(validtime-based rule),或称时态规则(temporal rule)。
时态规则的简单描述为: IF Rule-LogicExp THEN Actions Rule-Validtime。
规则前件Rule-LogicExp是传统的逻辑表达式,规则后件Action 可以是程序或其他动作,Rule-Validtime是有效时间,表示该规则有效的时间区间。
有效时间约束规则推理的前提是具有时态性的事实(事实库是时态数据库),即事实也需要有有效时间约束,时态事实可以描述为T-Fact(FactLogicExp,F-validtime)。时态规则的匹配过程是一个“时态驱动”过程,即首先要判断Rule-LogicExp和Fact-LogicExp是否匹配,同时要通过时态区间演算(例如采用Allen时态区间演算)进行时态有效性演算,判断“满足”时态事实的时态规则是否“时态有效” ,即 IN(Fact-LogicExp,Rule-LogicExp)或Overlap(Fact-LogicExp,Rule-LogicExp)等是否真。