Student research opportunities
Efficient and Scalable Theorem Proving in Propositional Dynamic Logic with Converse.
Project Code: CECS_866
This project is available at the following levels:
Honours
Please note that this project is only for undergraduate students.
Keywords:
automated reasoning, tableaux, logic, theorem proving
Supervisor:
Professor Rajeev GoreOutline:
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 of this project
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/Prerequisites
This project involves both theory and practice since you will also be
required to prove formally that your optimisations are sound and
terminating.
Student Gain
Successful completion is likely to lead to a
publication.
