References
[1] M. Baaz and A. Leitsch, Cut-elimination and Redundancy-elimination by Resolution, Journal of Symbolic Computation 29 (2), pp. 149-176, 2000.
[2] M. Baaz and A. Leitsch, Towards a clausal analysis of cut-elimination, Journal of Symbolic Computation 41 (3-4), pp. 381-410, 2006.
[3] Stefan Hetzl, Alexander Leitsch, Daniel Weller, and Bruno Woltzenlogel Paleo, A clausal approach to proof analysis in second-order logic. In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, volume 5407 of Lecture Notes in Computer Science, pp. 214-229. Springer Berlin, 2009.
[4] V. Aravantinos, R. Caferra and N. Peltier, A Schemata Calculus For Propositional Logic. In 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2009), Springer, 2009.
[5] V. Aravantinos, R. Caferra and N. Peltier, RegSTAB: a SAT-Solver for Propositional Schemata. In IJCAR 2010 (International Joint Conference on Automated Reasoning), Springer, 2010.
[6] Stefan Hetzl, Alexander Leitsch, and Daniel Weller. Ceres in higher-order logic. Annals of Pure and Applied Logic, 162(12), pp. 1001-1034, 2011.
[7] V. Aravantinos, R. Caferra and N. Peltier, Decidability and Undecidability Results for Propositional Schemata. In Journal of Artificial Intelligence Research, 40, pp. 599-656, 2011.
[8] Vincent Aravantinos and Nicolas Peltier. Generating schemata of resolution proofs. In Martin Giese and Roman Kuznets, editors, TABLEAUX 2011 Workshops, Tutorials, and Short Papers, pp. 16-30, 2011.
[9] M. Aigner and G. Ziegler. Proofs from THE BOOK. Springer, 1999.
[10] Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, and Hendrik Spohr. CERES: An analysis of Fuerstenberg's proof of the infinity of primes. Theoretical Computer Science, 403, pp. 160-175, 2008.