# A Framework for Implementing Modal Logics Using the BDD Method

## Research areas

## Temporary Supervisor

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

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