Abstract
定理證明之主要研究課題在於尋找一自動化之程序以決定邏輯理論中之任一定則是否為真。在數學以及其他領域中有很多問題都可以表示成定理證明問題, 它不僅是人工智慧領域中之重要研究項目, 並且是自動推理之核心理論。然而命題邏輯之定理證明已知是屬於NP完全性的問題, 而首階邏輯之定理證明甚至是不可決定性的問題。因此考慮用平行處理方式以加快自動定理證明之過程, 實有其必要性。本論文在探討定理證明之向量化處理技術, 首先我們提出一種向量表示法。利用這種方法, 在邏輯定則中之每一個子句都可以表示成一個向量。爾后只要以很簡單的AND、OR向量運算即可進行推理之步驟。此外, 又為了施行邏輯句集之化簡及考慮擴展問題之向量性, 我們在證明程序中加入數條推論法則, 這些法則可在每一推理步驟同時考慮多重因數以進行推論, 利用這種特性, 再配合向量運算之使用, 我們可以建造出一向量程度化相當高之證明程序。我們將此向量化證明程序在向量電腦上實現以驗證其效能, 實驗結果顯示經過向量化后之證明程序對提昇定理證明之速度有相當大之助益。最后我們指出幾個潛在的應用領域, 例如首階之定理證明、邏輯同義之驗證、及超大型積體電路之佈局等, 這些問題經過適當轉換, 都可以表示成命題邏輯之定理證明,並利用我們所提出之向量化程序加快其執行。