The method of semantic tableaux has been used extensively in computer science to automate reasoning in many modal and description logics. In many applications, there is a need for provers to handle larger and larger problem sizes, so there is a need to find good data structures which allow such scaling. Binary Decision Diagrams (BDDs) have been used as data-structures by the model checking community to produce spectacularly efficient model checkers. Question: can we use BDDs to implement efficient tableaux provers ? This project will suit someone who has good maths skills but who truly enjoys programming at a high level.
The project will require you to implement tableaux provers for some basic normal modal logics using BDDs as the underlying data structure. We know that this can be done in principle, you have to do it in practice. This is not just a hacking project because you will have to make many design decisions along the way, and the main part of the project will be to find a methodology which leads to efficient provers. It may even turn out that the answer to the question above is "no", but this is fine as long as a sensible approach has been taken to reach this conclusion.
You will need to learn about tableaux for automated reasoning, and will have to learn how to use the BDD package Buddy.
If you are successful then it may lead to a paper in an international conference.
automated reasoning, logic, theorem proving, theory, tableaux