Current preprints

• D. Weller. Exposition: Synthesis via Functional Interpretation. [ arxiv ]
• S. Hetzl, D. Weller. Expansion Trees with Cut. [ arxiv ]
• C. Dunchev, A. Leitsch, M. Rukhaia, D. Weller. CERES for First-Order Schemata. [ arxiv ]

Publications

2014

• S. Hetzl, A. Leitsch, G. Reis, D. Weller. Algorithmic Introduction of Quantified Cuts. [ final | arxiv ]
• S. Hetzl, A. Leitsch, G. Reis, J. Tapolczai, D. Weller. Introducing Quantified Cuts in Logic with Equality, accepted at IJCAR'14, , 2014. [ arxiv ]
*

2012

• C. Dunchev, A. Leitsch, T. Libal, M. Riener, M. Rukhaia, D. Weller, B. Woltzenlogel Paleo. ProofTool: GUI for the GAPT Framework, 10th International Workshop On User Interfaces for Theorem Provers, 2012. *
• C. Dunchev, A. Leitsch, T. Libal, M. Riener, M. Rukhaia, D. Weller, B. Woltzenlogel Paleo. System Feature Description: Importing Refutations into the GAPT Framework, Proof Exchange for Theorem Proving workshop, 2012. *
• M. Baaz, S. Hetzl, D. Weller. On the complexity of proof deskolemization, Journal of Symbolic Logic 77(2), pp. 669-686, 2012. [ draft ] *
• S. Hetzl, A. Leitsch, D. Weller. Towards Algorithmic Cut-Introduction, Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), N. Bjørner, A. Voronkov (eds.), Springer LNCS 7180, pp. 228-242, 2012. *

2011

• D. Weller. On the Elimination of Quantifier-Free Cuts, Theoretical Computer Science 412(49), pp. 6843-6854, 2011. [ draft | final ] *
• S. Hetzl, A. Leitsch, D. Weller. CERES in Higher-Order Logic, Annals of Pure and Applied Logic 162(12), pp. 1001-1034, 2011. [ draft | final ] *

2010

• T. Dunchev, A. Leitsch, T. Libal, D. Weller, B. Woltzenlogel Paleo. System Description: The Proof Transformation System CERES, Int. Joint Conference on Automated Reasoning 2010, R. Goebel et al. (eds.), Springer LNCS 6173 [ springer ]

2009

• S. Hetzl, A. Leitsch, T. Libal, D. Weller, B. Woltzenlogel Paleo. Resolution Refinements for Cut-Elimination based on Reductive Methods, ESSLLI Workshop on Structures and Deduction (2009), [ online ]
• 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 [ online ]

2008

• S. Hetzl, A. Leitsch, D. Weller, B. Woltzenlogel Paleo. Transforming and Analyzing Proofs in the CERES-system, Proc. of the LPAR 2008 Workshops, Piotr Rudnicki et al. (eds.), ISSN 1613-0073 [ online ]
• S. Hetzl, A. Leitsch, D. Weller, B. Woltzenlogel Paleo. Herbrand Sequent Extraction, Intelligent Computer Mathematics, S. Autexier et al. (eds.), Springer LNAI 5144, pp. 462-477. [ doi ]
• S. Hetzl, A. Leitsch, D. Weller, B. Woltzenlogel Paleo. Proof Analysis with HLK, CERES and ProofTool: Current Status and Future Directions, Proc. of CICM Workshop ESARM'08, G. Sutcliffe et al. (eds.), ISSN 1613-0073 [ online ]

Talks

• The structure of the solution space in algorithmic cut-introduction , Third Workshop of the Amadeus Project on Proof Compression, Nancy, France, 2013 [ slides ]
• Deskolemization, Equality and Logical Complexity , Logical Models of Reasoning and Computation , Moscow, Russia, 2012 [ slides ] [ video ]
• Skolemization, Cut-free proofs and Complexity, Epsilon Calculus and Constructivity, Bergen, Norway, 2011 [ slides ]
• Proof search in cut-elimination, Collegium Logicum 2011: Proof Theory, LIX, École Polytechnique, France, 2011 [ slides ]
• On the complexity of proof deskolemization (with M. Baaz and S. Hetzl), Collegium Logicum: proofs and structures, Paris, France, 2010 [ slides ]
• Towards CERES in Higher-Order Logic, Talk at the Laboratoire d'Informatique de l'Ecole Polytechnique, France, 2010 [ slides ]
• Proof Skolemization and De-Skolemization, Workshop on Logic and Computation, Vienna, Austria, 2009 [ slides ]
• CERES: a program for cut-elimination, Kurt Gödel Research Center, Vienna, Austria, 2009 [ slides ]
• Transforming and Analyzing Proofs in the CERES-system, KEAPPA 2008, Doha, Qatar [ slides ]
• Cut-Elimination by Resolution and Skolemization in Second-Order Logic, APS 2008, Doha, Qatar [ slides ]
• Skolemization of Sequent Calculus Proofs in Higher-Order Logic (Work in Progress), Structural Proof Theory 2008, Paris, France [ slides ]
• Implementing CERES: tools for proof analysis, Collegium Logicum 2007, Vienna, Austria [ slides ]

Technical Reports

• S. Hetzl, A. Leitsch, D. Weller, B. Woltzenlogel Paleo. CERES in Second-Order Logic, Technical Report, Vienna University of Technology, 2008 [ online ]

Thesis

• D. Weller. CERES in Higher-Order Logic, PhD Thesis, Vienna University of Technology, 2010 [ online ]

Papers marked * where supported by the FWF through project I-603 N18.