| 摘要 | 第6-7页 |
| Abstract | 第7-8页 |
| Chapter 1 Preface | 第11-16页 |
| 1.1 Research Background | 第11-13页 |
| 1.2 Current Research Statuses | 第13-14页 |
| 1.3 Structure of This Paper | 第14-16页 |
| Chapter 2 Preliminaries | 第16-26页 |
| 2.1 Definitions | 第16-20页 |
| 2.2 Simplification Techniques | 第20-26页 |
| Chapter 3 Redundant Clauses | 第26-31页 |
| 3.1 Redundancy and Irredundant Equivalent Subsets | 第26-27页 |
| 3.2 Relatively Redundancy and Absolute Redundancy | 第27-31页 |
| Chapter 4 Redundant Literals | 第31-40页 |
| 4.1 Formulae Implying Literals | 第31-34页 |
| 4.2 Equivalent Description of Redundant Literals | 第34-40页 |
| Chapter 5 Judgment of the Redundancy of Set of Clauses | 第40-48页 |
| 5.1 Subformulas in Propositional Logic | 第40-43页 |
| 5.1.1 Satisfiable Core | 第40-41页 |
| 5.1.2 Minimally Unsatisfiable Subformulas | 第41-43页 |
| 5.2 Judgment of the Redundancy of Set of Clauses | 第43-48页 |
| Conclusions and Future Works | 第48-50页 |
| Acknowledgments | 第50-51页 |
| Reference | 第51-56页 |
| Appendix: procedures for removing redundant clauses | 第56-72页 |
| List of Publications and Research Projects | 第72页 |
