謂詞邏輯是在命題邏輯的基礎(chǔ)上發(fā)展而來的，通過引入量詞，它比命題邏輯能更有效地表示和求證復(fù)雜問題。謂詞邏輯采用形式化語言系統(tǒng)，通過一定的推理規(guī)則和控制策略，研究前提和結(jié)論之間的蘊(yùn)涵關(guān)系。謂詞邏輯具有嚴(yán)格的理論基礎(chǔ)，可以保證推理過程和結(jié)論的正確性，同時(shí)它的形式化語言接近人類的自然語言，容易為人類所理解和接受。

　　經(jīng)典的演繹推理系統(tǒng)具有證明過程自然、易于理解、推理規(guī)則豐富、推理過程靈活等優(yōu)點(diǎn)，但也存在推理過程中容易產(chǎn)生組合爆炸、證明方法難以判定等缺點(diǎn)。Robinsonc于1 965年借助演繹推理反證法的思想提出了歸結(jié)原理，它是一種形式單一、處理規(guī)則簡單，可以在機(jī)器上實(shí)現(xiàn)的邏輯推理技術(shù)。歸結(jié)原理的提出，為人類提供了一種簡單易行的方法實(shí)現(xiàn)定理的證明和問題的求解，使定理證明可以在機(jī)器上機(jī)械現(xiàn)實(shí)，是自動(dòng)推理的重大突破。

　　本文從理論基礎(chǔ)、求證問題的方法及步驟方面對基于謂詞邏輯的歸結(jié)原理進(jìn)行了研究。論文的組織結(jié)構(gòu)如下：第2節(jié)分析了基于謂詞邏輯的歸結(jié)原理的理論基礎(chǔ)；第3節(jié)討論了將基于謂詞邏輯的歸結(jié)原理應(yīng)用于定理證明和問題答案提取的方法及步驟；最后對全文進(jìn)行了總結(jié)。