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

References

M. Aigner and G. Ziegler
Proofs from THE BOOK, Springer, 1999.
P. B. Andrews
Resolution in Type Theory, Journal of Symbolic Logic 36 (1971) 414-432.
M. Baaz, S. Hetzl, A. Leitsch, C. Richter and H. Spohr
Cut-Elimination: Experiments with CERES, in: F. Baader, A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) 2004, Vol. 3452 of Lecture Notes in Computer Science, Springer, 2005, pp. 481-495.
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.
CERES: An analysis of Fürstenberg's proof of the infinity of primes, Theoretical Computer Science 403 (2-3) (2008) 160-175.
M. Baaz and A. Leitsch
On skolemization and proof complexity, Fundamenta Informaticae 20 (4) (1994) 353-379
Cut Normal Forms and Proof Complexity, Annals of Pure and Applied Logic 97 (1999) 127-177.
Cut-elimination and Redundancy-elimination by Resolution, Journal of Symbolic Computation 29 (2) (2000) 149-176.
Towards a clausal analysis of cut-elimination, Journal of Symbolic Computation 41 (3-4) (2006) 381-410.
Fast Cut-Elimination by CERES, in Proofs, Categories and Computations, S. Feferman, W. Sieg (Ed.), College Publications, London, 2010, ISBN 978-1-84890-012-7, pp.31-49.
Methods of Cut-Elimination, Trends in Logic Vol. 34, Springer, 2010, ISBN 978-94-007-0319-3
T. Dunchev, A. Leitsch, T. Libal, D. Weller and B. Woltzenlogel Paleo
System Description: The Proof Transformation system CERES, Proceedings of IJCAR'10, Lecture Notes in Computer Science 6173, 427- 433 (2010).
E. Eder
Relative Complexities of First-Order Calculi, Vieweg, 1992.
G. Gentzen
Untersuchungen ├╝ber das logische Schlie├čen, Mathematische Zeitschrift 39 (1934-1935) 176-210, 405-431.
J.-Y. Girard
Proof Theory and Logical Complexity, Elsevier, 1987.
J. Herbrand
Recherches sur la théorie de la démonstration, Ph.D. thesis, University of Paris (1930).
S. Hetzl, A. Leitsch, D. Weller
S. Hetzl, A. Leitsch, D. Weller, B. Woltzenlogel Paleo
Herbrand Sequent Extraction, in: S. Autexier et al. (Eds.), Intelligent Computer Mathematics, Vol. 5144 of Lecture Notes in Computer Science, Springer, 2008, pp. 462-477
A Clausal Approach to Proof Analysis in Second-Order Logic, in: S. Artemov and A. Nerode (Eds.), Logical Foundations of Computer Science, Vol. 5407 of Lecture Notes in Computer Science, Springer, 2009, pp. 214-229
A. Leitsch and C. Richter
H. Luckhardt
Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken, Journal of Symbolic Logic 54 (1) (1989) 234-263.
G. Polya
Mathematics and Plausible Reasoning, Volume I: Induction and Analogy in Mathematics, Princeton University Press, 1954.
Mathematics and Plausible Reasoning, Volume II: Patterns of Plausible Inference, Princeton University Press, 1954.
C. Richter
Proof Transformations by Resolution - Computational Methods of Cut-Elimination, Ph.D. thesis, Vienna University of Technology (2006).
S. G. Simpson
Subsystems of Second Order Arithmetic, Springer, 1999.
G. Takeuti
Proof Theory, North-Holland, Amsterdam, 1987.
C. Urban
Classical logic and computation, Ph.D. thesis, University of Cambridge (October 2000).
D. Weller