Applying Decision Procedures to 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