Formally Verified Automated Reasoning in Non-Classical Logics
rajeev.gore@anu.edu.au
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. You will not need any programming skills at all!
[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 (Yogyakarta) 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.