Student research opportunities

Implementing Tableaux Using BDDs

Project Code: CECS_863

This project is available at the following levels:
Honours
Please note that this project is only for undergraduate students.

Keywords:

automated reasoning, logic, theorem proving, theory, tableaux

Supervisor:

Professor Rajeev Gore

Outline:

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.

Goals of this project

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.