Eine Methode zur automatischen Problemreduktion. - Matthias Baaz; Alexander Leitsch (ÖGAI, 1985)

Kripke-type semantics for da Costa's paraconsistent logic Cω. - Matthias Baaz (Notre Dame J. Formal Log., 1986)

Strong splitting rules in automated theorem proving. - Matthias Baaz; Alexander Leitsch (EUROCAL, 1987)

Automatisches Beweisen für Logiksysteme, in denen Widersprüche behandelt werden können. - Matthias Baaz (ÖGAI, 1987)

An Effective Decision Algorithm for Propositional Temporal Logic. - Matthias Baaz (ÖGAI, 1989)

A Strong Problem Reduction Method Based on Function Introduction. - Matthias Baaz; Alexander Leitsch (ISSAC, 1990)

A Formal Model for the Support of Analogical Reasoning in Legal Expert Systems. - Matthias Baaz; Gerald Quirchmayr (DEXA, 1991)

Algorithmic Structuring of Cut-free Proofs. - Matthias Baaz; Richard Zach (CSL, 1992)

Resolution for Many-Valued Logics. - Matthias Baaz; Christian G. Fermüller (LPAR, 1992)

Complexity of Resolution Proofs and Function Introduction. - Matthias Baaz; Alexander Leitsch (Ann. Pure Appl. Log., 1992)

Note on calculi for a three-valued logic for logic programming.. - Matthias Baaz; Richard Zach (Bull. EATCS, 1992)

Short Proofs of Tautologies Using the Schema of Equivalence. - Matthias Baaz; Richard Zach (CSL, 1993)

The Application of Kripke-Type Structures to Regional Development Programs. - Matthias Baaz; Fernando Galindo; Gerald Quirchmayr; Manuel Vázqez (DEXA, 1993)

Systematic Construction of Natural Deduction Systems for Many-Valued Logics. - Matthias Baaz; Christian G. Fermüller; Richard Zach (ISMVL, 1993)

MULTILOG: A System for Axiomatizing Many-valued Logics. - Matthias Baaz; Christian G. Fermüller; Arie Ovrutcki; Richard Zach (LPAR, 1993)

Dual systems of sequents and tableaux for many-valued logics. - Matthias Baaz; Christian G. Fermüller; Richard Zach (Bull. EATCS, 1993)

Elimination of Cuts in First-order Finite-valued Logics. - Matthias Baaz; Christian G. Fermüller; Richard Zach (J. Inf. Process. Cybern., 1993)

Semi-Unification and Generalizations of a Particularly Simple Form. - Matthias Baaz; Gernot Salzer (CSL, 1994)

Approximating Propositional Calculi by Finite-Valued Logics. - Matthias Baaz; Richard Zach (ISMVL, 1994)

A New Frame For Common-Sense Reasoning - Towards Local Inconsistencies. - Matthias Baaz; Karin Hörwein (KI, 1994)

A Non-Elementary Speed-Up in Proof Length by Structural Clause Form Transformation - Matthias Baaz; Christian G. Fermüller; Alexander Leitsch (LICS, 1994)

On Skolemization and Proof Complexity. - Matthias Baaz; Alexander Leitsch (Fundam. Informaticae, 1994)

Incompleteness of a First-Order Gödel Logic and Some Temporal Logics of Programs. - Matthias Baaz; Alexander Leitsch; Richard Zach (CSL, 1995)

Non-elementary Speedups between Different Versions of Tableaux. - Matthias Baaz; Christian G. Fermüller (TABLEAUX, 1995)

Generalizing Theorems in Real Closed Fields. - Matthias Baaz; Richard Zach (Ann. Pure Appl. Log., 1995)

Resolution-Based Theorem Proving for Manyvalued Logics. - Matthias Baaz; Christian G. Fermüller (J. Symb. Comput., 1995)

MUltlog 1.0: Towards an Expert System for Many-Valued Logics. - Matthias Baaz; Christian G. Fermüller; Gernot Salzer; Richard Zach (CADE, 1996)

Fast Cut-Elimination by Projection. - Matthias Baaz; Alexander Leitsch (CSL, 1996)

Intuitionistic Counterparts of Finitely-Valued Logics. - Matthias Baaz; Christian G. Fermüller (ISMVL, 1996)

Combining Many-valued and Intuitionistic Tableaux. - Matthias Baaz; Christian G. Fermüller (TABLEAUX, 1996)

The Axiom of Choice in Quantum Theory. - Matthias Baaz; Norbert Brunner; Karl Svozil (Math. Log. Q., 1996)

Completeness of a First-Order Temporal Logic with Time-Gaps. - Matthias Baaz; Alexander Leitsch; Richard Zach (Theor. Comput. Sci., 1996)

Lean Induction Principles for Tableaux. - Matthias Baaz; Uwe Egly; Christian G. Fermüller (TABLEAUX, 1997)

Quantifier Elimination in Fuzzy Logic. - Matthias Baaz; Helmut Veith (CSL, 1998)

Compact Propositional Gödel Logics. - Matthias Baaz; Richard Zach (ISMVL, 1998)

Proof Theory of Fuzzy Logics: Urquhart's C and Related Logics. - Matthias Baaz; Agata Ciabattoni; Christian G. Fermüller; Helmut Veith (MFCS, 1998)

Note on generalizing theorems in algebraically closed fields. - Matthias Baaz; Richard Zach (Arch. Math. Log., 1998)

Labeled Calculi and Finite-Valued Logics. - Matthias Baaz; Christian G. Fermüller; Gernot Salzer; Richard Zach (Stud Logica, 1998)

Embedding Logics into Product Logic. - Matthias Baaz; Petr Hájek 001; David Svejda; Jan Krajícek (Stud Logica, 1998)

System Description: CutRes 0.1: Cut Elimination by Resolution. - Matthias Baaz; Alexander Leitsch; Georg Moser (CADE, 1999)

On the Undecidability of some Sub-Classical First-Order Logics. - Matthias Baaz; Agata Ciabattoni; Christian G. Fermüller; Helmut Veith (FSTTCS, 1999)

Analytic Calculi for Projective Logics. - Matthias Baaz; Christian G. Fermüller (TABLEAUX, 1999)

Interpolation in fuzzy logic. - Matthias Baaz; Helmut Veith (Arch. Math. Log., 1999)

Cut Normal Forms and Proof Complexity. - Matthias Baaz; Alexander Leitsch (Ann. Pure Appl. Log., 1999)

Note on the Generalization of Calculations. - Matthias Baaz (Theor. Comput. Sci., 1999)

Hypersequent and the Proof Theory of Intuitionistic Fuzzy Logic. - Matthias Baaz; Richard Zach (CSL, 2000)

Quantified Propositional Gödel Logics. - Matthias Baaz; Agata Ciabattoni; Richard Zach (LPAR, 2000)

An Analytic Calculus for Quantified Propositional Gödel Logic. - Matthias Baaz; Christian G. Fermüller; Helmut Veith (TABLEAUX, 2000)

Cut-elimination and Redundancy-elimination by Resolution. - Matthias Baaz; Alexander Leitsch (J. Symb. Comput., 2000)

Normal Form Transformations. - Matthias Baaz; Uwe Egly; Alexander Leitsch (Handbook of Automated Reasoning, 2001)

Automated Deduction for Many-Valued Logics. - Matthias Baaz; Christian G. Fermüller; Gernot Salzer (Handbook of Automated Reasoning, 2001)

On a Generalisation of Herbrand's Theorem. - Matthias Baaz; Georg Moser (CSL, 2001)

A Note on the Proof-Theoretic Strength of a Single Application of the Schema of Identity. - Matthias Baaz; Christian G. Fermüller (Proof Theory in Computer Science, 2001)

Comparing the Complexity of Cut-Elimination Methods. - Matthias Baaz; Alexander Leitsch (Proof Theory in Computer Science, 2001)

Cut-Elimination in a Sequents-of-Relations Calculus for Gödel Logic. - Matthias Baaz; Agata Ciabattoni; Christian G. Fermüller (ISMVL, 2001)

Herbrand's Theorem for Prenex Gödel Logic and its Consequences for Theorem Proving. - Matthias Baaz; Agata Ciabattoni; Christian G. Fermüller (LPAR, 2001)

Complexity of t-tautologies. - Matthias Baaz; Petr Hájek 001; Franco Montagna; Helmut Veith (Ann. Pure Appl. Log., 2001)

On Generalizations of Semi-terms of Particularly Simple Form. - Matthias Baaz; Georg Moser (CSL, 2002)

Proof Analysis by Resolution. - Matthias Baaz (TABLEAUX, 2002)

A Schütte-Tait Style Cut-Elimination Proof for First-Order Gödel Logic. - Matthias Baaz; Agata Ciabattoni (TABLEAUX, 2002)

Foreword. - Matthias Baaz; Georg Gottlob; Georg Moser (Theor. Comput. Sci., 2002)

Characterization of the Axiomatizable Prenex Fragments of First-Order Gödel Logics. - Matthias Baaz; Norbert Preining; Richard Zach (ISMVL, 2003)

A Translation Characterizing the Constructive Content of Classical Theories. - Matthias Baaz; Christian G. Fermüller (LPAR, 2003)

Hypersequent Calculi for Gödel Logics - a Survey. - Matthias Baaz; Agata Ciabattoni; Christian G. Fermüller (J. Log. Comput., 2003)

Cut-Elimination: Experiments with CERES. - Matthias Baaz; Stefan Hetzl; Alexander Leitsch; Clemens Richter; Hendrik Spohr (LPAR, 2004)

CERES in Many-Valued Logics. - Matthias Baaz; Alexander Leitsch (LPAR, 2004)

Analytic Calculi for Monoidal T-norm Based Logic. - Matthias Baaz; Agata Ciabattoni; Franco Montagna (Fundam. Informaticae, 2004)

On the Proof Theory of the Existence Predicate. - Matthias Baaz; Rosalie Iemhoff (We Will Show Them! (1), 2005)

Note on Formal Analogical Reasoning in the Juridical Context. - Matthias Baaz (CSL, 2005)

On Interpolation in Existence Logics. - Matthias Baaz; Rosalie Iemhoff (LPAR, 2005)

Controlling witnesses. - Matthias Baaz (Ann. Pure Appl. Log., 2005)

Editorial. - Matthias Baaz; Agata Ciabattoni; Dov M. Gabbay; Petr Hájek 001 (Log. J. IGPL, 2005)

Editorial. - Sergei I. Adian; Matthias Baaz; Lev D. Beklemishev (J. Log. Comput., 2005)

Note on Conditional Constructivity. - Matthias Baaz (Algebraic and Proof-theoretic Aspects of Non-classical Logics, 2006)

Completeness of a Hypersequent Calculus for Some First-order Godel Logics with Delta. - Matthias Baaz; Norbert Preining; Richard Zach (ISMVL, 2006)

Proof Transformation by CERES. - Matthias Baaz; Stefan Hetzl; Alexander Leitsch; Clemens Richter; Hendrik Spohr (MKM, 2006)

Herbrand's theorem and term induction. - Matthias Baaz; Georg Moser (Arch. Math. Log., 2006)

The Skolemization of existential quantifiers in intuitionistic logic. - Matthias Baaz; Rosalie Iemhoff (Ann. Pure Appl. Log., 2006)

Towards a clausal analysis of cut-elimination. - Matthias Baaz; Alexander Leitsch (J. Symb. Comput., 2006)

Gentzen Calculi for the Existence Predicate. - Matthias Baaz; Rosalie Iemhoff (Stud Logica, 2006)

Monadic Fragments of Gödel Logics: Decidability and Undecidability Results. - Matthias Baaz; Agata Ciabattoni; Christian G. Fermüller (LPAR, 2007)

Proof Theory for First Order Lukasiewicz Logic. - Matthias Baaz; George Metcalfe (TABLEAUX, 2007)

First-order Gödel logics. - Matthias Baaz; Norbert Preining; Richard Zach (Ann. Pure Appl. Log., 2007)

Effective Finite-Valued Approximations of General Propositional Logics. - Matthias Baaz; Richard Zach (Pillars of Computer Science, 2008)

Herbrand Theorems and Skolemization for Prenex Fuzzy Logics. - Matthias Baaz; George Metcalfe (CiE, 2008)

Cut Elimination for First Order Gödel Logic by Hyperclause Resolution. - Matthias Baaz; Agata Ciabattoni; Christian G. Fermüller (LPAR, 2008)

Generalizing proofs in monadic languages. - Matthias Baaz; Piotr Wojtylak (Ann. Pure Appl. Log., 2008)

On Skolemization in constructive theories. - Matthias Baaz; Rosalie Iemhoff (J. Symb. Log., 2008)

Quantifier Elimination for Quantified Propositional Logics on Kripke Frames of Type omega. - Matthias Baaz; Norbert Preining (J. Log. Comput., 2008)

CERES: An analysis of Fürstenberg's proof of the infinity of primes. - Matthias Baaz; Stefan Hetzl; Alexander Leitsch; Clemens Richter; Hendrik Spohr (Theor. Comput. Sci., 2008)

SAT in Monadic Gödel Logics: A Borderline between Decidability and Undecidability. - Matthias Baaz; Agata Ciabattoni; Norbert Preining (WoLLIC, 2009)

Foreword. - Matthias Baaz (Ann. Pure Appl. Log., 2009)

Note on witnessed Gödel logics with Delta. - Matthias Baaz; Oliver Fasching (Ann. Pure Appl. Log., 2009)

Fuzzy Logic Corner. - Matthias Baaz; George Metcalfe (J. Log. Comput., 2009)

A Resolution Mechanism for Prenex Gödel Logic. - Matthias Baaz; Christian G. Fermüller (CSL, 2010)

Gödel logics with an operator shifting truth values. - Matthias Baaz; Oliver Fasching (LPAR short papers(Yogyakarta), 2010)

Herbrand's Theorem, Skolemization and Proof Systems for First-Order Lukasiewicz Logic. - Matthias Baaz; George Metcalfe (J. Log. Comput., 2010)

On the non-confluence of cut-elimination. - Matthias Baaz; Stefan Hetzl (J. Symb. Log., 2011)

Eskolemization in Intuitionistic Logic. - Matthias Baaz; Rosalie Iemhoff (J. Log. Comput., 2011)

First-order satisfiability in Gödel logics: An NP-complete fragment. - Matthias Baaz; Agata Ciabattoni; Norbert Preining (Theor. Comput. Sci., 2011)

Effective Finite-Valued Semantics for Labelled Calculi. - Matthias Baaz; Ori Lahav 001; Anna Zamansky (IJCAR, 2012)

Theorem proving for prenex Gödel logic with Delta: checking validity and unsatisfiability - Matthias Baaz; Agata Ciabattoni; Christian G. Fermüller (Log. Methods Comput. Sci., 2012)

Gödel logics with monotone operators. - Matthias Baaz; Oliver Fasching (Fuzzy Sets Syst., 2012)

On the complexity of proof deskolemization. - Matthias Baaz; Stefan Hetzl; Daniel Weller 001 (J. Symb. Log., 2012)

Finite-valued Semantics for Canonical Labelled Calculi. - Matthias Baaz; Ori Lahav 001; Anna Zamansky (J. Autom. Reason., 2013)

Vienna Summer of Logic. - Matthias Baaz; Thomas Eiter; Helmut Veith (KR, 2014)

Monotone operators on Gödel logic. - Oliver Fasching; Matthias Baaz (Arch. Math. Log., 2014)

Cut-Elimination: Syntax and Semantics. - Matthias Baaz; Alexander Leitsch (Stud Logica, 2014)

Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic. - Matthias Baaz; Christian G. Fermüller (CSL, 2015)

A Note on the Complexity of Classical and Intuitionistic Proofs. - Matthias Baaz; Alexander Leitsch; Giselle Reis (LICS, 2015)

Cut Elimination for Gödel Logic with an Operator Adding a Constant. - Juan P. Aguilera 001; Matthias Baaz (WoLLIC, 2016)

Skolemization in intermediate logics with the finite model property. - Matthias Baaz; Rosalie Iemhoff (Log. J. IGPL, 2016)

Proof theory of witnessed Gödel logic: A negative result. - Matthias Baaz; Agata Ciabattoni (J. Log. Comput., 2016)

First-Order Interpolation of Non-classical Logics Derived from Propositional Interpolation. - Matthias Baaz; Anela Lolic (FroCoS, 2017)

Gödel logics and the fully boxed fragment of LTL. - Matthias Baaz; Norbert Preining (LPAR, 2017)

Preface. - Matthias Baaz (FLAP, 2017)

On the Complexity of Translations from Classical to Intuitionistic Proofs. - Matthias Baaz; Alexander Leitsch (FLAP, 2017)

Preface. - Matthias Baaz; Agata Ciabattoni; Dov M. Gabbay; Stefan Hetzl; Daniel Weller 001 (J. Log. Comput., 2017)

Ten problems in Gödel logic. - Juan P. Aguilera 001; Matthias Baaz (Soft Comput., 2017)

A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem. - Matthias Baaz; Alexander Leitsch; Anela Lolic (LFCS, 2018)

Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic. - Matthias Baaz; Anela Lolic (LPAR, 2018)

Note on Globally Sound Analytic Calculi for Quantifier Macros. - Matthias Baaz; Anela Lolic (WoLLIC, 2019)

On the classification of first order Gödel logics. - Matthias Baaz; Norbert Preining (Ann. Pure Appl. Log., 2019)

Unsound Inferences Make Proofs Shorter. - Juan P. Aguilera 001; Matthias Baaz (J. Symb. Log., 2019)

A Globally Sound Analytic Calculus for Henkin Quantifiers. - Matthias Baaz; Anela Lolic (LFCS, 2020)

An abstract form of the first epsilon theorem. - Matthias Baaz; Alexander Leitsch; Anela Lolic (J. Log. Comput., 2020)

First-order interpolation derived from propositional interpolation. - Matthias Baaz; Anela Lolic (Theor. Comput. Sci., 2020)

Towards a proof theory for Henkin quantifiers. - Matthias Baaz; Anela Lolic (J. Log. Comput., 2021)

Andrews Skolemization May Shorten Resolution Proofs Non-elementarily. - Matthias Baaz; Anela Lolic (LFCS, 2022)

The number of axioms. - Juan P. Aguilera 001; Matthias Baaz; Jan Bydzovsky (Ann. Pure Appl. Log., 2022)

Towards a proof theory for quantifier macros. - Matthias Baaz; Anela Lolic (Inf. Comput., 2022)

Epsilon theorems in Intermediate Logics. - Matthias Baaz; Richard Zach (J. Symb. Log., 2022)

Effective Skolemization. - Matthias Baaz; Anela Lolic (WoLLIC, 2023)

On Translations of Epsilon Proofs to LK. - Matthias Baaz; Anela Lolic (LPAR, 2024)

Goedel logics: Prenex fragments. - Matthias Baaz; Mariami Gamsakhurdia (CoRR, 2024)

90 years of Gödel's incompleteness theorems: Logic and computation. - Matthias Baaz; Marcel Ertel; Reinhard Kahle; Thomas Piecha; Jan von Plato (J. Log. Comput., 2024)

Skolemization In Intermediate Logics. - Matthias Baaz; Mariami Gamsakhurdia; Rosalie Iemhoff; Raheleh Jalali (CoRR, 2025)