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

　　時(shí)序邏輯是人工智能和計(jì)算機(jī)科學(xué)領(lǐng)域中的重要建模工具。隨著時(shí)序邏輯的廣泛使用，應(yīng)用時(shí)序邏輯來對復(fù)雜系統(tǒng)進(jìn)行推理和驗(yàn)證的算法也應(yīng)運(yùn)而生。其中最成功的方法之一就是Resolution算法，這也是本書的主題。 1965年美國數(shù)理邏輯專家魯濱遜（J. A. Robinson）提出了一條Resolution推理規(guī)則，這標(biāo)志著Resolution算法的起點(diǎn)。因其簡潔性（整個(gè)推理過程中只使用一條推理規(guī)則）和便于機(jī)械操作的特點(diǎn)，Resolution算法得到了各國學(xué)者的重視，并且在各國學(xué)者的推動下發(fā)展得非常迅速。經(jīng)過幾十年的發(fā)展和持續(xù)的改進(jìn)，到目前為止，Resolution算法在經(jīng)典邏輯中已經(jīng)趨于成熟。 本書主要聚焦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ì)算樹邏輯（Computation Tree Logic）和其擴(kuò)展（Extended Computation Tree Logic） （3）交互時(shí)序邏輯（Alternating-Time Temporal Logic）

　　章嵐，2011年畢業(yè)于英國利物浦大學(xué)，并獲得博士學(xué)位（專業(yè)方向：計(jì)算機(jī)科學(xué)）?！≈饕芯糠较?yàn)槿斯ぶ悄?，?jì)算機(jī)邏輯，形式化驗(yàn)證（Formal Verification，Theoremproving）。　主講課程為《電子商務(wù)系統(tǒng)分析》、《數(shù)據(jù)庫應(yīng)用》、《專業(yè)外語》等。