Applying Decision Procedures to Synthesis Problems

在理论计算机科学中，逻辑公式被用来形式化地说明和编码问题。不同的问题和公式可以用不同的逻辑来描述，例如用于计算机程序形式化验证的线性时间逻辑或用于编程语言语义的类型理论。我们将关注高阶逻辑，比如二阶逻辑。我们将研究二阶逻辑的可判定片段。二阶逻辑可以编码重要的决策问题，如程序综合，但通常被认为是不可确定的。相反，我们将识别可判定的二阶逻辑片段。对于给定的片段，我们将确定它可以成功编码的问题类型，无论是在特定领域还是在问题本身的限制下。然后我们将针对这些问题设计决策算法，并分析这些算法的计算复杂度。这将使我们能够比较不同的综合问题的相对硬度，这些问题可以通过特定的算法来解决，而这些算法不能全面地决定程序综合的一般问题。这属于EPSRC的研究领域：逻辑学与组合学、程序设计语言、理论计算机科学和软件工程

Logical formulae are used in theoretical computer science in order to formally specify and encode problems. Different problems and formulae may be described by different logics, such as linear temporal logic for formal verification of computer programs or type theories for programming language semantics. We will focus on higher-order logics, for example second order logic. We will investigate decidable fragments of second order logic. Second order logic can encode important decision problems, such as program synthesis, however in general is considered undecidable. Instead, we shall identify fragments of second order logic that are decidable. For a given fragment we shall determine the types of problem which it can successfully encode, either in specific domains or with restrictions on the problems themselves. Then we shall design decision algorithms for these problems and analyse the computational complexity of such algorithms. This will allow us to compare relative hardness of different synthesis problems which may be solvable through specific algorithms which cannot overall decide the general problem of program synthesis. This falls under the EPSRC Research areas Logic and Combinatorics, Programming Languages, Theoretical Computer Science, and Software Engineering