Much current research in Artificial Intelligence currently utilises non-classical logics called modal logics. These logics can capture notions like time, space, obligation, knowledge, belief etc. which classical logic cannot do as easily. But the interests of AI researchers rarely looks at the task of actually building efficient reasoners for such logics. We have recently developed automated theorem provers for very expressive modal logics. Are they any good for AI research ?
The goal of the project is to build more specialised automated reasoners for logics with applications in Artificial Intelligence. We have a framework, we need help to tailor it to the needs of AI.
A strong background in maths or logic would be extremely useful but is not necessary. Of more importance is enthusiasm and an interest in the formal side of AI. You will need to learn the theory of modal logics and how to automated them. Then you will need to learn the uses of these logics in AI. Finally, you will need to use our technology to build the provers that are needed by AI researchers.
This project will introduce you to an area of theoretical computer science which mixes theory and practice and may lead to a publication. It will form a good basis for doing a Phd, either with us, or at another university.