Student research opportunities

A Framework for Implementing Modal Logics Using the BDD Method

Project Code: CECS_864

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

Keywords:

modal logic, theorem proving, logic, automated reasoning

Supervisor:

Professor Rajeev Gore

Outline:

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 where W is a set of points/vertices/states and R is
a set of edges connecting these points/vertices/states. By stipulating
further restrictions on these edges, we can obtain many different
propositional modal logics which greatly extend the expressive power
of classical propositional logic. For example:

R is reflexive: forall x. R(x,x)
R is serial: forall x exists y such that R(x,y)
R is transitive: for all x,y,z. R(x,y) and R(y,z) implies R(x,z)
R is euclidean: for all x,y,z. R(x,y) and R(x,z) implies R(y,z)
R is symmetric: for all x,y. R(x,y) implies R(y,x).

In almost all of these logics, the models for a formula A can be built
from the subsets of the set subfml(A) of all subformulae of A,
ignoring all other formulae which are not relevant to A. A simple way
to test if a given formula A has any models is then to just enumerate
these subsets and check if any of them can support a model for A.

This naive method has an average and best case complexity which is
exponential in the size of A since a formula of length n has at most n
subformulae and the size of subfml(A) is then 2^n. Recently, it has
been shown that this method can be made practical by using binary
decision diagrams (BDDs) as the underlying data structure.

Goals of this project

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.

Requirements/Prerequisites

It will involve significant amounts of programming using BDDs and will
suit someone who enjoys both theory and practice.

Student Gain

Successful
completion is likely to lead to a publication.

Background Literature

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

Contact: