A Schemata Calculus for Propositional Logic

We define a notion of formula schema handling arithmetic parameters, indexed propositional variables (e.g. P-i) and iterated conjunctions/disjunctions (e.g. boolean AND(n)(i=1) P-i, where n is a parameter). Iterated conjunctions or disjunctions are part of their syntax. We define a sound and complete (w.r.t. satisfiability) tableaux-based proof procedure for this language. This schemata calculus (called STAB) allows one to capture proof patterns corresponding to a large class of problems specified in propositional logic. Although the satisfiability problem is undecidable for unrestricted schemata, we identify a class of them for which STAB always terminates. An example shows evidence that the approach is applicable to non-trivial practical problems. We give some precise technical hints to pursue the present work.