面向機(jī)器人規(guī)劃的形式化研究.pdf

1、機(jī)器人規(guī)劃是機(jī)器人領(lǐng)域中的一個(gè)重要分支，是問題求解的重要手段。本文以定理證明器HOL4為研究平臺，采用定理證明方法對機(jī)器人規(guī)劃進(jìn)行了形式化研究，主要完成的工作包括:
　　首先對機(jī)器人、機(jī)器人規(guī)劃、形式化方法、定理證明、HOL4系統(tǒng)等相關(guān)知識進(jìn)行了深入研究與總結(jié)。
　　然后對關(guān)于機(jī)器人的STRIPS規(guī)劃進(jìn)行了形式化分析與建模，歸納總結(jié)了STRIPS規(guī)劃系統(tǒng)中世界模型、F規(guī)則以及操作方法三個(gè)部分的主要知識。接著對STRIPS規(guī)劃

2、領(lǐng)域中世界模型以及F規(guī)則等領(lǐng)域知識進(jìn)行了抽取與形式化建模，并在構(gòu)造基本操作函數(shù)的基礎(chǔ)上，封裝形成規(guī)則庫，作為一個(gè)整體供用戶使用。同時(shí)，總結(jié)了在HOL4系統(tǒng)中建立STRIPS規(guī)則庫的一般性方法與流程，并給出了本文建立的STRIPS規(guī)則庫的完整結(jié)構(gòu)與內(nèi)容。
　　最后，本文完成了STRIPS規(guī)則庫在機(jī)器人規(guī)劃相關(guān)問題中的應(yīng)用:以block world規(guī)劃為例，在HOL4系統(tǒng)中驗(yàn)證了block world規(guī)劃中動(dòng)作序列的可達(dá)性問題。完成了