Abstract
在人工智慧的領域中，自動定理證明一直是研究的主題之一，雖然其中較簡單的命題邏輯已經被證明是一個NP完全的問題，也就是說：到目前為止，在最差的情況下它必須花與指數次方成正比的時間才能得到結果，往往這需要很久，而更難的第一階邏輯定理證明的問題則被歸於是不可決定的，也就是說：不可能存在有計算方法來決定任何一個第一階邏輯敘述是對的或錯的，但是對於一矛盾化定理，證明程序是存在的，可用來證明此一定理的錯誤性，因此有許多證明程序相繼被提出來，當中大部份是基於Herbrand的基本定理或者是Robinson的分解理論，它們共同的特點是以第一階邏輯方式來表示定理，並且利用反證法來證明此矛盾化定理的錯誤性。除此以外，也有少數一些使用異於第一階邏輯的方式來解決幾可或代數上的問題，但是它們不在本論文的討論範圍內。雖然有許多證明程序被提出，但通常它們仍需花許多時間才得到結果。因此我們考慮：若是能將此一問題平行化解決，或許會節省許多時間。所以，在研究定理證明後，我們利用分解理論修改在命題邏輯上非常著名的Davis 和Putnam程序中的分離律使得它能夠被應用於第一階邏輯定理證明後。而且配上分解後合併的方式設計出一計算方法，能夠證明一組矛盾化定理的錯誤性。由於此一計算方法能夠被平行化，預期將會比傳統的證明程序有效。最後我們用此一分解後合併的程式證明一些群論上的基本定理。