# A Cyclic Prover for Propositional Dynamic Logic (available)

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)  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  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 . Cyclist is a framework, written in the OCaml functional programming language , 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.

 https://en.wikipedia.org/wiki/Propositional_dynamic_logic
 Simon Docherty, Reuben N. S. Rowe: A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic. TABLEAUX 2019
 https://www.cyclist-prover.org/
 https://www.ocaml.org/