淺談機(jī)器證明

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