情景演算中的關鍵推理技術及其套用研究

《情景演算中的關鍵推理技術及其套用研究》是依託中山大學，由劉詠梅擔任項目負責人的面上項目。

基本介紹

• 中文名：情景演算中的關鍵推理技術及其套用研究
• 項目類別：面上項目
• 項目負責人：劉詠梅
• 依託單位：中山大學

中文摘要

認知機器人學研究在動態改變著和信息不完備的環境中的機器人或智慧型體所面臨的知識表示及推理問題。 其長遠目標是為知識、感知和動作的集成提供一個統一的理論與實現框架。認知機器人學的研究已被套用於許多領域，如機器人學、計算機遊戲和動畫，以及語義網服務組合。在認知機器人學研究中，其知識表示語言已發展得相當完善，如最常用的語言是情景演算，並在此基礎上設計了高級機器人程式設計語言Golog。但是，目前認知機器人學研究也面臨著兩個極其關鍵的問題：一是關於動態系統的有效推理問題，二是不完備知識和感知下的高級控制問題。本項目旨在探討情景演算中的有效推理技術，如如何有效地解決預測問題、檢查狀態約束和目標可達性，如何有效地更新知識庫以反映動作執行對世界狀態以及智慧型體知識狀態的改變等。同時，把這些推理技術套用於不完備知識和感知下的高級控制問題。

結題摘要

關於動作和變化推理的最常用形式化語言是情景演算。本項目研究情景演算中的關鍵推理技術及其在不完備知識和感知下的高級智慧型體控制中的套用。演進是在執行一個動作後更新智慧型體對世界狀態的表示。我們通過套用模態邏輯中的互模擬概念把演進的定義擴展到能夠反映動作對智慧型體知識狀態的改變。通過遺忘技術，我們證明了對於只產生局部效果的動作來說，當初始知識庫為我們所識別的某種範式形式時，知識的演進總是在一階模態邏輯中可定義的和可計算的。在動態系統中，狀態約束是在任何可達狀態下都成立的邏輯公式。因而關於狀態約束的推理是一個二階邏輯的推理問題。我們針對一類包括許多標準規劃問題的動作理論，提出了一個自動驗證並發現量詞前綴為若干個全稱量詞後跟若干個存在量詞的狀態約束的合理但不完備的方法，並用SAT求解器進行實現。實驗表明，我們的方法是高效的，並能比已有的工作發現更多的狀態約束。Golog是一個基於情景演算的用於高級智慧型體控制的邏輯程式設計語言。然而，Golog的現有實現主要是基於封閉世界假設或其變種；並且幾乎都是基於回歸的。基於精確演進和受限推理，我們提出並實現了帶感知的基於知識的Golog的一階解釋器。情景演算主要關注的是單智慧型體情形下物理動作的推理；而動態認知邏輯主要關注的是多智慧型體情形下認知動作的推理，其中的一個重要概念是動作模型，用以表示不同智慧型體對同一動作的不同視角。借鑑動作模型的概念，我們給出了情景演算的一個多智慧型體擴展，並證明了動作模型邏輯可以被嵌入到擴展後的情景演算中。智慧型體的一項基本能力是解釋診斷的能力，即猜測已發生的動作以解釋所得到的觀察。我們在動態認知邏輯的框架下對多智慧型體解釋診斷任務進行了形式化。由於這個任務一般來說是不可判定的，我們識別了其重要可判定片斷。本項目組已在國際人工智慧頂級會議IJCAI和AAAI上發表論文5篇。