1996年度的圖靈獎授予了一位以色列學 者，著名的以色列魏茨曼學院(Weizmann Institute of Science，位於聖城耶 路撒冷西北約50公里的雷霍沃特)應用數學系教授艾米爾·伯努利(Amir Pnueli)，以彰顯他把時態邏輯引入電腦科學所做的貢 獻。

伯努利於1967年在魏茨曼學院獲應用數 學博士學位，後留校任教。他的主要研究方向是時態邏輯或叫 時序邏輯(temporal logic)。時態邏輯是非經典邏輯中的一種，它研究 如何處理含有時間資訊(現在、過去、將來；之前、之後等)的事件 的命題和謂詞。時態邏輯體系包含的要素有：

1. 基本符號：事件e，關係或謂詞r，時間區間i(interval)等。
2. 時態謂詞：after(e,r),before(e,r)等。
3. 時態事件演算規則：初始規則、終止規則等，如holds(before(e,r))： terminates(e,r)表終止規則，意為若事件已使謂詞r失效，則在e之前 且r成立以一段區間中r為真。
4. 時態邏輯運算：時態區間的並交，時態謂詞的與、或、非等。

1977年，伯努利把時態邏輯引入計算機 科學，把它作為開發反應式系統(reactivesystem)和併發式系統 (concurrentsystem)時進行規格說明(specification)和驗證(verification)的工具， 取得了極大的成功，在軟體工程界引起轟動，被認為是軟體工 程中的一場革命。伯努利也因此而聲名大振，他曾被斯坦福大 學，哈佛大學等著名高等學府聘為客座教授或進行講學。

伯努利主要從事教學和研究，但也和國 外絕大多數教授一樣，不限於“純學術”工作。他和別人一起在 美國馬薩諸塞州的Burlington辦了一個公司：iLogixInc，他任該公 司首席科學家。

伯努利和我國科學院院士、著名的邏輯 和軟體學家唐稚鬆是朋友和知交。唐稚鬆曾向伯努利建議，把 “時態邏輯”當作整個軟體開發過程(包括需求、規格說明、設計、 證實、驗證、程式碼生成和整合)的普遍的基礎，而不侷限於規格說 明和驗證。伯努利深受啟發並對唐先生的聰明和眼光大為贊 嘆。1995年8月，為慶祝唐稚鬆70壽辰，舉辦了一個名為“邏輯和軟 件工程”的國際專題討論會，伯努利帶了一篇新的論文來北京 參加了這個討論會，並負責編輯出版了會議論文集(Logicand Software Engineering: International Workshopin Honour of ChihSung Tang, Singapore: World Scientific Press,1996)。在論文集的前言中，伯努利敘述了他和唐稚鬆 之間的這段交往。

伯努利的代表作如下：

《The Temporal Logic of Reactiveand Concurrent Systems: Specification》(SpringerVerlag,1992)

《Temporal Verification of Reactive Systems: Safety》 (Springer Verlat, 1995)

伯努利現任斯普林格出版社著名的系 列叢書“Lecture Notesin Computer Science”的編委，也是有關領域的不少 雜誌如《Acta In formatica》、《Science of Computer Programming》、《Noteson Computer Science》的編委。

-------------------------------------------------------------------------------------------------------------------------------------------------------------------------

描述邏輯、時態邏輯、模態邏輯、非經典/現代邏輯

描述邏輯

描述邏輯(DescriptionLogic)是基於物件的知識表示的形式化，它吸取了KL-ONE的主要思想，是一階謂詞邏輯的一個可判定子集。除了知識表示以外，描述邏輯還用在其它許多領域，它被認為是以物件為中心的表示語言的最為重要的歸一形式。描述邏輯的重要特徵是很強的表達能力和可判定性，它能保證推理演算法總能停止，並返回正確的結果。在眾多知識表示的形式化方法中，描述邏輯在十多年來受到人們的特別關注，主要原因在於：它們有清晰的模型-理論機制；很適合於通過概念分類學來表示應用領域；並提供了很多有用的推理服務。

 
應用
　　由於描述邏輯在很多不同應用領域中都有較好的應用，這使得描述邏輯的結果變得越來越重要。實際上描述邏輯在許多領域中被作為知識表示的工具，如資訊系統（Catarci,1993）,資料庫（Borgida,1995;Bergamaschi1992;Sheth,1993）軟體工程(Devambu,1991)，網路智慧訪問（Levy，1996；Blanco，1994）和規劃（Seida,1992）。上述的許多文章中都指出，對許多相應的應用領域通常需要DL的整體能力。（Doyle1991）
 
演變發展
　　描述邏輯最開始只是用來表示靜態知識的。為了考慮在時間上的變化，或者在一定動作下的變化，以及保持其語言的相對簡單性，很自然地我們需要通過相應的模態運算元來擴充套件它，以保留其命題模態狀態。眾所周知，即使只是對簡單的模態系統的綜合，也可能會導致很複雜的系統。Schild，Schmiedel等人最初所構造的時序描述邏輯和認知邏輯要麼就是因為表達能力太強而導致不可判定性，要麼就是太弱（時態運算元僅僅對公式或者概念是可用的）。Baader和Laux[2]則進行了折中，將描述邏輯ALC與多型K相結合，允許將模態運算元使用到公式和概念上，並證明在擴充套件領域模型中的結果語言的滿足性問題是可判定的。Wolter等對具有模態運算元的描述邏輯進行了深入系統的調查分析，並證明在恆定的領域假設下多種認知和時序描述邏輯是可判定的。他將將描述邏輯和命題動態邏輯PDL相結合，提出了動態描述邏輯。 　　為了對動作和規劃能在統一的框架下進行表示和推理，A.Artale和E.Franconi(1998)提出了一個知識表示系統，用時間約束的方法將狀態、動作和規劃的表示統一起來。為了能使該表示方法進行有效的推理和具有明確的語義，它又和描述邏輯結合起來，從而形成了一個很好的知識表示方法。它具有以下優點：(i)能用統一的方法表示狀態、動作和規劃，這一點與情景演算不同；(ii)能進行高效的推理，該框架下的可滿足性問題和包含檢測問題等都是多項式時間；(iii)有明確的語義；(iv)能自動進行規劃識別。
 
可滿足性問題及理論推廣
　　可滿足性問題是描述邏輯推理中的核心問題，因為其它許多問題（如包含檢測、一致性問題等）都可化為可滿足性問題。為了能用計算機自動判斷描述邏輯中可滿足性問題，Schmidt-Schaub和Smolka首先建立了基於描述邏輯ALC的Tableau演算法，該演算法能在多項式時間內判斷描述邏輯ALC概念的可滿足性問題。目前，Tableau演算法已用於各種描述邏輯中（如ALCN、ALCQ等），並且Tableau演算法也可用於判斷例項檢測等問題。現在主要研究各種描述邏輯中Tableau演算法的擴充套件、複雜性及優化策略等。 　　為了能讓描述邏輯處理模態詞，F.Baader將模態操作引入描述邏輯。證明了該描述邏輯公式的可滿足性問題是可判定的。結合可能世界語義和可達關係，引入時間依賴和信念等模態操作，提出了多維描述邏輯框架，該描述邏輯較好的刻畫了多主體系統模型。目前，主要研究工作集中在建立合理的模態公理及多維描述邏輯。在描述邏輯中第一個整合時間的方法是由A.Schmiedel提出來的。他使用了兩個時間運算子來擴充套件描述邏輯，提出了在時間段上受限的全稱和存在量詞。Schild提出了一種簡單的時序擴張，利用時態邏輯(tenselogic)中在時間點“自從”Since和“直到”Until上的時序運算子來討論ALC邏輯。

時態邏輯

1996年圖靈獎獲得者：阿米爾?伯努利（Amir Pnueli）PhD, Weizmann Institute; Prof, NYU  ——  把時態邏輯引入電腦科學

阿米爾·伯努利（Amir Pnueli），出生於1941年4月22日於Nahalal，以色列。Amir Pnueli年青時代從以色列Technion - Israel Institute of Technology 技術學院獲得其數學學士學位，從以色列Weizmann Institute of Science獲得其應用數學博士學位。Pnueli的博士論文工作是關於"Cacluation of Tides in the Ocean"。

 　　阿米爾·伯努利（Amir Pnueli） ACM會士，1941年4月22日出生於以色列。在斯坦 福大學和IBM Waston研究中心從事博士後的研究工作其間，Pnueli將研究工作方向轉移到電腦科學領域。1999年，Pnueli加入美國紐約大學計算機科學系並出任教授。1996年授予Amir Pnueli 圖靈獎，以表彰其在電腦科學中引入時序邏輯的開創性的研究工作，和其在程式語言和系統驗證方面的突出貢獻。[1]

　　2009年11月2日 逝世
相關研究
　　把時態邏輯引入電腦科學 　　1996年度的圖靈獎授予了一位以色列學者，著名的以色列魏茨曼學院(Weizmann Institute Of Science，位於聖城耶路撒冷西北約50 km的雷霍沃特)應用數學系教授阿米爾·伯努利(Amir Pnueli)，以彰顯他把時態邏輯引入電腦科學所做的貢獻。 　　伯努利於1967年在魏茨曼學院獲應用數學博士學位，後留校任教。他的主要研究方向是時態邏輯或叫時序邏輯(temporal logic)。時態邏輯是非經典邏輯中的一種，它研究如何處理含有時間資訊(現在、過去、將來；之前、之後等)的事件的命題和謂詞。時態邏輯體系包含的要素有： 　

1．基本符號：事件e，關係或謂詞r，時間區間i(interval)等。 　　

2．時態謂詞：after(e，r)，before(e，r)等。 　　

3．時態事件演算規則：初始規則、終止規則等，如holds(before(e，r))：—terminates(e，r)表終止規則，意為若事件已使謂詞r失效，則在e之前且r成立的一段區間中r為真。

 4．時態邏輯運算：時態區間的並、交，時態謂詞的與、或、非等。 　　

1977年，伯努利把時態邏輯引入電腦科學，把它作為開發反應式系統(reactive system)和併發式系統(concurrent system)時進行規格說明(specification)和驗證(verification)的工具，取得了極大的成功，在軟體工程界引起轟動，被認為是軟體工程中的一場革命。伯努利也因此而聲名大振，他曾被美國斯坦福大學、哈佛大學等著名高等學府聘為客座教授或進行講學。 　　

伯努利和他的同事曼納(Z．Manna)共同開發的時態邏輯系統叫“命題線性時態邏輯系統”(Proposition Linear Temporal 1ogic，縮寫PLTL)。

PLTL包含可數無窮多個命題變元，邏輯聯結詞“否定”┐，“合取”∧，“析取”∨，“蘊含” ，“等價”≡；

時態運算元□，意為“任一時刻”；

◇，意為“某一時刻”；

○，意為“下一時刻”；

μ，意為“直到”。

合式公式（well-formed formula）在PLTL中的定義如下： 　

（1）命題變元P是合式公式； 　　

（2）若w、w1和w2是合式公式，則┐w、 w1∧w2、w1∨w2、w1 w2、w1≡w2都是合式公式；□W、◇W、○W和w1μw2也都是合式公式； 　　

（3）每個合式公式均可通過有限次應用（1）、（2）獲得。 　

　PLTL中包含10條公理和3條推理規則，它們是： 　　

公理1：┐◇w≡□┐w 　　

公理2：□(w1 w2) (□w1 □w2) 　　

公理3：□w w 　　

公理4：○┐w≡┐○w 　　

公理 5：○(w1 w2) (○w1 ○w2) 　　

公理6：□w ○w 　　

公理7：□w ○□w 　　

公理 8：□(w ○w) (w □w) 　　

公理9：(w1μw2) ≡(w2∨(w1∧○(w1μw2))) 　　

公理10： (w1μw2) ◇w2 　　

推理規則1(重言規則)：若u是命題重言式(tautology)，則├u 　　

推理規則2(假言推理規則)：若├u v且├u ，則├v 　　

推理規則3(口引入規則)：若├u，則├□u 　　

應用上述公理和推理規則，經過有窮步驟，可推匯出一系列合式公式，即PLTL的定理。 　

　顯然，PLTL是對普通命題邏輯(propositional lohic)的擴充，但這一擴充卻意義重大，因為這使系統具有了處理隨時間變化而改變其值的動態變元(稱為時序或時態變元)的能力。在時態邏輯中，時間的結構可以有線性、分支、離散、連續，基於時間點或時區的這樣幾種不同情況，可視具體應用背景而定。PLTL採用線性、離散，且與自然數同構的時間結構。它的語義解釋是一個無窮狀態序列σ=S0,S1,S2,…，每個Si都是對命題變元的一個賦值。

若令σ（i）=Si,si+1,si+2…，且用σ|=w表示時態公式w在解釋σ下為真，則各時態運算元的含義如下： 　　σ|=□w當且僅當對任意i≥0，均有σ（i）|=w 　　σ|=◇w 當且僅當存在i≥0，使σ（i）|=w 　　σ|=○w當且僅當σ（i）|=w 　　σ|=w1μw2當且僅當存在i≥0，使 σ（i）|=w2且對任意j(0)≤j<(i)均有σ（j）|=w1 　　

由於程式的行為是一種動態現象，其狀態是隨著時間的推移而不斷改變的，而這種改變又可能反過來影響其外部環境。併發反應式程式的這種持續的動態行為無法用經典邏輯描述，由著名的邏輯學家霍恩(A．Hom)於1951年提出，因而用他的名字命名的至多包含一個正文字的Hom子句所組成的霍恩邏輯也不能描述。而伯努利的PLTL則憑著它的極強的表達能力，填補了這一空白，成為研究併發程式尤其是持續不終止的反應式程式(如作業系統，網路通訊協議等)的強有力的形式化工具，可充分表達程式的安全性、活性和事件的優先性等，成為程式規約(specification)、驗證(verification)等的有力工具。 　

　值得指出的是，中國科學家在伯努利工作的基礎上，將時態邏輯用於電腦科學的研究大大地向前發展了一步。伯努利只把時態邏輯用於程式規約和驗證，而我國科學家唐稚鬆(中科院院士，軟體所研究員)在20世紀70年代末、80年代初把時態邏輯用於軟體開發的整個過程，包括需求定義、規約、設計、證實、驗證、程式碼生成和整合，並開發了世界上第一個可執行時態邏輯語言XYZ/E和一組相應的CASE工具，在國際上引起強烈反響。1979年，時任美國加州大學伯克利分校計算機科學系主任的布盧姆(M．Blum，計算複雜性理論奠基人之一，1995年圖靈獎獲得者)曾致信唐稚松本人，稱：“在美國，很有一些最重要的電腦科學家知道您及您的工作，他們都對您的研究工作作了高度評價”。伯努利本人也同唐稚鬆建立了聯絡，併成為朋友。1995年8月，為慶祝唐稚鬆70壽辰，舉辦了一個名為“邏輯和軟體工程”的國際專題討論會，伯努利和他的老搭擋曼納帶了一篇新的論文“有時鐘的變遷系統”(Clocked Transition System)來北京參加了這個討論會，並親自編輯出版了會議論文集(Logic and Software Engineering：International Workshop in Honour Of Chih-Sung Tang，Singapore：World Scientific Pr.，1996)。在論文集的前言中，伯努利高度評價了唐稚鬆的工作。 　　

伯努利主要從事教學和研究，但也和國外絕大多數教授一樣，不限於“純學術”工作。他和別人一起在美國馬薩諸塞州的布靈頓(Burlington)辦了一個公司：i—Logix Inc，他任該公司首席科學家。
研究成果
　　主要有： 　　《反應式系統和併發系統的時態邏輯：規約》(The Temporal Verification of Reactive and Concurrent Systems：Specification，Springer，1992) 　　《反應式系統的時態驗證：安全》(Temporal Verification of Reactive Systems：Safety，Springer，1995) 　　伯努利現任施普林格出版社(Springer Verlag)著名的系列叢書kecture Notesin Computer Science的編委，也是有關領域的不少雜誌如Acta lnformatica、Science Of Computer Programming、Notes On Computer Science的編委。