Formally Verified Automated Reasoning in Non-Classical Logics

Picture of Rajeev Goré Rajeev Goré

7 Jul 2023

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. 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.

You are on Aboriginal land.

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

arrow-left bars search times arrow-up