HLK ProofTool
TU Vienna logic.at Theory and Logic Group (E185-2)

Bibliography

1
G. Gentzen, Untersuchungen über das logische Schließen, Mathematische Zeitschrift 39 (1934-1935) 176-210,405-431.

2
E. Eder, Relative complexities of first-order calculi, Vieweg, 1992.

3
M. Baaz, A. Leitsch, On skolemization and proof complexity, Fundamenta Informaticae 20 (4) (1994) 353-379.

4
M. Baaz, A. Leitsch, Cut Normal Forms and Proof Complexity, Annals of Pure and Applied Logic 97 (1999) 127-177.

5
M. Baaz, A. Leitsch, Cut-elimination and Redundancy-elimination by Resolution, Journal of Symbolic Computation 29 (2) (2000) 149-176.

6
M. Baaz, S. Hetzl, A. Leitsch, C. Richter, H. Spohr, Proof Transformation by CERES, in: J. M. Borwein, W. M. Farmer (Eds.), Mathematical Knowledge Management (MKM) 2006, Vol. 4108 of Lecture Notes in Artificial Intelligence, Springer, 2006, pp. 82-93.

7
C. Richter, Proof transformations by resolution - computational methods of cut-elimination, Ph.D. thesis, Vienna University of Technology (2006).

8
S. Hetzl, A. Leitsch, D. Weller, B. Woltzenlogel Paleo. A Clausal Approach to Proof Analysis in Second-Order Logic, Logical Foundations of Computer Science 2009, Sergei Artemov and Anil Nerode (eds.), Springer LNCS 5407

9
B. Woltzenlogel Paleo, A General Analysis of Cut-Elimination by CERes, Ph.D. thesis, Vienna University of Technology (2009).

10
M. Baaz, A. Leitsch, Methods of Cut-elimination. To appear in: Trends in Logic, Springer (2010).