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

Note: Due to the rollout of TU Wien’s new publication database, the list below may be slightly outdated. Once APIs for the new database have been released, everything will be up to date again.

2021

2020

2019

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
  • 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
  • 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

2012

  • CERES for First-Order Schemata / A. Leitsch / Talk: Collegium Logicum 2012: Structural Proof Theory, Paris, France; 2012-11-15 - 2012-11-16
  • 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
  • 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

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 / 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
  • 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

2008

2007

2006

  • 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
  • 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

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

 

Note: Due to the rollout of TU Wien’s new publication database, the list below may be slightly outdated. Once APIs for the new database have been released, everything will be up to date again.