摘要： 一階邏輯自動(dòng)定理證明是人工智能領(lǐng)域重要的研究?jī)?nèi)容。為提高單元結(jié)果歸結(jié)演繹效率,提出了一種新的基于多元、動(dòng)態(tài)、協(xié)同的單元結(jié)果演繹方法,稱為矛盾體分離單元結(jié)果演繹方法,并詳細(xì)地給出了其演繹定義、演繹方法、演繹的優(yōu)勢(shì)分析及算法實(shí)現(xiàn);提出的演繹方法允許多個(gè)子句同時(shí)參與演繹,且允許多個(gè)非單元子句參與1次單元結(jié)果演繹,能較好地處理長(zhǎng)子句;提出的演繹算法能使用策略選定較優(yōu)的子句和動(dòng)態(tài)設(shè)定變?cè)?.. （共9頁(yè)）