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 provers and algorithms (e.g. pdlProver [5] and MLProver [6]). A survey of existing provers is available from 2010 [7].
References
[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/
[5] Pietro Abate, Rajeev Goré, Florian Widmann. An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability. Electronic Notes in Theoretical Computer Science, Volume 231, 2009, Pages 191-209, ISSN 1571-0661, https://doi.org/10.1016/j.entcs.2009.02.036
[6] Oliver Friedmann, Martin Lange. A Solver for Modal Fixpoint Logics. Electronic Notes in Theoretical Computer Science, Volume 262, 2010, Pages 99-111, ISSN 1571-0661, https://doi.org/10.1016/j.entcs.2010.04.008
[7] Hustadt, U., Schmidt, R. A. A Comparison of Solvers for Propositional Dynamic Logic. In Konev, B., Schmidt, R. A., & Schulz, S., editors, Proceedings of the Workshop on Practical Aspect of Automated Reasoning (PAAR-2010), 2010. https://doi.org/10.29007/63hq