Efficient and Scalable Theorem Proving in Propositional DynamicLogic with Converse.

Research areas

Temporary Supervisor

Professor Rajeev Gore

Description

Propositional dynamic logic with converse (CPDL) is a logic of fundamental importance in computer science. It extends propositional modal logic with regular expressions allowing us to capture sentences like "every state reachable from the current state by executing program alpha will satisfy property P". Indeed, it is expressive enough to capture the basic components of programming like conditionals, and while-loops. We have developed prototype automated theorem provers for reasoning in CPDL using the method of semantic tableaux, but they are currently not amenable to applications because they do not scale to real-world examples.

Goals

Your task is to take these prototype to the next level by finding and incorporating various optimisations to make these provers both efficient and scalable to large formulae. Example applications are to use CPDL for efficient composition of web-services so users can build specially tailored services from a given set of basic ones

Requirements

This project involves both theory and practice since you will also be required to prove formally that your optimisations are sound and terminating.

Gain

Successful completion is likely to lead to a publication.

Keywords

automated reasoning, tableaux, logic, theorem proving

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