  We define a logic of propositional formula schemata adding to the syntax of
propositional logic indexed propositions and iterated connectives ranging over
intervals parameterized by arithmetic variables. The satisfiability problem is
shown to be undecidable for this new logic, but we introduce a very general
class of schemata, called bound-linear, for which this problem becomes
decidable. This result is obtained by reduction to a particular class of
schemata called regular, for which we provide a sound and complete terminating
proof procedure. This schemata calculus allows one to capture proof patterns
corresponding to a large class of problems specified in propositional logic. We
also show that the satisfiability problem becomes again undecidable for slight
extensions of this class, thus demonstrating that bound-linear schemata
represent a good compromise between expressivity and decidability.
