關(guān)于我們
書(shū)單推薦
新書(shū)推薦

基于時(shí)序邏輯的Resolution自動(dòng)定理證明方法

基于時(shí)序邏輯的Resolution自動(dòng)定理證明方法

定  價(jià):55 元

        

  • 作者:章嵐
  • 出版時(shí)間:2021/9/1
  • ISBN:9787563832668
  • 出 版 社:首都經(jīng)濟(jì)貿(mào)易大學(xué)出版社
  • 中圖法分類:TP301.6 
  • 頁(yè)碼:
  • 紙張:膠版紙
  • 版次:
  • 開(kāi)本:16開(kāi)
9
7
8
8
3
7
2
5
6
6
6
3
8

時(shí)序邏輯是人工智能和計(jì)算機(jī)科學(xué)領(lǐng)域中的重要建模工具。隨著時(shí)序邏輯的廣泛使用,應(yīng)用時(shí)序邏輯來(lái)對(duì)復(fù)雜系統(tǒng)進(jìn)行推理和驗(yàn)證的算法也應(yīng)運(yùn)而生。其中成功的方法之一就是Resolution算法,這也是本書(shū)的主題。
1965年美國(guó)數(shù)理邏輯專家魯濱遜(J. A. Robinson)提出了一條Resolution推理規(guī)則,這標(biāo)志著Resolution算法的起點(diǎn)。因其簡(jiǎn)潔性(整個(gè)推理過(guò)程中只使用一條推理規(guī)則)和便于機(jī)械操作的特點(diǎn),Resolution算法得到了各國(guó)學(xué)者的重視,并且在各國(guó)學(xué)者的推動(dòng)下發(fā)展得非常迅速。經(jīng)過(guò)幾十年的發(fā)展和持續(xù)的改進(jìn),到目前為止,Resolution算法在經(jīng)典邏輯中已經(jīng)趨于成熟。
本書(shū)主要聚焦Resolution算法在時(shí)序邏輯領(lǐng)域的研究,詳細(xì)介紹了把Resolution算法從表達(dá)能力較弱的時(shí)序邏輯逐漸向表達(dá)能力較強(qiáng)的時(shí)序邏輯進(jìn)行拓展和優(yōu)化的研究成果。主要涉及以下幾種時(shí)序邏輯:
(1)線性時(shí)序邏輯(Propositional Linear-Time Temporal Logic)
(2)計(jì)算樹(shù)邏輯(Computation Tree Logic)和其擴(kuò)展(Extended Computation Tree Logic)
(3)交互時(shí)序邏輯(Alternating-Time Temporal Logic)

 你還可能感興趣
 我要評(píng)論
您的姓名   驗(yàn)證碼: 圖片看不清?點(diǎn)擊重新得到驗(yàn)證碼
留言內(nèi)容