臺灣博碩士論文加值系統

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

TABLE OF CONTENTS
Chinese Abstract
Englisgh Abstract
List of Figures
1.Introduction
1.1 Motivation
1.2 Why Vector Processing
1.3 Synopsis of the Thesis
2.Preliminaries
2.1 Well Formed Formulas
2.2 Normal Forms
2.3 Theorem Proving Problem
2.4 Vector Instructions
3.Previous Works
3.1 The 2-CNF Satisfiability Problem
3.2 The Horn Satisfiability Problem
3.3 Theorem Proving Problem in Propositional Logic
4.Vectorization Techniques by Covering Vectors
4.1 The Basic Idea of the Vectorization Method
4.2 Proof by Covering Vectors
4.3 Computation of Covering Vectors by Merging
5.Vectorization Techniques Using Generalized Rules
5.1 The Basic Ideas
5.2 The Generalized Rules
5.3 Vectorization of the Generalized Rules
5.4 Techniques for Elimination of Clause Sets
5.5 The Vectorized Procedure
6.Experimental Results
6.1 Experiments on Covering Vectors
6.2 Experiments on the Generalized Rules
6.3 Discussion
7.Applications
7.1 Theorem Proving in the First Order Logic
7.2 Tautology Checking
7.3 Channel Routing
8.Concluding Remarks and Future Directions
8.1 Conclusions
8.2 Future Research Directions
參