Multiple-conclusion Rules, Hypersequents Syntax and Step Frames
Nick Bezhanishvili, Silvio Ghilardi

Abstract:
We investigate proof theoretic properties of logical systems via
algebraic methods. We introduce a calculus for deriving
multiple-conclusion rules and show that it is a Hilbert style
counterpart of hyper-sequent calculi. Using step-algebras we develop a
criterion establishing the bounded proof property and nite model
property for these systems. Finally, we show how this criterion can be
applied to universal classes axiomatized by certain canonical rules,
thus recovering and extending known results from both semantically and
proof-theoretically inspired modal literature