# A Framework for Implementing Modal Logics Using the BDD Method

## Temporary Supervisor

Professor Rajeev Gore

## Description

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

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

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

## 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

## Gain

Successful completion is likely to lead to a publication.

## Keywords

modal logic, theorem proving, logic, automated reasoning

Updated:  1 June 2019/Responsible Officer:  Dean, CECS/Page Contact:  CECS Marketing