Modal logics extend classical propositional logic by adding a unary connective  with A interpreted as any of the following: "A is known", "A is believed", "A is necessary". The models for modal logics are graphs
The project is to build a framework which accepts an arbitrary collection of restrictions on R and which outputs a theorem prover specially designed for the modal logic captured by those restrictions.
It will involve significant amounts of programming using BDDs and will suit someone who enjoys both theory and practice.
BDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics. Rajeev GorÃ©, Jimmy Thomson Proc. IJCAR 2012: International Joint Conference on Automated Reasoning 2012. Lecture Notes in Computer Science, volume 7364, pp 301-315, Springer 2012
Successful completion is likely to lead to a publication.
modal logic, theorem proving, logic, automated reasoning