| 详细摘要 | 第1-10页 |
| 1. Introduction | 第10-12页 |
| ·Motivation | 第10-11页 |
| ·Main work and future work | 第11页 |
| ·Organization of the thesis | 第11-12页 |
| 2. Preliminaries | 第12-19页 |
| ·Propositional logic | 第12-14页 |
| ·Basic definitions | 第14页 |
| ·MU(1) and Basic Matrix | 第14-16页 |
| ·Tree-resolution proof | 第16-19页 |
| 3. Basic Result on MU(1) | 第19-23页 |
| ·Important statements on MU formulas | 第19-20页 |
| ·Two Basic Result on MU(1) | 第20-23页 |
| 4. The Extension of CNF | 第23-29页 |
| ·Case1 and Case2 | 第23-25页 |
| ·Case3 and Case4 | 第25-27页 |
| ·The algorithm deciding CNF-to-MU(1) | 第27-28页 |
| ·Time complexity of the algorithm | 第28-29页 |
| Acknowledgements | 第29-30页 |
| Bibliography | 第30-33页 |
| Publications | 第33-34页 |
| 原创性声明 | 第34页 |
| 关于学位论文使用授权的声明 | 第34页 |
