Efficient CEGAR-tableaux for 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.
Of course, there is no such thing as a free lunch, for it is significantly harder to decide whether a non-classical formula is true or false (EXPTIME vs NP). Can we develop and implement efficient algorithms for this problem?
This problem has been attacked using multiple different methods for the past 40 years, without much success. But, in 2021, second-year student Cormac Kikkert and I showed that we could improve the existing decision procedures for these logics by orders of magnitude by combining two well-known existing methods giving rise to what we called CEGAR-tableaux [1].
Your project is to continue this work and to hopefully publish an academic paper in an international conference in 2024.
You will need excellent programming skills and a good background in maths. This project would set you up for a follow-up honours project in this area, which is exactly what Cormac is currently doing!
https://github.com/cormackikkert/CEGARBox
https://github.com/cormackikkert/CEGARBoxCPP
Rajeev Goré, Cormac Kikkert: CEGAR-Tableaux: Improved Modal Satisfiability via Modal Clause-Learning and SAT. TABLEAUX 2021: 74-91.
Rajeev Gore and Cormac Kikkert cegarboxktn : Improved decision procedures for multimodal tense description logic ALCI. (submitted to TABLEAUX 2023).
Rajeev Gore, Cormac Kikkert: Improved modal satisfiability for KD, KT, KB, K4 and K5 via CEGAR-tableaux: system description (submitted to TABLEAUX 2023).