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.