Talks

• Proof Structuring and Compression by Atomic-Cut-Introduction by Resolution (CIRes)
  • In the Seminar of the Theory and Logic Groups of the TU-Wien (Vienna, Austria, November 2009).

• A General Analysis of Cut-Elimination by CERes
  • In the defense of my PhD Thesis (Vienna, Austria, November 2009)

• Resolution Refinements for Cut-Elimination based on Reductive Methods
  • In the Workshop on Structures and Deduction, part of the European Summer School of Logic, Language and Information (ESSLLI 2009) (Bordeaux, France, July 2009)

• Atomic-Cut-Introduction (and Proof Compression) by Resolution: Preliminary Investigations
  • In the 8th Conference on Proof, Computation and Complexity (Nancy, France, July 2009).

• Clause Sets and Projections for Cut-Elimination by Resolution
  • Invited talk for the Calligramme team in INRIA (Nancy, France, July 2009).

• Sequent Calculi with Hilbert's Choice Operator Epsilon
  • In the final seminar of Prof. Richard Zach's course on the Epsilon Calculus, TU-Wien (Vienna, Austria, May 2009).

• Análise e Transformação de Provas Matemáticas através da Eliminação de Cortes
  • In the Seminar of Logic of the Center of Logic, Epistemology and History of Science, University of Campinas (UniCamp) (Campinas, Brasil, March 2009).

• Reductive Cut-Elimination by Resolution
  • In the Seminar of the Theory and Logic Groups of the TU-Wien (Vienna, Austria, January 2009).
  • Errata: Stefan Hetzl found a counter-example for my declarative definition of the profile. Read these slides with care!

• Goedel's Incompleteness Theorem and the Theory of Everything in Physics
  • In the Seminar of Physics and Logic of the TU-Wien (Vienna, Austria, December 2008).
  • Additional material: Erman's Slides | Diagonal Lemma

• The No Counter-Example Interpretation
  • In the Seminar of Logic of the TU-Wien (Vienna, Austria, November 2008).

• Herbrand Sequent Extraction for Mathematical Knowledge Management
  • In the International Conference on Mathematical Knowledge Management (Birmingham, England, July 2008).

• Proof Analysis with CERes, HLK and ProofTool
  • In the Workshop on Empirically Successful Automated Reasoning for Mathematics (Birmingham, England, July 2008).

• Herbrand Sequent Extraction
  • In the Workshop on Classical Logic and Computation (Reyjkjavik, Iceland, July 2008).

• Cut-Elimination by Resolution and Herbrand Sequent Extraction
  • In the Workshop on Deep Inference (Nancy, France, June 2008).

• Herbrand Sequent Extraction
  • In the Computation Logic Student Workshop (Lisbon, Portugal, February 2008).