Translating and dIscovering CAlculi for MOdal and RElated logics – TICAMORE

The nature of the project is basic theoretical research and it takes advantage of fundamental concepts and techniques of proof-theory, namely:
- cut admissibility/elimination: a central property of a proof system, necessary for ensuring its analyticity, in itself an essential condition for obtaining computational properties (termination of proof search), countermodel generation and metalogical properties (e.g. interpolation).

- semantical analysis of a logic: it is necessary to define labelled calculi, importing the semantics into the syntax in a controlled way. The so-obtained calculi can then be possibly transformed into internal (structured) calculi by proof-normalisation and transformation.

- computational analysis of proof-systems in order to achieve termination and complexity bounds: the analysis is based on one hand on the control of proof-search, redundancy checking, and loop-checking; on the other hand on standard proof-theoretical properties, such as the invertibility of rules.

- Proof-transformation techniques: based on permutability and admissibility of rules in order to obtain a meaningful normal form enjoying special properties.

- Implementation of Calculi: in the form of theorem provers incorporating automated proof search. Particularly suitable is the LEAN methodology of Prolog implementation giving rise to very compact implementations of calculi. An alternative is to use proof-assistant tools which allow to check proofs and build them interactively.

The research has developed along the three main axes of the projet:

EMBEDDINGS BETWEEN INTERNAL AND EXTERNAL CALCULI
We have provided constructive translations between calculi for the main logics studied in the project: conditional logics, BI logics, and tense logic.

OBTAINING NEW INTERNAL CALCULI FROM EXISTING CALCULI AND APPLICATIONS
We have studied new internal calculi for some families of logics, basing on pre-existing external calculi or from a semantical specification :
- Modal and conditional logics : we have proposed first internal calculi for complex Conditional logics and new labelled calculi and semantic for non-normal modal logics.
- BI and substructural logics : we have proposed a new labelled sequent calculus for multiplicative intuitionistic linear logic and the first tableaux calculus for Public Announcement Separation Logic, as well as new calculi based on bunched hypersequent that allows to define new logics in the vicinity of Boolean BI.
- Intermediate logics : we have defined the first natural deduction systems for a large class of intermediate logics by an embeddings between hypersequents and systems of rules of second level.

Application of proof theoretic techniques to (open) problems, among the results :
- We have proved that Gödel logic enjoys the Lyndon interpolation property, a long standing open problem.
- Decidability through proof-search : we have proposed a constructive approach via redundancy-free proof-search, the method, mechanized in axiom-free Coq, provides a decision procedure for Implicational Relevance Logic.

VALIDATION BY AUTOMATED REASONING TOOLS
- The theorem prover VINTE implementing calculi for Countefactual Logic V and its extensions, the first theorem prover for these logics.
- The theorem prover iiProve, the first theorem prover for intermediate logics using nested sequents.

The research will continue along the three axes of the project, building on the results obtained so far:

EMBEDDINGS BETWEEN INTERNAL AND EXTERNAL CALCULI
we shall study translations of hypersequent and nested calculi to sequent calculi: the hope is to obtain a new classification of these logics based on the required restrictions for translation and, conversely negative expressivity results for sequent calculi. Moreover we intend to study translations between existing internal calculi and our new labelled calculi for non-normal modal logics. aiming to define new internal calculi semantically grounded.

OBTAINING NEW INTERNAL CALCULI FROM EXISTING CALCULI AND APPLICATIONS
We intend to study how to derive internal calculi for modal and epistemic extensions of the BI and BBI logics from our external labelled calculi and how to use them to study decidability of fragments. Moreover we intend to study how to obtain internal calculi from the display calculi for intermediate and substructural logics by investigating the residuation-invariant form of these calculi.

VALIDATION BY AUTOMATED REASONING TOOLS
We intend to implement a prover based on the labelled tableau calculus for BI and BBI logics, allowing countermodel generation. We also intend to implement our labelled calculi for non-normal modal logics, it will be the first existing one for these logics. Finally we intend to develop an automated translation from the internal to the labelled calculi for Lewis conditional logics.

Partial list :
M. Girlando, B. Lellmann, N. Olivetti, and G.L. Pozzato. Hypersequent Calculi for Lewis Conditional Logics with Uniformity and Reflexivity. Proc. TABLEAUX 2017.

 M. Girlando, B. Lellmann, N. Olivetti, G.L. Pozzato, and Q. Vitalis. VINTE: an Implementation of Internal Calculi for Lewis Logics of Counterfactual Reasoning. Proc. TABLEAUX 2017.

A. Ciabattoni and F. Genco. Hypersequents and Systems of Rules: Embeddings and Applications. ACM Transaction on Computational Logic 19(2), Article 11 (2018).

J-R. Courtault and H. van Ditmarsch and D. Galmiche. A Public Announcement Separation Logic. Proc. MSCS, 2017.

A. Ciabattoni, T. Lyon, and R. Ramanayake. From Display to Labelled Proofs for Tense Logics. Proc. LFCS 2018.

 A. Ciabattoni and R. Ramanayake. Bunched Hypersequent Calculi for Distributive Substructural Logics. Proc. LPAR 2017.

 T. Dalmonte, N. Olivetti, and S. Negri. Non-normal modal logics: bi-neighbourhood semantics and its labelled calculi. Proc. AIML 2018.

D. Galmiche and M. Marti and D. Méry. Proof Translations in BI Logic -extended abstract. 1st Int. Workshop EICNCL 2018, Oxford, UK, July 2018.

D. Galmiche and D.Méry. Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic. 3rd Int. Workshop ARQNL 2018, Oxford, UK, July 2018.

 M. Girlando, S. Negri, and N. Olivetti. Counterfactual logic: labelled and internal calculi, two sides of the same coin? Proceedings AIML 2018.

R. Kuznets and B. Lellmann. Interpolation for Intermediate Logics via Hyper- and Linear Nested Sequents. Proc. of AIML 2018.

D. Larchey-Wendling. Constructive Decision via Redundancy-free Proof-Search. Proc. IJCAR 2018.

M. Marti and Th. Studer. The internalized Disjunction Property for Intuitionistic Justification Logic. Proc. AIML 2018

L. Santocanale. The equational theory of the natural join and inner union is decidable. Proc. FOSSACS 2018.

The fruitful application of logical methods in several areas of computer science, epistemology and artificial intelligence has resulted in an explosion of new logics. These logics are more expressive than classical logic, allowing finer distinctions and a direct representation of notions that do not find a natural place in classical logic. Logics are used to express different modes of truth (modal logics) and other types of reasoning including hypothetical and plausible reasoning (conditional logics), reasoning about knowledge (epistemic logics), and separation and sharing of resources (bunched implications logics). In addition to formalizing reasoning in this way, logics are also used to model various systems and to prove properties about them leading to applications in checking correctness and safe behaviour. In this project we consider those logics that are variants and generalizations of modal logics (inclusive of all the logics listed above) and characterized by variants of Kripke semantics; they find applications specifically in the areas of formal verification, epistemology and knowledge representation. Our investigation will focus on the proof-theory of these logics. Proof-theory provides a constructive approach to investigating fundamental meta-logical and computational properties of a logic through the design and the study of calculi (formal proof systems) with suitable properties (analyticity). Analytic calculi are also the base for developing practical reasoning tools such as theorem provers and proof assistants.

In the literature of the last 30 years, several formal proof systems, generalizing the original sequent calculi by Gentzen, have been proposed to provide analytic calculi for modal and related logics; among them hypersequent calculi, labelled calculi and display calculi. The proof systems we study here fall into two categories: internal calculi, in which every basic object of the calculus can be read as a formula of the language of the logic, and external calculi
where the basic objects are formulas of a more expressive language which partially encode the semantics (meaning) of the logic. The success of this investigation is varied: for some important classes of logics, no internal calculi are known, for others no terminating or optimal external calculi are known. The internal and external calculi reflect the two different ways of presenting a logic: syntactically and semantically. Both presentations are useful: they exhibit distinct properties and reveal different facets of the logic. The relationships between internal and external calculi are largely unexplored and their investigation is our main objective. We intend to systematically study the relationships between internal and external calculi with the aim of transferring the advantages from one type of
calculi into the other. We think that such a study will shed light on the relationship between provability in syntactic and semantic-based calculi, enable the transfer of proof-theoretic properties between different calculi and lead to the discovery of internal calculi for logics that do not yet enjoy them. These new internal calculi will be helpful for the solution of several important theoretical problems including interpolation and conservativity. Indeed, the question of decidability is also still open for many logics and a main obstacle is the lack of an analytic internal calculus.

The TICAMORE project will clarify the relationship between the two fundamental and historically distinct approaches, thus promoting the unification and cross-fertilization of new ideas between practitioners in the two communities, leading to new insights into the proof-theory of modal and related logics. Finally the project will contribute to the development of new automated reasoning tools to be applied in knowledge representation and in the formal verification of system properties.