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.
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
This project involves both theory and practice since you will also be required to prove formally that your optimisations are sound and terminating.
Successful completion is likely to lead to a publication.
automated reasoning, tableaux, logic, theorem proving