M. Baaz and R. Zach, Algorithmic structuring of cut-free proofs, Lecture Notes in Computer Science, vol.702, pp.29-42, 1993.
DOI : 10.1007/3-540-56992-8_4

T. Dunchev, A. Leitsch, T. Libal, D. Weller, and B. Paleo, System Description: The Proof Transformation System CERES, 5th International Joint Conference on Automated Reasoning (IJCAR), pp.427-433, 2010.
DOI : 10.1007/978-3-642-14203-1_36
URL : https://hal.archives-ouvertes.fr/hal-00545482

F. Gécseg and M. Steinby, Tree Languages Handbook of Formal Languages, pp.1-68, 1997.

G. Gentzen, Untersuchungen ???ber das logische Schlie???en. I, Mathematische Zeitschrift, vol.39, issue.1, pp.176-210, 1934.
DOI : 10.1007/BF01201353

J. Herbrand, Recherches sur la théorie de la démonstration, 1930.

S. Hetzl, Proofs as Tree Languages, submitted

S. Hetzl, On the form of witness terms, Archive for Mathematical Logic, vol.7, issue.4, pp.529-554, 2010.
DOI : 10.1007/s00153-010-0186-7
URL : https://hal.archives-ouvertes.fr/hal-00498696

S. Hetzl, Applying Tree Languages in Proof Theory, Lecture Notes in Computer Science, vol.7183, pp.301-312, 2012.
DOI : 10.1007/978-3-642-28332-1_26

S. Hetzl, A. Leitsch, and D. Weller, Towards Algorithmic Cut-Introduction, In: Logic for Programming, Artificial Intelligence and Reasoning Lecture Notes in Computer Science, vol.7180, issue.18, pp.228-242, 2012.
DOI : 10.1007/978-3-642-28717-6_19
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.222.8297

S. Hetzl and L. Straßburger, Herbrand-Confluence for Cut-Elimination in Classical First-Order Logic
URL : https://hal.archives-ouvertes.fr/hal-00759228

F. Jacquemard, F. Klay, and C. Vacher, Rigid Tree Automata, Third International Conference on Language and Automata Theory and Applications (LATA) 2009, pp.446-457, 2009.
DOI : 10.1007/978-3-540-71389-0_13
URL : https://hal.archives-ouvertes.fr/inria-00579001

G. Mcguire, B. Tugemann, and G. Civario, There is no 16-Clue Sudoku: Solving the Sudoku Minimum Number of Clues Problem

D. Miller, A compact representation of proofs, Studia Logica, vol.19, issue.4, pp.347-370, 1987.
DOI : 10.1007/BF00370646

G. Sutcliffe, The TPTP Problem Library and Associated Infrastructure, Journal of Automated Reasoning, vol.13, issue.2, pp.337-362, 2009.
DOI : 10.1007/s10817-009-9143-8

J. Vysko?il, D. Stanovsk´ystanovsk´y, and J. Urban, Automated Proof Compression by Invention of New Definitions, Logic for Programming, Artifical Intelligence and Reasoning (LPAR-16). Lecture Notes in Computer Science, pp.447-462, 2010.
DOI : 10.1007/978-3-642-17511-4_25