References
Proofs from THE BOOK, Springer, 1999.
Resolution in Type Theory, Journal of Symbolic Logic 36 (1971) 414-432.
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.
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
System Description: The Proof Transformation system CERES, Proceedings
of IJCAR'10, Lecture Notes in Computer Science 6173, 427-
433 (2010).
Relative Complexities of First-Order Calculi, Vieweg, 1992.
Untersuchungen über das logische Schließen,
Mathematische Zeitschrift 39 (1934-1935) 176-210, 405-431.
Proof Theory and Logical Complexity, Elsevier, 1987.
Recherches sur la théorie de la démonstration, Ph.D. thesis,
University of Paris (1930).
CERES in Higher-Order Logic,
in: Workshop on Classical Logic and Computation (pdf)
CERES in Higher-Order Logic, in: Annals of Pure and Applied Logic 162(12) (pdf)
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
Equational Theories in CERES, unpublished (available at
http://www.logic.at/ceres/)
(2005).
Herbrand-Analysen zweier Beweise des Satzes von Roth:
Polynomiale Anzahlschranken, Journal of Symbolic Logic 54 (1) (1989) 234-263.
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.
Proof Transformations by Resolution - Computational Methods of
Cut-Elimination, Ph.D. thesis, Vienna University of Technology (2006).
Subsystems of Second Order Arithmetic, Springer, 1999.
Proof Theory, North-Holland, Amsterdam, 1987.
Classical logic and computation, Ph.D. thesis, University of
Cambridge (October 2000).
CERES in Higher-Order Logic, Ph.D. Thesis, Vienna University of Technology, 2010 (pdf)