| 2024 | LPAR | On Translations of Epsilon Proofs to LK. | Matthias Baaz, Anela Lolic |
| 2023 | WoLLIC | Effective Skolemization. | Matthias Baaz, Anela Lolic |
| 2022 | LFCS | Andrews Skolemization May Shorten Resolution Proofs Non-elementarily. | Matthias Baaz, Anela Lolic |
| 2020 | LFCS | A Globally Sound Analytic Calculus for Henkin Quantifiers. | Matthias Baaz, Anela Lolic |
| 2019 | WoLLIC | Note on Globally Sound Analytic Calculi for Quantifier Macros. | Matthias Baaz, Anela Lolic |
| 2018 | LFCS | A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem. | Matthias Baaz, Alexander Leitsch, Anela Lolic |
| 2018 | LPAR | Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gdel Logic. | Matthias Baaz, Anela Lolic |
| 2017 | LPAR | Gdel logics and the fully boxed fragment of LTL. | Matthias Baaz, Norbert Preining |
| 2016 | WoLLIC | Cut Elimination for Gdel Logic with an Operator Adding a Constant. | Juan P. Aguilera, Matthias Baaz |
| 2015 | CSL | Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic. | Matthias Baaz, Christian G. Fermller |
| 2015 | LICS | A Note on the Complexity of Classical and Intuitionistic Proofs. | Matthias Baaz, Alexander Leitsch, Giselle Reis |
| 2014 | KR | Vienna Summer of Logic. | Matthias Baaz, Thomas Eiter, Helmut Veith |
| 2012 | CADE | Effective Finite-Valued Semantics for Labelled Calculi. | Matthias Baaz, Ori Lahav, Anna Zamansky |
| 2010 | CSL | A Resolution Mechanism for Prenex Gdel Logic. | Matthias Baaz, Christian G. Fermller |
| 2010 | LPAR | Gdel logics with an operator shifting truth values. | Matthias Baaz, Oliver Fasching |
| 2009 | WoLLIC | SAT in Monadic Gdel Logics: A Borderline between Decidability and Undecidability. | Matthias Baaz, Agata Ciabattoni, Norbert Preining |
| 2008 | CiE | Herbrand Theorems and Skolemization for Prenex Fuzzy Logics. | Matthias Baaz, George Metcalfe |
| 2008 | LPAR | Cut Elimination for First Order Gdel Logic by Hyperclause Resolution. | Matthias Baaz, Agata Ciabattoni, Christian G. Fermller |
| 2007 | LPAR | Monadic Fragments of Gdel Logics: Decidability and Undecidability Results. | Matthias Baaz, Agata Ciabattoni, Christian G. Fermller |
| 2007 | TABLEAUX | Proof Theory for First Order Lukasiewicz Logic. | Matthias Baaz, George Metcalfe |
| 2005 | CSL | Note on Formal Analogical Reasoning in the Juridical Context. | Matthias Baaz |
| 2005 | LPAR | On Interpolation in Existence Logics. | Matthias Baaz, Rosalie Iemhoff |
| 2004 | LPAR | Cut-Elimination: Experiments with CERES. | Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr |
| 2004 | LPAR | CERES in Many-Valued Logics. | Matthias Baaz, Alexander Leitsch |
| 2003 | LPAR | A Translation Characterizing the Constructive Content of Classical Theories. | Matthias Baaz, Christian G. Fermller |
| 2002 | CADE | Proof Analysis by Resolution. | Matthias Baaz |
| 2002 | CSL | On Generalizations of Semi-terms of Particularly Simple Form. | Matthias Baaz, Georg Moser |
| 2002 | TABLEAUX | Proof Analysis by Resolution. | Matthias Baaz |
| 2002 | TABLEAUX | A Schtte-Tait Style Cut-Elimination Proof for First-Order Gdel Logic. | Matthias Baaz, Agata Ciabattoni |
| 2001 | CSL | On a Generalisation of Herbrand's Theorem. | Matthias Baaz, Georg Moser |
| 2001 | LPAR | Herbrand's Theorem for Prenex Gdel Logic and its Consequences for Theorem Proving. | Matthias Baaz, Agata Ciabattoni, Christian G. Fermller |
| 2000 | CSL | Hypersequent and the Proof Theory of Intuitionistic Fuzzy Logic. | Matthias Baaz, Richard Zach |
| 2000 | LPAR | Quantified Propositional Gdel Logics. | Matthias Baaz, Agata Ciabattoni, Richard Zach |
| 2000 | TABLEAUX | An Analytic Calculus for Quantified Propositional Gdel Logic. | Matthias Baaz, Christian G. Fermller, Helmut Veith |
| 1999 | CADE | System Description: CutRes 0.1: Cut Elimination by Resolution. | Matthias Baaz, Alexander Leitsch, Georg Moser |
| 1999 | TABLEAUX | Analytic Calculi for Projective Logics. | Matthias Baaz, Christian G. Fermller |
| 1998 | CSL | Quantifier Elimination in Fuzzy Logic. | Matthias Baaz, Helmut Veith |
| 1998 | MFCS | Proof Theory of Fuzzy Logics: Urquhart's C and Related Logics. | Matthias Baaz, Agata Ciabattoni, Christian G. Fermller, Helmut Veith |
| 1997 | TABLEAUX | Lean Induction Principles for Tableaux. | Matthias Baaz, Uwe Egly, Christian G. Fermller |
| 1996 | CADE | MUltlog 1.0: Towards an Expert System for Many-Valued Logics. | Matthias Baaz, Christian G. Fermller, Gernot Salzer, Richard Zach |
| 1996 | CSL | Fast Cut-Elimination by Projection. | Matthias Baaz, Alexander Leitsch |
| 1996 | TABLEAUX | Combining Many-valued and Intuitionistic Tableaux. | Matthias Baaz, Christian G. Fermller |
| 1995 | CSL | Incompleteness of a First-Order Gdel Logic and Some Temporal Logics of Programs. | Matthias Baaz, Alexander Leitsch, Richard Zach |
| 1995 | TABLEAUX | Non-elementary Speedups between Different Versions of Tableaux. | Matthias Baaz, Christian G. Fermller |
| 1994 | CSL | Semi-Unification and Generalizations of a Particularly Simple Form. | Matthias Baaz, Gernot Salzer |
| 1994 | KI | A New Frame For Common-Sense Reasoning - Towards Local Inconsistencies. | Matthias Baaz, Karin Hrwein |
| 1994 | LICS | A Non-Elementary Speed-Up in Proof Length by Structural Clause Form Transformation | Matthias Baaz, Christian G. Fermller, Alexander Leitsch |
| 1993 | CSL | Short Proofs of Tautologies Using the Schema of Equivalence. | Matthias Baaz, Richard Zach |
| 1993 | DEXA | The Application of Kripke-Type Structures to Regional Development Programs. | Matthias Baaz, Fernando Galindo, Gerald Quirchmayr, Manuel Vzqez |
| 1993 | LPAR | MULTILOG: A System for Axiomatizing Many-valued Logics. | Matthias Baaz, Christian G. Fermller, Arie Ovrutcki, Richard Zach |
| 1992 | CSL | Algorithmic Structuring of Cut-free Proofs. | Matthias Baaz, Richard Zach |
| 1992 | LPAR | Resolution for Many-Valued Logics. | Matthias Baaz, Christian G. Fermller |
| 1991 | DEXA | A Formal Model for the Support of Analogical Reasoning in Legal Expert Systems. | Matthias Baaz, Gerald Quirchmayr |
| 1990 | ISSAC | A Strong Problem Reduction Method Based on Function Introduction. | Matthias Baaz, Alexander Leitsch |