Matthias Baaz

Orcid: 0000-0002-7815-2501

According to our database1, Matthias Baaz authored at least 135 papers between 1985 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

On csauthors.net:

Bibliography

2024
Goedel logics: Prenex fragments.
CoRR, 2024

On Translations of Epsilon Proofs to LK.
Proceedings of the LPAR 2024: Proceedings of 25th Conference on Logic for Programming, 2024

2023
Effective Skolemization.
Proceedings of the Logic, Language, Information, and Computation, 2023

2022
Epsilon theorems in Intermediate Logics.
J. Symb. Log., 2022

Towards a proof theory for quantifier macros.
Inf. Comput., 2022

The number of axioms.
Ann. Pure Appl. Log., 2022

Andrews Skolemization May Shorten Resolution Proofs Non-elementarily.
Proceedings of the Logical Foundations of Computer Science - International Symposium, 2022

2021
Towards a proof theory for Henkin quantifiers.
J. Log. Comput., 2021

2020
First-order interpolation derived from propositional interpolation.
Theor. Comput. Sci., 2020

An abstract form of the first epsilon theorem.
J. Log. Comput., 2020

A Globally Sound Analytic Calculus for Henkin Quantifiers.
Proceedings of the Logical Foundations of Computer Science - International Symposium, 2020

2019
Unsound Inferences Make Proofs Shorter.
J. Symb. Log., 2019

On the classification of first order Gödel logics.
Ann. Pure Appl. Log., 2019

Note on Globally Sound Analytic Calculi for Quantifier Macros.
Proceedings of the Logic, Language, Information, and Computation, 2019

2018
Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic.
Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem.
Proceedings of the Logical Foundations of Computer Science - International Symposium, 2018

2017
Ten problems in Gödel logic.
Soft Comput., 2017

Preface.
J. Log. Comput., 2017

On the Complexity of Translations from Classical to Intuitionistic Proofs.
FLAP, 2017

Preface.
FLAP, 2017

Gödel logics and the fully boxed fragment of LTL.
Proceedings of the LPAR-21, 2017

First-Order Interpolation of Non-classical Logics Derived from Propositional Interpolation.
Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

2016
Proof theory of witnessed Gödel logic: A negative result.
J. Log. Comput., 2016

Skolemization in intermediate logics with the finite model property.
Log. J. IGPL, 2016

Cut Elimination for Gödel Logic with an Operator Adding a Constant.
Proceedings of the Logic, Language, Information, and Computation, 2016

2015
A Note on the Complexity of Classical and Intuitionistic Proofs.
Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic.
Proceedings of the 24th EACSL Annual Conference on Computer Science Logic, 2015

2014
Cut-Elimination: Syntax and Semantics.
Stud Logica, 2014

Monotone operators on Gödel logic.
Arch. Math. Log., 2014

Vienna Summer of Logic.
Proceedings of the Principles of Knowledge Representation and Reasoning: Proceedings of the Fourteenth International Conference, 2014

2013
Finite-valued Semantics for Canonical Labelled Calculi.
J. Autom. Reason., 2013

2012
On the complexity of proof deskolemization.
J. Symb. Log., 2012

Gödel logics with monotone operators.
Fuzzy Sets Syst., 2012

Theorem proving for prenex Gödel logic with Delta: checking validity and unsatisfiability
Log. Methods Comput. Sci., 2012

Effective Finite-Valued Semantics for Labelled Calculi.
Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011
First-order satisfiability in Gödel logics: An NP-complete fragment.
Theor. Comput. Sci., 2011

Eskolemization in Intuitionistic Logic.
J. Log. Comput., 2011

On the non-confluence of cut-elimination.
J. Symb. Log., 2011

2010
Herbrand's Theorem, Skolemization and Proof Systems for First-Order Lukasiewicz Logic.
J. Log. Comput., 2010

Gödel logics with an operator shifting truth values.
Proceedings of the Short papers for 17th International Conference on Logic for Programming, 2010

A Resolution Mechanism for Prenex Gödel Logic.
Proceedings of the Computer Science Logic, 24th International Workshop, 2010

2009
Fuzzy Logic Corner.
J. Log. Comput., 2009

Note on witnessed Gödel logics with Delta.
Ann. Pure Appl. Log., 2009

Foreword.
Ann. Pure Appl. Log., 2009

SAT in Monadic Gödel Logics: A Borderline between Decidability and Undecidability.
Proceedings of the Logic, 2009

2008
CERES: An analysis of Fürstenberg's proof of the infinity of primes.
Theor. Comput. Sci., 2008

Quantifier Elimination for Quantified Propositional Logics on Kripke Frames of Type omega.
J. Log. Comput., 2008

On Skolemization in constructive theories.
J. Symb. Log., 2008

Generalizing proofs in monadic languages.
Ann. Pure Appl. Log., 2008

Cut Elimination for First Order Gödel Logic by Hyperclause Resolution.
Proceedings of the Logic for Programming, 2008

Herbrand Theorems and Skolemization for Prenex Fuzzy Logics.
Proceedings of the Logic and Theory of Algorithms, 2008

Effective Finite-Valued Approximations of General Propositional Logics.
Proceedings of the Pillars of Computer Science, 2008

2007
First-order Gödel logics.
Ann. Pure Appl. Log., 2007

Proof Theory for First Order Lukasiewicz Logic.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2007

Monadic Fragments of Gödel Logics: Decidability and Undecidability Results.
Proceedings of the Logic for Programming, 2007

2006
Gentzen Calculi for the Existence Predicate.
Stud Logica, 2006

Towards a clausal analysis of cut-elimination.
J. Symb. Comput., 2006

The Skolemization of existential quantifiers in intuitionistic logic.
Ann. Pure Appl. Log., 2006

Herbrand's theorem and term induction.
Arch. Math. Log., 2006

Proof Transformation by CERES.
Proceedings of the Mathematical Knowledge Management, 5th International Conference, 2006

Completeness of a Hypersequent Calculus for Some First-order Godel Logics with Delta.
Proceedings of the 36th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2006), 2006

Note on Conditional Constructivity.
Proceedings of the Algebraic and Proof-theoretic Aspects of Non-classical Logics, 2006

2005
Editorial.
J. Log. Comput., 2005

Editorial.
Log. J. IGPL, 2005

Controlling witnesses.
Ann. Pure Appl. Log., 2005

On Interpolation in Existence Logics.
Proceedings of the Logic for Programming, 2005

Note on Formal Analogical Reasoning in the Juridical Context.
Proceedings of the Computer Science Logic, 19th International Workshop, 2005

On the Proof Theory of the Existence Predicate.
Proceedings of the We Will Show Them! Essays in Honour of Dov Gabbay, Volume One, 2005

2004
Analytic Calculi for Monoidal T-norm Based Logic.
Fundam. Informaticae, 2004

CERES in Many-Valued Logics.
Proceedings of the Logic for Programming, 2004

Cut-Elimination: Experiments with CERES.
Proceedings of the Logic for Programming, 2004

2003
Hypersequent Calculi for Gödel Logics - a Survey.
J. Log. Comput., 2003

A Translation Characterizing the Constructive Content of Classical Theories.
Proceedings of the Logic for Programming, 2003

Characterization of the Axiomatizable Prenex Fragments of First-Order Gödel Logics.
Proceedings of the 33rd IEEE International Symposium on Multiple-Valued Logic (ISMVL 2003), 2003

2002
Foreword.
Theor. Comput. Sci., 2002

A Schütte-Tait Style Cut-Elimination Proof for First-Order Gödel Logic.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2002

Proof Analysis by Resolution.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2002

On Generalizations of Semi-terms of Particularly Simple Form.
Proceedings of the Computer Science Logic, 16th International Workshop, 2002

2001
Complexity of t-tautologies.
Ann. Pure Appl. Log., 2001

Herbrand's Theorem for Prenex Gödel Logic and its Consequences for Theorem Proving.
Proceedings of the Logic for Programming, 2001

Cut-Elimination in a Sequents-of-Relations Calculus for Gödel Logic.
Proceedings of the 31st IEEE International Symposium on Multiple-Valued Logic, 2001

Comparing the Complexity of Cut-Elimination Methods.
Proceedings of the Proof Theory in Computer Science, International Seminar, 2001

A Note on the Proof-Theoretic Strength of a Single Application of the Schema of Identity.
Proceedings of the Proof Theory in Computer Science, International Seminar, 2001

On a Generalisation of Herbrand's Theorem.
Proceedings of the Computer Science Logic, 15th International Workshop, 2001

Automated Deduction for Many-Valued Logics.
Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

Normal Form Transformations.
Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

2000
Cut-elimination and Redundancy-elimination by Resolution.
J. Symb. Comput., 2000

An Analytic Calculus for Quantified Propositional Gödel Logic.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2000

Quantified Propositional Gödel Logics.
Proceedings of the Logic for Programming and Automated Reasoning, 2000

Hypersequent and the Proof Theory of Intuitionistic Fuzzy Logic.
Proceedings of the Computer Science Logic, 2000

1999
Note on the Generalization of Calculations.
Theor. Comput. Sci., 1999

Cut Normal Forms and Proof Complexity.
Ann. Pure Appl. Log., 1999

Interpolation in fuzzy logic.
Arch. Math. Log., 1999

Analytic Calculi for Projective Logics.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1999

On the Undecidability of some Sub-Classical First-Order Logics.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1999

System Description: CutRes 0.1: Cut Elimination by Resolution.
Proceedings of the Automated Deduction, 1999

1998
Embedding Logics into Product Logic.
Stud Logica, 1998

Labeled Calculi and Finite-Valued Logics.
Stud Logica, 1998

Note on generalizing theorems in algebraically closed fields.
Arch. Math. Log., 1998

Proof Theory of Fuzzy Logics: Urquhart's C and Related Logics.
Proceedings of the Mathematical Foundations of Computer Science 1998, 1998

Compact Propositional Gödel Logics.
Proceedings of the 28th IEEE International Symposium on Multiple-Valued Logic, 1998

Quantifier Elimination in Fuzzy Logic.
Proceedings of the Computer Science Logic, 12th International Workshop, 1998

1997
Lean Induction Principles for Tableaux.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1997

1996
Completeness of a First-Order Temporal Logic with Time-Gaps.
Theor. Comput. Sci., 1996

The Axiom of Choice in Quantum Theory.
Math. Log. Q., 1996

Combining Many-valued and Intuitionistic Tableaux.
Proceedings of the Theorem Proving with Analytic Tableaux and Related Methods, 1996

Intuitionistic Counterparts of Finitely-Valued Logics.
Proceedings of the 26th IEEE International Symposium on Multiple-Valued Logic, 1996

Fast Cut-Elimination by Projection.
Proceedings of the Computer Science Logic, 10th International Workshop, 1996

MUltlog 1.0: Towards an Expert System for Many-Valued Logics.
Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

1995
Resolution-Based Theorem Proving for Manyvalued Logics.
J. Symb. Comput., 1995

Generalizing Theorems in Real Closed Fields.
Ann. Pure Appl. Log., 1995

Non-elementary Speedups between Different Versions of Tableaux.
Proceedings of the Theorem Proving with Analytic Tableaux and Related Methods, 1995

Incompleteness of a First-Order Gödel Logic and Some Temporal Logics of Programs.
Proceedings of the Computer Science Logic, 9th International Workshop, 1995

1994
On Skolemization and Proof Complexity.
Fundam. Informaticae, 1994

A Non-Elementary Speed-Up in Proof Length by Structural Clause Form Transformation
Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

A New Frame For Common-Sense Reasoning - Towards Local Inconsistencies.
Proceedings of the KI-94: Advances in Artificial Intelligence, 1994

Approximating Propositional Calculi by Finite-Valued Logics.
Proceedings of the 24th IEEE International Symposium on Multiple-Valued Logic, 1994

Semi-Unification and Generalizations of a Particularly Simple Form.
Proceedings of the Computer Science Logic, 8th International Workshop, 1994

1993
Elimination of Cuts in First-order Finite-valued Logics.
J. Inf. Process. Cybern., 1993

Dual systems of sequents and tableaux for many-valued logics.
Bull. EATCS, 1993

MULTILOG: A System for Axiomatizing Many-valued Logics.
Proceedings of the Logic Programming and Automated Reasoning,4th International Conference, 1993

Systematic Construction of Natural Deduction Systems for Many-Valued Logics.
Proceedings of the 23rd IEEE International Symposium on Multiple-Valued Logic, 1993

The Application of Kripke-Type Structures to Regional Development Programs.
Proceedings of the Database and Expert Systems Applications, 4th International Conference, 1993

Short Proofs of Tautologies Using the Schema of Equivalence.
Proceedings of the Computer Science Logic, 7th Workshop, 1993

1992
Note on calculi for a three-valued logic for logic programming..
Bull. EATCS, 1992

Complexity of Resolution Proofs and Function Introduction.
Ann. Pure Appl. Log., 1992

Resolution for Many-Valued Logics.
Proceedings of the Logic Programming and Automated Reasoning, 1992

Algorithmic Structuring of Cut-free Proofs.
Proceedings of the Computer Science Logic, 6th Workshop, 1992

1991
A Formal Model for the Support of Analogical Reasoning in Legal Expert Systems.
Proceedings of the Proceedings of the International Conference on Database and Expert Systems Applications, 1991

1990
A Strong Problem Reduction Method Based on Function Introduction.
Proceedings of the International Symposium on Symbolic and Algebraic Computation, 1990

1989
An Effective Decision Algorithm for Propositional Temporal Logic.
Proceedings of the 5. Österreichische Artificial Intelligence-Tagung, 1989

1987
Automatisches Beweisen für Logiksysteme, in denen Widersprüche behandelt werden können.
Proceedings of the 3. Österreichische Artificial Intelligence-Tagung, 1987

Strong splitting rules in automated theorem proving.
Proceedings of the EUROCAL '87, 1987

1986
Kripke-type semantics for da Costa's paraconsistent logic C<sub>ω</sub>.
Notre Dame J. Formal Log., 1986

1985
Eine Methode zur automatischen Problemreduktion.
Proceedings of the Österreichische Artificial Intelligence-Tagung, 1985


  Loading...