Starting Date: June 2022
Prerequisites: Interest in formal logic; knowledge of OCaml, or another functional programming language, or the ability and willingness to learn.
Will results be assigned to University: No
Propositional Dynamic Logic (PDL) [1] is a logic in which abstract properties about the behaviour of programs can be expressed, in a very general way. Because of its generality it is suitable for checking the behaviour or a wide range of programs and systems, via model checking.
PDL is what is known as a modal logic, meaning that logical formulas are subject to modalities that, in this context, describe the actions of programs. If a modality is applied to a formula, the intended meaning is that the property expressed by the formula will hold after the action of some program (indicated by the modality) is performed.
For example, the formula (x > 4) ⟶ [x++](x > 5) expresses the simple fact that, if the variable x holds a value greater than 4, then after executing the code x++ incrementing the variable, it will hold a value greater than 5.
Although algorithms already exist for deciding the validity of statements in PDL, recent research [2] has developed a cyclic proof system for PDL that can also be used as the basis for deciding validity, through a process of proof search. The aim of this project would be to implement the proof system within the Cyclist automatic theorem proving framework [3]. Cyclist is a framework, written in the OCaml functional programming language [4], for generating automatic provers from a definition of a cyclic proof system.
Once the cyclic prover is produced for PDL, we would then test it against implementations of the existing algorithms.
[1] https://en.wikipedia.org/wiki/Propositional_dynamic_logic
[2] Simon Docherty, Reuben N. S. Rowe: A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic. TABLEAUX 2019
[3] https://www.cyclist-prover.org/
[4] https://www.ocaml.org/