[科普中國(guó)]-定理證明

數(shù)學(xué)領(lǐng)域中對(duì)臆測(cè)的定理尋求一個(gè)證明，一直被認(rèn)為是一項(xiàng)需要智能才能完成的任務(wù)。

證明定理時(shí)，不僅需要有根據(jù)假設(shè)進(jìn)行演繹的能力，而且需要有某些知覺(jué)的技巧。例如數(shù)學(xué)家在求證一個(gè)定理時(shí)，會(huì)熟練地運(yùn)用他豐富的專(zhuān)業(yè)知識(shí)，猜測(cè)應(yīng)當(dāng)先證明哪一個(gè)引理，精確判斷出已有的那些定理將其作用，并把主問(wèn)題分解為若干問(wèn)題，分別獨(dú)立進(jìn)行求解。

因此人工智能研究中機(jī)器定理證明很早就受到注視。在人工智能的發(fā)展時(shí)期，1957年A.Newell、J.Shaw和H.Simon等人的心理學(xué)小組編制出一個(gè)稱(chēng)為1邏輯理論機(jī)LT（The Logic Theory Machine）的數(shù)學(xué)定理證明程序，該程序證明了B.A.W.Russell和A.N.Whitehead的“數(shù)學(xué)原理”一書(shū)第二章的38個(gè)定理。并取得不少成果。

（1） 先想出大致的解題計(jì)劃；

（2） 根據(jù)記憶中的公理定理和推理規(guī)則組織解題過(guò)程；

（3） 進(jìn)行方法和目的分析，修正解題計(jì)劃。

由此可見(jiàn)定理證明在人工智能的發(fā)展中已取得不少成果。

定理證明的研究在人工智能方法的發(fā)展中曾起到重要的作用，例如使用謂詞邏輯語(yǔ)言，其演繹過(guò)程的形式體系研究，幫助人們更清楚地理解推理過(guò)程的各個(gè)組成部分。

許多其他領(lǐng)域的問(wèn)題，如醫(yī)療診斷信息檢索等也可以應(yīng)用定理證明的方法，因此機(jī)器定理證明的研究具有普遍意義。