Applying Decision Procedures to Synthesis Problems

将决策程序应用于综合问题

• 批准号: 2444465
• 金额: --
• 依托单位: University of Bristol
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2020
• 资助国家: 英国
• 起止时间: 2020 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2444465
• 关键词: Applying; Decision; Procedures; Synthesis; Problems

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

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