Towards a Generic Theorem Prover for Non-Classical Logics

Context. A wide variety of non–classical logics have been introduced over the past decades : modal logics, substructural logics, linear logics, Lambek calculi,... This diversity is an asset : each logic has an interest for a specific purpose, and one can pick and resort to some of them for reasoning about a given applicative issue [14]. The main reason why practitioners turn to non-classical logics instead of classical logic is that these logics often remain decidable while providing sufficient expressive power [15]. However, from a theoretical and formal point of view, non–classical logics are still disorganized and scattered and somehow miss a common formal ground. In response to that situation, the framework of atomic and molecular logics provides a uniform and generic way to explore and study non–classical logics. Atomic and molecular logics were introduced by Guillaume Aucher and can be (somehow) seen as normal forms for logics [5]. One can define and compute automatically notions of bisimulations for any atomic and molecular logic and the model theory of non-classical logics can be developed in a systematic way [6]. Likewise, they allow us to develop in a systematic and uniform way the proof theory of non–classical logics. Indeed, one can automatically compute a display calculus for any (basic) atomic logic [1, 4]. The correspondence theory of atomic and molecular logics and a characterization of displayable atomic and molecular logics has also been recently studied [3, 2]. Given the systematic aspect of this overall approach, it is natural to ask for some sort of machine-checked formalisation and automation. With colleagues, Rajeev Goré has developed Coq and Isabelle formalisations of many non-classical logics in a uniform way, usually concentrating on their sequent calculi [12, 10, 9, 8, 13]. Thus it makes sense to explore whether the methodologies developed by Gore and colleagues can be merged with the methodology developed by Aucher.

Objectives. The main objective of this project is to produce a Coq library for reasoning, formally, about the proof-theory, model-theory and correspondence-theory of this plethora of non-classical logics in a uniform way via the framework of atomic and molecular logics. Much of this theory has already been worked out on pen-and-paper, but encoding it in Coq will require a totally constructive approach which is amenable to Coq’s extraction facility so that we can automatically produce algorithms relevant to each (proof-theoretic, model-theoretic, or correspondence-theoretic) aspect. This can be achieved if the following sub-objectives are also addressed during the PhD, some possibly in parallel with others. In the first stage of the PhD, we will start by considering only atomic logics, not molecular logics.

1. Formalize in Coq the syntax and semantics of atomic (and molecular) logic.

2. Encode the computation of a sound and complete display calculus for any basic atomic logic using the formalization in Coq of the previous item. This computation is formally defined and presented in [1].

3. Formalize in Coq the correspondence algorithms introduced in [3, 2]. Since these algorithms are based on those proposed for modal polyadic logics, maybe resort to some implementations of correspondence algorithms for modal logics, such as SQEMA [7, 11].

4. Encode the computation of an appropriate notion of bisimulation for any atomic (and molecular) logic. This computation is formally defined and presented in [6].

Practicalities. The student is supposed to stay most of the time in Rennes in France but with some regular travel(s) to Australia every year, for example to attend the ANU logic summer school. Regular online meetings will be organized with both supervisors and the student.