Investigations of proof theory and automated reasoning for non-classical logics

This thesis presents some new results in structural proof theory for modal, intuitionistic, and intuitionistic modal logics. The first part introduces three original Gentzen-style natural deduction calculi for, respectively, intuitionistic verification-based epistemic states -- namely, belief and knowledge operators -- and intuitionistic strong L\"ob logic for arithmetical provability. For each of these calculi strong normalisation results are proven w.r.t. several systems of proof rewritings, which are considered on the basis of their structural relevance, e.g.\ for establishing the related subformula principles, or for providing a categorical semantics of normal deductions. The presentation of new and original sequent calculi for a wide family of interpretability logics closes this first part of the thesis. These sequent systems are modularly designed by recurring to internalisation techniques which make possible their fine grained structural analysis, this way establishing both their semantic and structural completeness. The second part has a more applicative nature. It presents first an implementation in the HOL Light proof assistant of an internal theorem prover and countermodel constructor for G\"odel-L\"ob logic, relying on a previous computerised proof of modal completeness for that logic within the same formal environment. The design of that proof search algorithm is surveyed, and examples of both its interactive and automated use are shown. An overview of an ongoing automation-oriented implementation in UniMath of the basics of univalent universal algebra closes this second part of the thesis. The coding style and methodology used are discussed besides some concrete formalisation examples of algebraic structures. Finally, two appendices describe the logical engine underlying each of the proof assistants that are used for the results presented in the second part, namely classical higher order logic for HOL Light, and univalent type theory for UniMath.