Abstract In this dissertation we study schematic formulae and proofs from both the propositional and first-order perspective. By schematic we mean that the formulae have a free numeric parameter indexing the formulae. In the propositional case we study an extension of a decision procedure for satisfiability of regular propositional schematic formulae, defined in , allowing for multiple free parameters within a single formula. Our work concerning first-order schematic formulae makes up the major of the dissertation and is mainly concerned with cut-elimination for proof schemata using the CERES method . By proof schemata, we are referring to a restricted form of cyclic proofs with a free indexing parameter. The CERES method of cut elimination introduced in  extracts what is referred to as the characteristic clause set from a sequent calculus proof and uses resolution to refute the clause set. The characteristic clause set represents the cut structure of the sequent calculus proof it is derived from and is always unsatisfiable. Unlike the work of , which introduces a complete method for cut elimination in first order logic,  only introduces a framework which can be used to define proof schemata and possibly eliminate the cuts within a given proof schemata. The problem with proof schemata is that they essentially define an infinite sequence of proofs and many theoretic results used in  no longer hold for proof schemata. For example, reductive cut elimination is not as straight forward as it was for first-order sequent calculus proofs and it is unclear if it is even possible to define a reductive method for proof schemata. Also, most importantly, resolution is on longer a complete method for unsatisfiable clause sets, specifically, it is not complete for unsatisfiable schematic clause sets. This issue with resolution being one of the main issues addressed in this thesis. We approach this problem of the lack of a theoretic backbone for cut-elimination on proof schemata by constructing several formal proofs in a schematic version of the standard sequent calculus, each of which is based on a well studied problem (the infinitary pigeonhole principle) often used in the analysis of proof complexity within a given proof system. Using these formal proofs, we apply the schematic version of the CERES method to each of the proofs to see if the method is expressive enough to handle cut elimination for the given proof schema, and if it is not, we ask if we can generalize certain parts of the method to handle the given proof schema and allow for cut elimination in this more general framework. In the process, we develop a generalized version of the resolution calculus introduced in , a possible method for Herbrand sequent extraction, though the method is quite restrictive and relies a lot on the structure of the proof schema, and combinatorial results pertaining to the structure of the characteristic clause sets of the given proof schemata. As a final remark, theorem provers where heavily used in the application of the schematic CERES method to the formalized proof schemata used in this dissertation. We also provide an outline as to how this was done and what results where attained with the aid of automated theorem provers, as well as, idea on how automated theorem provers might be beneficial to future research in this subject.