A Framework for Implementing Modal Logics Using the BDD Method

Research areas

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