淺談機器證明

淺談機器證明什么是機器證明？提問機器證明是指用計算機程序去自動完成事實的證明，如定理的證明、結(jié)論的推理等。要實現(xiàn)機器證明，必須用比較嚴格的知識表示方法。本節(jié)將介紹用歸結(jié)原理進行定理證明的思路，我們首先了解這種證明方法的知識表示，然后說明歸結(jié)原理的思想以及如何用它證明問題。1知識的表示在歸結(jié)原理中，可以使用以下兩種形式表示知識：（1）用謂詞表示知識，這種方法類似于Prolog語言中知識的表示形式。例1：事實：表示為子句例2：事實：表示為子句例3：事實：表示為子句Mary喜歡打球like(mary,ball)Mary不喜歡打球~like(mary,ball)John很幸運luck(John)（2）通過用符號“Ⅴ”將謂詞連接起來的子句表示知識，其中“Ⅴ”表示“或”的意思。例4：事實：表示為子句例5：事實：表示為子句Mary去打球或去看電影play(mary,ball)Ⅴsee(mary,film)Rose不是人，或Rose是會死的人~man(rose)Ⅴdie(rose)2歸結(jié)原理及其應(yīng)用簡述1965年魯濱遜提出了歸結(jié)原理。歸結(jié)原理的思想是：若子句AⅤBⅤC：及~AⅤD成立，則子句BⅤCⅤD成立。即A和~A可以互相抵消，而得BⅤCⅤD，其中A、B、C、D是謂詞或命題。利用歸結(jié)原理進行定理證明的步驟如下：（1）寫出事實的子句集；（2）寫出要證明問題的子句；（3）將要證明的問題子句“否定”化，然后將其加入到事實的子句集中；（4）反復(fù)用歸結(jié)原理，對子句集中的子句進行歸結(jié)（進行消解），并將產(chǎn)生的子句加入到子句集中。若歸結(jié)得到一個“空子句”，則推理成功，從而定理得證。例6：若下面事實成立：（1）狗不是動物或狗不是麒麟；（2）狗是動物。證明“狗不是麒麟”這一命題為真。證明：第一步，寫出事實的子句集：（1）~animal(dog)Ⅴ~kylin(dog)（2）animal(dog)第二步，寫出待證結(jié)論的子句形式：kylin(dog)第三步，將結(jié)論的子句“否定”化后，加入到由事實子句構(gòu)成的子句集中。（3）kylin(dog)第四步，反復(fù)用歸結(jié)原理，對子句集中的子句進行歸結(jié)，并將產(chǎn)生的子句加入子句集中。子句（1）和子句（2）進行歸結(jié)，得：（4）~kylin(dog)子句（3）和子句（4）進行歸結(jié)，得：（5）NIL（NIL表示空子句）歸結(jié)得到一個空子句，結(jié)論~kylin(dog)成立。例7：若下面事實成立：（1）Rose不是人，或Rose是會死的人；（2）Rose是人。證明“Rose是會死的人”這一命題為真。證明：事子句集：（1）~man(rose)Vdie(rose)（2）~man(rose)將待證結(jié)論否定，得：（3）~die(rose)子句（1）和子句（2）進行歸結(jié)，得：（4）die(