大家好我是执念斩长河。今天讲述的是1996年图灵奖获得者阿米尔·伯努利。图灵奖奖励他将时态逻辑引入计算机科学。读完本篇博文大家可以收获的是:
- 什么是时态逻辑
- 时态逻辑包含哪些
- 伯努利的时态逻辑系统
- 伯努利的著作
伯努利于1967年在魏茨曼学院获应用数学博士学位,后留校任教。时态逻辑是非经典逻辑的一种,他研究如何处理含有时间信息(现在、过去、将来);之前、之后等)的时间命题和谓词。时态逻辑体系包含的要素有:
- 基本符号:事件e,关系或谓词r,时间区间i等
- 时态谓词:after(e,r),before(e,r)等
- 事态事件演算规则:初始规则、终止规则等
- 时态逻辑运算:时态区间的并、交、时态谓词的与、或、非等。
伯努利和他的同事曼纳共同开发的时态逻辑系统叫“命题线性时态逻辑”。这个系统可以拿来推导公式用或者证明定理。伯努利的主要著作:
- 《反应式系统和并发系统的时态逻辑:规约》
- 《反应式系统的时态验证:安全》