  We introduce a novel, logic-independent framework for the study of
sequent-style proof systems, which covers a number of proof-theoretic
formalisms and concrete proof systems that appear in the literature. In
particular, we introduce a generalized form of sequents, dubbed 'g-sequents,'
which are taken to be binary graphs of typical, Gentzen-style sequents. We then
define a variety of 'inference rule types' as sets of operations that act over
such objects, and define 'abstract (sequent) calculi' as pairs consisting of a
set of g-sequents together with a finite set of operations. Our approach
permits an analysis of how certain inference rule types interact in a general
setting, demonstrating under what conditions rules of a specific type can be
permuted with or simulated by others, and being applicable to any sequent-style
proof system that fits within our framework. We then leverage our permutation
and simulation results to establish generic calculus and proof transformation
algorithms, which show that every abstract calculus can be effectively
transformed into a lattice of polynomially equivalent abstract calculi. We
determine the complexity of computing this lattice and compute the relative
sizes of proofs and sequents within distinct calculi of a lattice. We recognize
that top elements in lattices correspond to nested sequent systems, while
bottom elements correspond to labeled sequent systems, and observe that top and
bottom elements coincide with many known (cut-free) nested and labeled sequent
systems for logics characterized by Horn properties.
