矛盾體分離單元結(jié)果演繹方法及應(yīng)用

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