There are several opportunities for PhD research in this group, supervised by Roy Dyckhoff. Some suggestions are below, although other possible research areas are available. Some of the research could be collaborative with other researchers at St Andrews or (less formally) elsewhere. Other suggestions from Ian Gent are similar.
See for details of PhD studentships at St Andrews University.
The currently proposed projects are all in the general area
of computational logic, especially proof theory, as follows:
Students with a pure mathematical background and/or expertise in logic are especially welcome.
Details of most publications can be found at http://www-theory.dcs.st-and.ac.uk/~rd/publications.
See also the Proceedings of Tableaux 2000 (ed. R.Dyckhoff) , Springer-Verlag
Lecture Notes in Artificial Intelligence 1847 (2000).
Many logics, especially non-classical logics of the kind arising in computer science and artificial intelligence, can be expressed in terms of tableaux systems or sequent calculi: these may be regarded as inductive definitions of a provability property of formulae and expressed very succinctly in Prolog-like languages as logic programs (and thus "executed"). Such programs are usually inefficient, or (even worse) non-terminating; however, other more efficient calculi (e.g.[1]) can often be developed that express the same logic.But they are usually far more complex, and it is hard to check the correctness of the transformations that lead from the first to the second:in other words, that the new calculus is both sound and complete with respect to the old one. The purpose of this project is to develop tools for semi-automatically making such checks, perhaps even in the more general case of pure logic programs.
For (primitive recursive) functions on the natural numbers, several important complexity classes can be captured by syntactic restrictions, e.g.on the use of multiplication. The purpose of this project is to explore the application of such ideas to other inductively defined types, such as the type of (finite) lists, and co-inductively defined types, such as that of arbitrary lists.
[1] A new recursion theoretic characterisation of the polytime functions, S. Bellantoni & S. Cook, Computational Complexity 2 (1992).
How do we know our programs are correct? One answer is to use the beautiful link between proofs and programs to derive correct programs. Indeed, it is even possible to extract programs automatically from proofs, and this has been made much more practicable by recent work by Jim Caldwell. Using this, we have been able to extract a correct program for the important search algorithm Conflict Directed Backjumping for problems like satisfiability and Hamiltonian circuit. We propose to extend this research to further algorithms and, especially, more complex problems such as Intuitionistic Propositional Logic and QSAT.
Search Algorithms in Type Theory
James Caldwell,
Ian Gent, and Judith
Underwood. Theoretical
Computer Science, Vol. 232, No. 1-2, pp.55-90, February 2000.
A draft copy dated May 1998 is available here.
One of the most fruitful ideas in logic has been the correspondence between proofs and programs, observed by Curry, Howard and others, with a similar correspondence between logical formulae and type systems for programming languages. Dependent type theory (of Martin-Löf) is an example of a strong type system in this line of development. Some of the basic ideas have been taken further [1], in the area of natural language semantics. The purpose of this project is to push this development even further, with
- automation of the search for proofs (i.e.parsing or making sense of lists of words as sentences)
- resolution of standard linguistic problems, regarded as fatal to older (non-dependent) type-theoretic approaches.
Ideas on proof search in dependent type theory from [2] would probably be exploited.
Fuzzy logics allow one to categorise propositions as "partially true", e.g.true with degree a,where a is a real number in the range [0,1]. Such categorisation is of importance in the modelling of the real world, e.g.in expert systems and deductive databases. Techniques are recently developed [1,2] for solving decision problems in such logics, i.e.for efficiently deciding whether formulae are valid.The purpose of this project is to extend such techniques to a wider range of fuzzy logic, with implementations and experimentation (and comparison with different approaches by others).
Sequent calculi are often used for expressing provability properties, and a common problem in the meta-theory of such calculi is to show the admissibility of important inference rules, such as Gentzen's CUT rule, in calculi without such rules. Typically, such problems are solved by simple induction on countable ordinals. More generally, relationships between calculi are of interest. The purpose of this project is to develop tools, e.g.in the system Coq, for solving such problems semi-automatically.
The usual rule of beta-reduction in the lambda calculus can be decomposed into a reduction step and several substitution steps, performed explicitly and interleavable with reduction steps. In [1] we show the strong normalisation of an interesting calculus, based on proof theory, of rules of this form; further work is needed to develop the theory for logical connectives beyond implication, to develop and evaluate strategies for reduction using a system such as STRATEGO, and to develop correctness proofs for a first-order version using Urban's work on nominal logic.