Logic and computational complexity

我研究的主要目的是了解计算机程序在解决某些重要类型问题方面的局限性。这些问题是有一定数量的条件需要满足的问题；假设给定的条件集合，很容易检查所提出的解决方案实际上是否正确，但似乎很难搜索到解决方案。这类问题的一个日常例子是由拼图游戏或解魔方的难题提供的。这些类型的问题属于NP类别。其中，最著名的是来自逻辑的可满足性问题，即命题逻辑公式是否具有满意赋值的问题。 我们的主要目标是证明这类问题，特别是可满足性问题，一般很难解决。在可满足性问题没有解的情况下，我们可以通过在逻辑系统中提供证明来证明这一点。如果我们能证明在问题复杂的某些情况下，不可满足性的证明一定是指数长的，那么这表明在最坏的情况下，问题的某些算法必须花费指数长的时间。这一点已经在最著名和最成功的可满足性算法--归纳法中得到了证明。我希望在我的研究中将这些结果扩展到更强大的逻辑系统，从而扩展到更广泛的算法类别。

The principal aim of my research is to understand the limitations of computer programs in solving certain important types of problems. These problems are ones where there are a certain number of conditions to be satisfied; assuming a given collection of conditions, it is easy to check whether or not a proposed solution is in fact correct, but it appears to be difficult to search for a solution. An everyday example of this kind of problem is provided by puzzles, such as jigsaw puzzles, or the problem of solving Rubik's Cube. These type of problems are in the category NP. Of these, the best known is the Satisfiability problem from logic, which is the problem of whether a formula of propositional logic has a satisfying assignment. The main goal is to show that such problems, and in particular the Satisfiability problem, are hard to solve in general. In the case where a satisfiability problem has no solution, we can demonstrate this by providing a proof in a logical system. If we can show that in certain cases, where the problems are complicated, that the proofs of unsatisfiability must be exponentially long, then this shows that certain algorithms for the problem must take an exponentially long time in the worst case. This has already been shown for the best known and most successful algorithm for satisfiability, the resolution method. I hope in my research to extend these results to more powerful logical systems, and hence to broader classes of algorithms.