Computational Complexity of Automated Theorem Proving

自动定理证明系统是人工智能领域的热门课题之一，受到众多研究者的讨论。然而，由于缺乏对其基础的分析，使其没有实际应用的前景。在本研究工作中，我们讨论了一个重言式定理证明系统——分解的难解性。我们得到了以下结果：(1)在寻找分辨率证明问题上已经做了大量的工作，并且最近开发了快速算法。我们从最优化的角度来分析这个问题，即寻找最短分辨率证明的问题。我们证明了寻找长度小于S+O（n^d）的证明的问题是np困难的，其中n是变量的数量，S是最短证明的长度，d是一个任意常数。(2)讨论了求解CNF可满足性问题（SAT）的一种算法——分辨率与回溯法之间的关系。我们证明了在不增加树的大小的情况下，通过分辨率证明可以得到回溯的搜索树，反之亦然。(3)我们找到了一组CNF公式，可以通过增加冗余来减少证明的长度。设NH为将某图问题转化为sat得到的公式集，NH需要分辨率的指数长度证明。然而，如果我们在NH的公式中加入少量的子句，我们可以用多项式的步数来证明NH。在某些情况下，我们将难于组合的问题转化为sat，在这种情况下，将原始问题转化为简短的公式似乎是合理的。然而，我们的结果表明，在某些情况下，冗余起着重要的作用。

Automated theorem proving system is one of the most popular topics of AI field and has been discussed by many researchers. However, there is no perspective of making it into practical use because of the lack of fundamental analysis on it. In this research work, we discussed the intractability of Resolution, a theorem proving system of tautology. We obtained the following results :(1) A lot of effort has been done for the problem of finding Resolution proofs and fast algorithms are developed recently. We analyzed this problem in terms of optimization, i.e., the problem of finding shortest Resolution proofs. We showed that the problem of finding a proof of length less than S+O(n^d) is NP-hard, where n is the number of variables, S is the length of the shortest proof, and d is an arbitrary constant.(2) We discussed the relation between Resolution and Backtracking method, an algorithm for CNF Satisfiability problem (SAT). We showed that a search tree of Backtracking can be obtained from Resolution proof without increasing the size of the tree, and vice versa.(3) We found a set of CNF formulas such that we can reduce the length of the proof by adding redundancy. Let NH be the set of formulas obtained by translating some graph problem into SAT.NH needs exponential length of Resolution proof. However, if we add small number of clauses to formulas in NH,we can prove NH in polynomial number of steps. In some occasions, we solve hard combinatorial problems translating into SAT.In this case, it seems reasonable to translate the original problem into short formulas. However, our result shows that there are some occasions in which redundancy plays an important role.