Formally Verified Automated Reasoning in Non-Classical Logics

Classical propositional logic (CPL) captures our basic understanding of the linguistic connectives “and”, “or” and “not”. It also provides a very good basis for digital circuits. But it does not account for more sophisticated linguistic notions such as “always”, “possibly”, “believed” or “knows”. Philosophers therefore invented many different non-classical logics which extend CPL with further operators for these notions.

Over the past fifty years, such non-classical logics have proved vital in computer science and logic-based artificial
intelligence: after all, any intelligent agent must be able to reason with more than just and-gates, not-gates and or-gates! For example, we now have non-classical logics which capture notions such as “phi is true until psi becomes true”; “if we execute atomic program alpha in state x then we end up in a state y which obeys formula psi”, and many more.

The most common way to determine the true or false status of a given formula is to use the tableau method [1]. We have developed and implemented such methods for a plethora of non-classical logics [2]. But how can we guarantee that the implementation is faithful to the theory? Indeed, how can we be sure that we have not made a mistake in the theory?

Over the past twenty years, we have shown that we can encode the theory of the tableau method into an interactive proof-assistant, such as Coq [3]. The proof-assistant checks all of the claims we make about our tableau rules. We then interact with the proof-assistant to prove the following claim: for all formulae phi, it is possible to decide whether phi is true or false in the given non-classical logic.

The proof of the claim contains an algorithm for deciding whether an arbitrary formula is true or else false! This proof can then be exported automatically to produce a formally verified computer program that implements the decision procedure [4].

Your project is to continue this work and to hopefully publish an academic paper in an international conference.

You will need a strong background in maths but no programming skills in languages such as C++. You will need to read and understand the previous work, and then learn to program in Coq. The research is to extend the existing work to new logics.

[1] Rajeev Gore: Tableaux Methods for Modal and Temporal Logics. Handbook of Tableau Methods, Kluwer, 1999.

[2] Rajeev Gore, Florian Widmann: Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse. IJCAR 2010:
225-239.

[3] Jeremy E. Dawson, Rajeev Gore: Generic Methods for Formalising Sequent Calculi Applied to Provability Logic. LPAR 2010:
263-277.

[4] Minchao Wu, Rajeev Gore: Verified Decision Procedures for Modal Logics. International Conference on Interactive Theorem
Proving 2019: 31:1-31:19.