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

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

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