TU Wien Informatics

Alexander Leitsch

Univ.Prof.i.R. Dr.phil.

Research Focus

Research Areas

  • automated deduction, proof theory

About

1) Automated deduction: Resolution decision procedures, decidable classes of first-order logic, automated model building, subsumption algorithms. 2) Proof theory: Analysis of cut elimination 3) Automated Lemma Generation 4) Proof Analysis

Role

2018

2017

2016

2015

2014

2013

  • Methods of Cut-Elimination / A. Leitsch / Talk: Ninth International Tbilisi Summer School in Logic and Language, Tbilisi, Georgia; 2013-09-30 - 2013-10-04
  • A method of algorithmic cut-introduction / A. Leitsch / Talk: Workshop on Skolemization, Utrecht; 2013-05-27 - 2013-05-29
  • Ceres for First-Order Schemata / A. Leitsch, T. Dunchev, D. Weller, M. Rukhaia / CoRR - Computing Research Repository, arXiv:1303.4257 (2013), 1 - 40
  • Prooftool: a GUI for the GAPT Framework / A. Leitsch, T. Libal, M. Riener, D. Weller, B. Woltzenlogel-Paleo, T. Dunchev / Talk: 10th International Workshop On User Interfaces for Theorem Provers, Bremen; 2013-07-11; in: "Proceedings 10th International Workshop on User Interfaces for Thorem Provers,", C. Kaliszyk et al. (ed.); (2013), ISSN: 2075-2180; 1 - 14

2012

  • CERES for First-Order Schemata / A. Leitsch / Talk: Collegium Logicum 2012: Structural Proof Theory, Paris, France; 2012-11-15 - 2012-11-16
  • Towards Algorithmic Cut-Introduction / A. Leitsch, S. Hetzl, D. Weller / in: "Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18", N. Bjorner, A. Voronkov (ed.); Springer LNCS, 2012, ISBN: 978-3-642-28716-9, 228 - 242
  • Towards CERes in intuitionistic logic / A. Leitsch, G. Reis, B. Woltzenlogel-Paleo / in: "Computer Science Logic (CSL'12) - 26th International Workshop/21st", P. Cegielski et al. (ed.); Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2012, ISBN: 978-3-939897-42-2, 485 - 499
  • System feature description: importing refutations into the GAPT framework / C. Dunchev, A. Leitsch, T. Libal, M. Riener, M. Rukhaia, D. Weller, B. Woltzenlogel-Paleo / Talk: Proof Exchange for Theorem Proving, Second International Workshop, Manchester, UK; 2012-06-30; in: "Proceeding of Proof Exchange for Theorem Proving | Second International Workshop, PxTP 2012", D. Pichardie, T. Weber (ed.); (2012), ISSN: 1613-0073; 51 - 57

2011

2010

  • CERES in higher-order-logic / A. Leitsch / Talk: Collegium Locicum 2010: Proofs and Structures, Paris (invited); 2010-11-08 - 2010-11-10
  • CERES in higher-order-logic / S. Hetzl, A. Leitsch, D. Weller / Talk: Workshop on Classical Logic and Computation (CL&C'10), Brünn; 2010-08-22
  • Fast Cut-Elimination by CERES / A. Leitsch, M. Baaz / in: "Proofs, Categories and Computations", S. Feferman, W. Sieg (ed.); College Publications, London, 2010, ISBN: 978-1-84890-012-7, 31 - 49
  • Fast cut-elimination by CERES / M. Baaz, A. Leitsch / in: "Proofs, Categories and Computations, Essays in Honor of Grigori Mints", S. Feferman, W. Sieg (ed.); College Publications (Kings College), 2010, ISBN: 978-1-84890-012-7, 31 - 48
  • System Description: The Proof Transformation System CERES / A. Leitsch, T. Dunchev, D. Weller, B. Woltzenlogel-Paleo, T. Libal / in: "IJCAR 2010", J. Giesl, R. Hähnle (ed.); Springer, LNAI, Heidelberg, 2010, ISBN: 978-3-642-14202-4, 427 - 433

2009

  • Fast Cut-Elimination by CERES / A. Leitsch / Talk: Moscow-Vienna Workshop on Logic and Computation 2009, Wien (invited); 2009-06-29 - 2009-07-02
  • A Clausal Approach to Proof Analysis in Second-Order Logic / A. Leitsch, S. Hetzl, D. Weller, B. Woltzenlogel-Paleo / in: "Lecture Notes in Computer Science, 5407", E. Artemov, A. Nerode (ed.); Springer LNCS, Heidelberg, 2009, ISBN: 3-540-92686-0, 214 - 229
  • A Clausal Approach to Proof Analysis in Second-Order Logic / A. Leitsch, S. Hetzl, D. Weller, B. Woltzenlogel-Paleo / Talk: Symposium on Logical Foundations of Computer Science (LFCS 2009), Deerfield Beach, FL, USA; 2009-01-03 - 2009-01-06; in: "Logical Foundations of Computer Science", A. Nerode, S. Artemov (ed.); Springer, LNCS, 5407 (2009), ISBN: 3-540-92686-0; 214 - 229

2008

2007

2006

  • CERES: Cut-Elimination by Resolution / A. Leitsch / Talk: MANYVAL 06, Gargnano; 2006-03-20 - 2006-03-22
  • Proof transformation by CERES / M. Baaz, S. Hetzl, A. Leitsch, Clemens Richter, H. Spohr / Lecture Notes in Computer Science, 4108 (2006), 82 - 93
  • Towards a clausal analysis of cut-elimination / M. Baaz, A. Leitsch / Journal of Symbolic Computation, 41 (2006), 381 - 410
  • Proof Transformation by CERES / M. Baaz, S. Hetzl, A. Leitsch, Clemens Richter, H. Spohr / in: "MKM 2006", J.M. Borwein, W.M. Farmer (ed.); Springer, Berlin Heidelberg, 2006, 82 - 93
  • System Description: The Cut-Elimination System CERES / M. Baaz, S. Hetzl, A. Leitsch, Clemens Richter, H. Spohr / Talk: FLoC'06 Workshop on Empirically Successful Computerized Reasoning (ESCoR), Seattle, USA; 2006-08-21; in: "ESCoR 2006 Empirically Successful Computerized Reasoning", G. Sutcliffe, R. Schmidt, S. Schulz (ed.); CEUR Workshop Proceedings, 192 (2006), ISSN: 1613-0073; Paper ID 11, 9 pages

2005

  • Abstracting from the Propositional Structure of First-Order Proofs / S. Hetzl, A. Leitsch / Talk: Paris-Vienna Workshop 2005, Paris; 2005-12-19
  • Cut-Elimination: Experiments with CERES / M. Baaz, S. Hetzl, A. Leitsch, Clemens Richter, H. Spohr / Talk: Second Florence-Vienna Workshop on Logic and Computation, Florenz; 2005-11-02 - 2005-11-05
  • CERES in many-valued logics / A. Leitsch / Talk: Second Florence-Vienna Workshop on Logic and Computation, Florenz, Italien; 2005-11-02 - 2005-11-05
  • Computational Analysis of Proofs / A. Leitsch / Talk: European Summer School in Logic Language and Information 2005, Edinburgh, U.K.; 2005-08-13 - 2005-08-20
  • The Resolution Principle / A. Leitsch, C. Fermüller / in: "Handbook of Philosophical Logic, 2nd ed., Volume 12", D.M. Gabbay, F. Guenthner (ed.); Springer, Dordrecht, Netherlands, 2005, 87 - 173
  • Cut-Elimination: Experiments with CERES / M. Baaz, S. Hetzl, A. Leitsch, Clemens Richter, H. Spohr / in: "LOgic for Programming, Artificial Intelligence, and Reasoning", issued by: Franz Baader, Andrei Voronkov; Springer, LNAI, Heidelberg, 2005, ISBN: 3-540-25236-3, 481 - 495
  • Event-related Outputs of Computations in P Systems / M. Cavaliere, R. Freund, A. Leitsch, Gh. Paun / in: "Third Brainstorming Week on Membrane Computing", M.A. Gutiérrez-Naranjo, A. Riscos-Núñez, F.J. Romero-Campero, D. Sburlan (ed.); issued by: Research Group on Natural Computing, Sevilla University; Fénix Editora, Sevilla, 2005, 107 - 122
  • CERES in many-valued logics / M. Baaz, A. Leitsch / in: "Logic for Programming, Artificial Intelligence, and Reasoning (LNAI 3452)", F. Baader, A. Voronkov (ed.); Springer, 2005, ISBN: 3-540-25236-3, 1 - 20
  • Resolution Theorem Proving: a logical point of view / A. Leitsch / in: "Logic Colloquium '01", issued by: Matthias Baaz, Sy-David Friedman, Jan Krajicek; Association of Symbolic Logic, A K Peters, Ltd., Wellesley, Massachusetts, 2005, (invited), ISBN: 1-56881-247-7, 3 - 42
  • CERES in Many-Valued Logics / A. Leitsch, M. Baaz / in: "Logic for Programming, Artificial Intelligence, and Reasoning", issued by: Franz Baader, Andrei Voronkov; Springer, LNAI, Heidelberg, 2005, (invited), ISBN: 3-540-25236-3, 1 - 20

2004

2003