Modular construction of cut-free calculi for paraconsistent logics

In this talk we focus on the problem of automatization of paraconsistent reasoning. We describe a general method for a systematic generation of cut-free calculi for thousands of paraconsistent logics known as Logics of Formal (In)consistency (LFIs). The method relies on nondeterministic semantics for these logics, and produces in a modular way uniform Gentzen-type rules, corresponding to a variety of schemata considered in the literature of LFIs.
(Joint work with Arnon Avron and Beata Konikowska).