Generating Inference Systems for Non Classical Logics

Unfortunately there is not just one logic as basis for every useful application. Moreover, typical application scenarios hardly allow to single out in advance a particular logic as the most adequate basis for formal reasoning. We are therefore urged to investigate large families of logics, and -- if possible -- define uniform calculi that facilitate the switch from one logic to another, deepening the understanding of the relations between them. Therefore, a central task of logic in computer science is to provide an automated generation of analytic calculi for a wide range of non-classical logics, i.e., calculi in which the proof search proceeds by step-wise decomposition of the formula to be proved. The most famous example of an analytic calculus is Gentzen`s sequent calculus LK for classical logic (and its variants). Cut-free "Gentzen-style`` calculi serve as a basis for automated deduction and allow the extraction of important implicit information from proofs, such as numerical bounds and programs in proof-style. Moreover, they are a key to a profound understanding of the relation between the logic`s syntax and semantics. The aim of this project is to provide tools for the automated generation of analytic calculi (with hypersequent and sequents of relations) for broad classes of logics. We intend to describe: * meta-theorem provers which allow for an automated adaption of existing theorem provers to the logics under consideration * modular cut-elimination procedures which are based on general transfer principles extending cut-elimination from subclasses of calculi to all cases * tools for proof mining, i.e., the automated extraction of implicit information from proofs such as bounds or variants of Herbrand`s disjunctions.