Seminar Computer Science - Dr. R. Ramanayake

Title: Logics and Proof Systems in Computer Science

Abstract:
Logic---the study of reasoning---plays a crucial role in computer science as a foundational framework and a powerful modelling tool. Classical logic is the most well-known logic and familiar from its truth tables. However it is not suitable in most situations. Indeed, the diversity of applications (verifying software correctness, artificial intelligence, database queries, computational linguistics, to name just a few) calls for a deep understanding of a vast number of very different reasoning systems (logics), with new logics appearing all the time. My research vision is to establish results and powerful techniques that apply to large classes of logics (rather than just a single logic).

I first present the main themes of my research. One of the most prominent ways to study a logic is via proof theory i.e. using a mathematical object called a proof system which generates exactly the valid statements of the logic. A proof system can be used to establish theoretical properties of the logic, and for automated reasoning. I will discuss some of the computational and logical properties I seek. For this approach to succeed, the proof system must be sufficiently 'well-behaved'. Historically this has led to the development of various exotic types of proof systems. I will talk about an alternative and unifying approach using the sequent calculus (the most well-studied type of proof system) that parametrises the notion of well-behaved. I will
also discuss my implementation goals: computer-verified proofs and automated theorem provers.

Next I present some of my most recent research results which combine proof theory, order theory, and combinatorics to establish the decidability of the decision problem for infinitely many logics, extending a famous result of Kripke from 1959 for relevant logic.