Abstract
用計算機來作定理證明早已是人工智慧中的研究主題之一。在有關的文獻中，已有許多的證明程序。但是其中幾乎沒有平行的方法。在研究平行式定理證明中，我們發展出一種平行式的方法，它能比傳統用細分原理為基礎的證明程序更有效率。對於命題錐輯的定理證明，我們應用分割－征服的策略設計了一種有效率的平行式計算方法。這個平行式計算方法能在多項式時間內測試一個有限的命題邏輯式是否為不可滿足，因此它是目常有效率的。我們也證明此平行式計算方法是正確的。對於一階邏輯的定理證明，我們提出了一種平行式證程序，它能產生許多的地子句，同時測試他們是否為不可滿足。在這個證明程序中，一些永遠不會用在任何證明中的地子句不會產生，而產生的地子句也只被測試一次。因此我們的平行式證明程序也比其他程序更為有效率。我們也證明此平行式證明程序是正確的。我們也提出平行式計算模型來更進一步提升在命題邏輯中作定理證明之平行式計算方法的效率。這些模型都依據一種管線式的工作型式而建立。其中協調的方法、基本處理單位、模型的大小等均有討論。分析的結果顯示計算機結構及邏輯式的特性等都影響到效率。計算機結構，包括一種MIMD樹型機，一種簡化的樹型機，一種資料流計算機，以及一種混合式的結構都可用於這些平行式計算模型。我們建議最通用的結構是混合式的，因為它能很迅速地測試較小邏輯式之不可滿足性，同時也能用來測試較大的邏輯式。我們的平行式定理證明方法是非常系統化以及有效率。所提出的結構可以用VLSI晶片來設計。因此我們期望這種平行式定理證明方法可以用在邏輯程式設計，也可以用在新一代計算機系統中。