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 [17]. 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 [18]. 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 [2]. 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 [3]. 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, 5]. The correspondence theory of atomic and molecular logics and a characterization of displayable atomic and molecular logics has also been recently studied [6, 4]. 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]. Thus it makes sense to explore whether the methodologies developed by Goré and colleagues can be merged with the methodology developed by Aucher.

Objectives. There are two main objectives in this project, the former rather ‘applied’ and the latter more
‘theoretical'.
1. The first objective is to produce an Isabelle library for reasoning, formally, about the proof-theory, modeltheory 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 Isabelle will require a totally constructive approach which is amenable to Isabelle’s extraction facility so that we can automatically produce algorithms relevant to each (proof-theoretic, model-theoretic, or correspondence-theoretic) aspect. The sub-objectives are therefore the following.

   (a) Formalize in Isabelle the syntax and semantics of atomic (and molecular) logic.
   (b) Encode the computation of a sound and complete display calculus for any basic atomic logic using
the formalization in Isabelle of the previous item. This computation is based on the one formally
defined and presented in [1, 5].

   (c) Formalize in Isabelle the correspondence algorithms introduced in [6, 4]. 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 [8, 11].
2. The second objective is to develop the theory of atomic and molecular logics. There are two main subobjectives that we plan to consider.
   (a) The first sub-objective deals with the correspondence theory of atomic and molecular logics. At the moment, the correspondence theory from axioms and inference rules to semantic first-order conditions has been very much studied [5, 6, 4], but the other direction needs to be developed as well since it is often quite relevant in practical applications of logic. This second direction, from semantics to proof systems, has been the object of study of some works in modal (polyadic) logics [16, 7, 15].

   (b) The second sub-objective deals with the integration in the framework of atomic and molecular logics of more expressive non-classical logics with fixed-points such as PDL or the μ-calculus. These logics can be seen as fragments of second-order logics [13, 14]. So, we will need to develop a second-order version of atomic and molecular logics in which the truth conditions of connectives are not expressed by first-order formulas but by second-order formulas. Yet, the overall methodology should be the same as in the first-order case and should lead to a similar kind of ‘second-order’ atomic logics.

Practicalities. The student will be based mainly in Rennes, but with regular travel(s) to Australia every year, for example to attend the ANU logic summer school. Regular online meetings will be organized with the supervisors. A cotutorship should be arranged between France and Australia.