From Input/Output Logics to Conditional Logics via Sequents - with Provers.

We consider cut-free sequent calculi for a number of deontic logics from the family of Input/Output logics. These sequent calculi provide a correspondence to the flat fragment of certain conditional logics. Two of the introduced calculi are non-standard in that they include non-derivability statements, and hence are interesting also from a purely technical perspective. We further modularise the calculi in an extended sequent framework. Proof search in the extended calculi is implemented in Prolog, providing seemingly the first automated reasoning systems for some of the considered logics.