機(jī)器定理證明

機(jī)器定理證明推理技術(shù)01基本信息恒真性目錄02基本信息把人證明數(shù)學(xué)定理和日常生活中的演繹推理變成一系列能在計(jì)算機(jī)上自動(dòng)實(shí)現(xiàn)的符號(hào)演算的過(guò)程和技術(shù)，又稱自動(dòng)定理證明和自動(dòng)演繹?；拘畔⒒拘畔C(jī)器定理證明是人工智能的重要研究領(lǐng)域，它的成果可應(yīng)用于問(wèn)題求解、自然語(yǔ)言理解、程序驗(yàn)證和自動(dòng)程序設(shè)計(jì)等方面。數(shù)學(xué)定理證明的過(guò)程盡管每一步都很嚴(yán)格有據(jù)，但決定采取什么樣的證明步驟，卻依賴于經(jīng)驗(yàn)、直覺(jué)、想象力和洞察力，需要人的智能。因此，數(shù)學(xué)定理的機(jī)器證明和其他類型的問(wèn)題求解,就成為人工智能研究的起點(diǎn)。早在17世紀(jì)中葉，萊布尼茲就提出過(guò)用機(jī)器實(shí)現(xiàn)定理證明的思想。19世紀(jì)后期G.弗雷格的“思想語(yǔ)言”的形式系統(tǒng)，即后來(lái)的謂詞演算，奠定了符號(hào)邏輯的基礎(chǔ)，為自動(dòng)演繹推理提供了必要的理論工具。20世紀(jì)50年代，由于數(shù)理邏輯的發(fā)展,特別是電子計(jì)算機(jī)的產(chǎn)生和應(yīng)用,機(jī)器定理證明才變?yōu)楝F(xiàn)實(shí)。A.紐厄爾和H.A.西蒙首先用探試法實(shí)現(xiàn)了用以證明命題邏輯中重言式的邏輯理論家系統(tǒng)LT。后來(lái)，開(kāi)始探討通用的機(jī)器定理證明的方法，歸結(jié)原理是其中突出的例子。恒真性恒真性歸結(jié)原理和非歸結(jié)定理證明一階謂詞邏輯的恒真性問(wèn)題是不可解的，即不存在能判定一階邏輯中任意合式公式是不是恒真式的算法，但是這個(gè)問(wèn)題又是部分可解的。如果A是恒真式,那么必有算法可以證明。許多一階邏輯的證明算法都以J.厄爾布朗定理為基礎(chǔ)，其中以1965年J.A.魯賓遜提出的、對(duì)于一階邏輯是完備的證明算法即歸結(jié)原理最為著名。歸結(jié)原理的提出，把機(jī)器定理證明的研究推向高潮。但歸結(jié)原理不依賴于領(lǐng)域知識(shí)，不使用依賴問(wèn)題領(lǐng)域的探試法，證明過(guò)程冗長(zhǎng)，不能在合理的時(shí)間和計(jì)算機(jī)存儲(chǔ)容量?jī)?nèi)證明較為復(fù)雜的數(shù)學(xué)定理，因此人們又提出非歸結(jié)定理證明方法，后來(lái)又對(duì)以探試法為基礎(chǔ)的問(wèn)題求解技術(shù)發(fā)生興趣。與此同時(shí)還出現(xiàn)了因否定歸結(jié)原理進(jìn)而否定所有自動(dòng)演繹方法的傾向。但是人工智能所要解決的問(wèn)題，其信息往往是不完全的，而且即使信息完全，要對(duì)有限的但為數(shù)眾多的情形一一列舉,實(shí)際上也不可行,因而只有用演繹推理的方法。邏輯程序設(shè)計(jì)和日本以PROLOG為原型開(kāi)發(fā)第五代計(jì)算機(jī)系統(tǒng)的核語(yǔ)言，進(jìn)一步恢復(fù)了歸結(jié)原理和自動(dòng)演繹技術(shù)的地位。人工智能的歷史表明，以認(rèn)知心理學(xué)為基礎(chǔ)的探試法和以邏輯為基礎(chǔ)的自動(dòng)演繹相輔相成，不可偏廢。自動(dòng)演繹與探試法等技術(shù)相結(jié)合而不用歸結(jié)原理的定理證明技術(shù)，主要用于數(shù)學(xué)定理的機(jī)器證明。幾何定理的機(jī)器證明在數(shù)學(xué)定理機(jī)器證明中，有一類問(wèn)題已有判定算法，如1951年W.斯米列夫給出的阿貝爾群判定算法，1951年A.塔斯基給出的初等幾何和代數(shù)的判定算法，1960年王浩提出的命題邏輯判定算法和1976年以來(lái)吳文俊提出的初等幾何