PhD STUDENTSHIPS IN
AI Research, Logic and Computation
Dr Alexander Bolotov
LOGIC provides the foundational framework for representing, analysing and implementing a wide range of computational systems in computer science and artificial intelligence. COMPUTATIONAL aspects concern with making logics amenable to proof or direct execution so that they become extremely useful as high-level abstractions of the original systems. While the range of possible logics is huge, non-classical logics, in particular, modal and temporal logics, are of a specific interest as they provide a high-level specification language for a variety of computational entities. These logics apply to such areas of AI and computer science as software and hardware specification, concurrent, dynamic and distributed systems, allowing also to represent reasoning, autonomy and learning components. The latter makes them relevant in such areas of AI as neural nets and agent technology. On the other hand, theorem-proving in logic serves as a basis for the verification of these high-level specifications, which makes research in efficient verification methods highly valuable.
Areas of research
The prospective research is thought as logic engineering in the framework of non-classical logic (modal and temporal) that matches our abstract intuition concerning complex computational systems. The two computational aspects of logic that are supposed to be analyzed are theorem-proving and direct execution. In particular, the research can be undertaken in the following areas:
(a) Efficient proof techniques for branching-time temporal logics and fixpoint logics
(b) Analysis of natural deduction based systems:
(b.1) Development of the natural deduction system for temporal logic.
(b.2) Proof search strategies in natural deduction for classical first order logic.
(c) Application of formal tools to the modelling of GRID systems
(d) Logical foundations of agent based systems
I am currently applying for funding to support PhD research. Contact me for details.