Multiple-conclusion rules, hypersequents syntax and step frames

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 hypersequent calculi. Using step-algebras we develop a criterion establishing the bounded proof property and finite 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.