本文關(guān)鍵詞：非確定動作推理的霍爾證明系統(tǒng)

  更多相關(guān)文章： 動作語言 規(guī)劃生成與驗證 循環(huán)規(guī)劃 霍爾邏輯

【摘要】：人工智能規(guī)劃(AI planning)是人工智能領(lǐng)域的一個重要研究方向,它主要研究智能主體在給定一系列關(guān)于動作的描述的前提下,如何生成一個規(guī)劃(plan)以完成被賦予的任務(wù)或目標。為了更好地進行規(guī)劃,我們需要研究動作能夠執(zhí)行的前提和其產(chǎn)生的效果,以及其效果對世界狀態(tài)和主體的認知狀態(tài)的影響,這屬于動作推理的范疇,是人工智能規(guī)劃的一個分支。對動作推理的研究,有助于我們預(yù)測某一個動作序列所產(chǎn)生的最終效果,以及驗證其能否實現(xiàn)目標,從而幫助我們更好地提出一個可行規(guī)劃。相對于傳統(tǒng)的完全信息的序列規(guī)劃(規(guī)劃是一個動作序列),不完全信息下的循環(huán)規(guī)劃(帶有循環(huán)結(jié)構(gòu)的規(guī)劃)因更具一般性和簡潔性,而受到越來越多的關(guān)注。盡管已有許多學(xué)者對帶循環(huán)的規(guī)劃問題的算法方面進行研究,然而其語義方面卻沒有得到足夠的重視,大量例子表明,程序語言的形式語義也是非常重要的。本文在綜合考慮和比較動作推理的主要邏輯表達方式后,決定采用具有類似于自然語言語法的動作語言來研究動作推理的性質(zhì)以及相關(guān)問題,以兩個例子作為動機,將感知動作、非確定動作和循環(huán)在動作語言中結(jié)合,得到動作語言ALK以處理在非確定論域下帶循環(huán)的規(guī)劃問題,然后給出AL K的兩個基于轉(zhuǎn)移系統(tǒng)的形式語義——通用語義和0-逼近語義。接著,基于0-逼近語義,我們?yōu)锳L K構(gòu)造一個可靠且(相對)完全的霍爾證明系統(tǒng),用于規(guī)劃的生成和驗證。該系統(tǒng)使用了知識編譯中的離線編譯和在線推理的思想,使得智能主體能夠利用空閑的時間和空間,盡可能多地驗證相對較短的規(guī)劃,然后使用系統(tǒng)中的組合性規(guī)則將這些已驗證的規(guī)劃組合成較長的規(guī)劃,以完成快速的在線回答。換句話說,智能主體可以利用已有的規(guī)劃生成和驗證新的規(guī)劃,從而大大提高實際規(guī)劃的效率。我們認為,本文構(gòu)建的形式語義以及證明系統(tǒng)均可作為帶循環(huán)的動作推理的邏輯基礎(chǔ)。
【學(xué)位授予單位】：中山大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2016
【分類號】：B812.3

【參考文獻】

中國期刊全文數(shù)據(jù)庫 前1條

1 SHEN YuPing;ZHAO XiShun;;Proof systems for planning under 0-approximation semantics[J];Science China(Information Sciences);2014年07期

，

本文編號：1190270