TICAMORE: Translating and discovering calculi for modal and related logics

Many logics in addition to classical, boolean logic have been applied successfully in diverse areas of computer science, philosophy, epistemology and artificial intelligence. These logics are used, for instance, to express different modes of truth (modal logics), to capture hypothetical and plausible reasoning (conditional logics), reason about knowledge (epistemic logics), obligations and prohibitions (deontic logics), separation and sharing of resources (bunched implications logics) and to model the properties of various systems. Moreover, the widespread use of logical methods in these fields has in turn lead to an explosion of new logics to (study and) apply. Our investigation will focus on the proof theory of logics that are variants and generalizations of modal logics (inclusive of the logics listed above), and in particular, on formal proof systems with the analyticity property. Indeed, having an analytic calculus for the logic of interest is crucial for investigating the logical properties and is the key to developing automated reasoning methods. There are two types of proof systems: internal calculi (e.g. Gentzen sequent calculus) where every basic object of the calculus can be read as a formula of the logic, and external calculi (e.g. labelled and display calculi) where the basic objects are formulas belonging to a more expressive language capable of encoding the semantics (meaning) of the logic. Internal and external calculi have vastly different properties. For instance it is easier to use internal calculi to establish logical properties such as decidability and interpolation whereas the external calculi are easier to construct and analyticity is easier to prove. The TICAMORE project will clarify the relationship between these two fundamental and historically distinct approaches to proof systems, 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. An integrated and systematic study of internal and external calculi has not been carried out in the 30 years of research in this area. Our study will enable the transfer of properties between different calculi, facilitate their implementation and lead to the discovery of internal calculi for logics that do not yet enjoy them. The new calculi will be an important tool to aid the solution of important open problems in the formalized logics including interpolation, decidability and conservativity. 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.

Logic offers precision and trust and it is therefore at the base of applications in many areas, ranging from Philosophy to Artificial Intelligence (AI). Proof theory is a central field of logic, which nowadays is used to enable computers to automatically generate proofs. Classical logic, dealing with objects that can only be either true or false, is not adequate as the base of all of possible applications. Indeed, different applications often call for logics more expressive than classical logic. This project focused on the proof theory of useful families of logics allowing finer distinctions and a direct representation of notions that cannot be well expressed in classical logic. These logics are variants and generalizations of modal logics which are used to express different modes of truth, and to study different types of reasoning, like reasoning about obligations and prohibitions (central, for instance, in legal reasoning) or about knowledge or hypothetical and plausible reasoning, and reasoning about computer programs. Apart from formalizing and analyzing reasoning, the considered logics are used also to describe systems (for instance AI agents) with mathematical precision and to prove properties about them, thus ensuring their correct behaviour. A prerequisite for applying a logic to solve concrete problems is the availability of an algorithmic presentation for the logic, i.e., a proof system. Several types of proof systems (calculi) have been proposed for modal and related logics falling into two categories: internal calculi, whose basic objects can be read as formulas of the logic, and external calculi, whose basic objects are formulas of a more expressive language which partially encode the logic's semantics. Internal and external calculi possess different properties and have their strengths and weaknesses. For instance external calculi are easier to define but harder to handle. Internal and external calculi have been introduced as two independent, occasionally opposing, streams in proof theory with varying degrees of success. For certain classes of modal and related logics however no calculi whatsoever are known. In the TICAMORE project we performed an integrated and systematic study of internal and external calculi for modal and related logics. We investigated the relationships between the two types of calculi, and transferred results between them. We also provided first calculi for important classes of logics and new tools to tackle and solve important open mathematical problems about the formalized logics (decidability, complexity, interpolation...). Furthermore we provided computer programs that implemented some of the calculi introduced for the class of considered logics, thus facilitating their use in applications.