Matthias Baaz

Mariami Gamsakhurdia

CoRR, 2024

On Translations of Epsilon Proofs to LK.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2024: Proceedings of 25th Conference on Logic for Programming, 2024

2023

Effective Skolemization.

[BibT_eX]

[DOI]

Proceedings of the Logic, Language, Information, and Computation, 2023

2022

Epsilon theorems in Intermediate Logics.

[BibT_eX]

[DOI]

J. Symb. Log., 2022

Towards a proof theory for quantifier macros.

[BibT_eX]

[DOI]

Inf. Comput., 2022

The number of axioms.

[BibT_eX]

[DOI]

Jan Bydzovsky

Ann. Pure Appl. Log., 2022

Andrews Skolemization May Shorten Resolution Proofs Non-elementarily.

[BibT_eX]

[DOI]

Proceedings of the Logical Foundations of Computer Science - International Symposium, 2022

2021

Towards a proof theory for Henkin quantifiers.

[BibT_eX]

[DOI]

J. Log. Comput., 2021

2020

First-order interpolation derived from propositional interpolation.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2020

An abstract form of the first epsilon theorem.

[BibT_eX]

[DOI]

J. Log. Comput., 2020

A Globally Sound Analytic Calculus for Henkin Quantifiers.

[BibT_eX]

[DOI]

Proceedings of the Logical Foundations of Computer Science - International Symposium, 2020

2019

Unsound Inferences Make Proofs Shorter.

[BibT_eX]

[DOI]

J. Symb. Log., 2019

On the classification of first order Gödel logics.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2019

Note on Globally Sound Analytic Calculi for Quantifier Macros.

[BibT_eX]

[DOI]

Proceedings of the Logic, Language, Information, and Computation, 2019

2018

Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic.

[BibT_eX]

[DOI]

Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem.

[BibT_eX]

[DOI]

Proceedings of the Logical Foundations of Computer Science - International Symposium, 2018

2017

Ten problems in Gödel logic.

[BibT_eX]

[DOI]

Soft Comput., 2017

Preface.

[BibT_eX]

[DOI]

J. Log. Comput., 2017

On the Complexity of Translations from Classical to Intuitionistic Proofs.

[BibT_eX]

[DOI]

FLAP, 2017

Preface.

[BibT_eX]

[DOI]

FLAP, 2017

Gödel logics and the fully boxed fragment of LTL.

[BibT_eX]

[DOI]

Proceedings of the LPAR-21, 2017

First-Order Interpolation of Non-classical Logics Derived from Propositional Interpolation.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

2016

Proof theory of witnessed Gödel logic: A negative result.

[BibT_eX]

[DOI]

J. Log. Comput., 2016

Skolemization in intermediate logics with the finite model property.

[BibT_eX]

[DOI]

Log. J. IGPL, 2016

Cut Elimination for Gödel Logic with an Operator Adding a Constant.

[BibT_eX]

[DOI]

Proceedings of the Logic, Language, Information, and Computation, 2016

2015

A Note on the Complexity of Classical and Intuitionistic Proofs.

[BibT_eX]

[DOI]

Giselle Reis

Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic.

[BibT_eX]

[DOI]

Proceedings of the 24th EACSL Annual Conference on Computer Science Logic, 2015

2014

Cut-Elimination: Syntax and Semantics.

[BibT_eX]

[DOI]

Stud Logica, 2014

Monotone operators on Gödel logic.

[BibT_eX]

[DOI]

Arch. Math. Log., 2014

Vienna Summer of Logic.

[BibT_eX]

[DOI]

Thomas Eiter

Proceedings of the Principles of Knowledge Representation and Reasoning: Proceedings of the Fourteenth International Conference, 2014

2013

Finite-valued Semantics for Canonical Labelled Calculi.

[BibT_eX]

[DOI]

Ori Lahav

Anna Zamansky

J. Autom. Reason., 2013

2012

On the complexity of proof deskolemization.

[BibT_eX]

[DOI]

Stefan Hetzl

Daniel Weller

J. Symb. Log., 2012

Gödel logics with monotone operators.

[BibT_eX]

[DOI]

Fuzzy Sets Syst., 2012

Theorem proving for prenex Gödel logic with Delta: checking validity and unsatisfiability

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2012

Effective Finite-Valued Semantics for Labelled Calculi.

[BibT_eX]

[DOI]

Ori Lahav

Anna Zamansky

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011

First-order satisfiability in Gödel logics: An NP-complete fragment.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2011

Eskolemization in Intuitionistic Logic.

[BibT_eX]

[DOI]

J. Log. Comput., 2011

On the non-confluence of cut-elimination.

[BibT_eX]

[DOI]

Stefan Hetzl

J. Symb. Log., 2011

2010

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

[BibT_eX]

[DOI]

J. Log. Comput., 2010

Gödel logics with an operator shifting truth values.

[BibT_eX]

[DOI]

Proceedings of the Short papers for 17th International Conference on Logic for Programming, 2010

A Resolution Mechanism for Prenex Gödel Logic.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 24th International Workshop, 2010

2009

Fuzzy Logic Corner.

[BibT_eX]

[DOI]

J. Log. Comput., 2009

Note on witnessed Gödel logics with Delta.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2009

Foreword.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2009

SAT in Monadic Gödel Logics: A Borderline between Decidability and Undecidability.

[BibT_eX]

[DOI]

Proceedings of the Logic, 2009

2008

CERES: An analysis of Fürstenberg's proof of the infinity of primes.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2008

Quantifier Elimination for Quantified Propositional Logics on Kripke Frames of Type omega.

[BibT_eX]

[DOI]

J. Log. Comput., 2008

On Skolemization in constructive theories.

[BibT_eX]

[DOI]

J. Symb. Log., 2008

Generalizing proofs in monadic languages.

[BibT_eX]

[DOI]

Piotr Wojtylak

Ann. Pure Appl. Log., 2008

Cut Elimination for First Order Gödel Logic by Hyperclause Resolution.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2008

Herbrand Theorems and Skolemization for Prenex Fuzzy Logics.

[BibT_eX]

[DOI]

Proceedings of the Logic and Theory of Algorithms, 2008

Effective Finite-Valued Approximations of General Propositional Logics.

[BibT_eX]

[DOI]

Proceedings of the Pillars of Computer Science, 2008

2007

First-order Gödel logics.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2007

Proof Theory for First Order Lukasiewicz Logic.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2007

Monadic Fragments of Gödel Logics: Decidability and Undecidability Results.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2007

2006

Gentzen Calculi for the Existence Predicate.

[BibT_eX]

[DOI]

Stud Logica, 2006

Towards a clausal analysis of cut-elimination.

[BibT_eX]

[DOI]

J. Symb. Comput., 2006

The Skolemization of existential quantifiers in intuitionistic logic.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2006

Herbrand's theorem and term induction.

[BibT_eX]

[DOI]

Arch. Math. Log., 2006

Proof Transformation by CERES.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Knowledge Management, 5th International Conference, 2006

Completeness of a Hypersequent Calculus for Some First-order Godel Logics with Delta.

[BibT_eX]

[DOI]

Proceedings of the 36th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2006), 2006

Note on Conditional Constructivity.

[BibT_eX]

[DOI]

Proceedings of the Algebraic and Proof-theoretic Aspects of Non-classical Logics, 2006

2005

Editorial.

[BibT_eX]

[DOI]

Sergei I. Adian

Lev D. Beklemishev

J. Log. Comput., 2005

Editorial.

[BibT_eX]

[DOI]

Log. J. IGPL, 2005

Controlling witnesses.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2005

On Interpolation in Existence Logics.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2005

Note on Formal Analogical Reasoning in the Juridical Context.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 19th International Workshop, 2005

On the Proof Theory of the Existence Predicate.

[BibT_eX]

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.

[BibT_eX]

[DOI]

Franco Montagna

Fundam. Informaticae, 2004

CERES in Many-Valued Logics.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2004

Cut-Elimination: Experiments with CERES.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2004

2003

Hypersequent Calculi for Gödel Logics - a Survey.

[BibT_eX]

[DOI]

J. Log. Comput., 2003

A Translation Characterizing the Constructive Content of Classical Theories.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2003

Characterization of the Axiomatizable Prenex Fragments of First-Order Gödel Logics.

[BibT_eX]

[DOI]

Proceedings of the 33rd IEEE International Symposium on Multiple-Valued Logic (ISMVL 2003), 2003

2002

Foreword.

[BibT_eX]

[DOI]

Georg Gottlob

Theor. Comput. Sci., 2002

A Schütte-Tait Style Cut-Elimination Proof for First-Order Gödel Logic.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2002

Proof Analysis by Resolution.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2002

On Generalizations of Semi-terms of Particularly Simple Form.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 16th International Workshop, 2002

2001

Complexity of t-tautologies.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2001

Herbrand's Theorem for Prenex Gödel Logic and its Consequences for Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2001

Cut-Elimination in a Sequents-of-Relations Calculus for Gödel Logic.

[BibT_eX]

[DOI]

Proceedings of the 31st IEEE International Symposium on Multiple-Valued Logic, 2001

Comparing the Complexity of Cut-Elimination Methods.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Proof Theory in Computer Science, International Seminar, 2001

On a Generalisation of Herbrand's Theorem.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 15th International Workshop, 2001

Automated Deduction for Many-Valued Logics.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

Normal Form Transformations.

[BibT_eX]

[DOI]

Uwe Egly

Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

2000

Cut-elimination and Redundancy-elimination by Resolution.

[BibT_eX]

[DOI]

J. Symb. Comput., 2000

An Analytic Calculus for Quantified Propositional Gödel Logic.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2000

Quantified Propositional Gödel Logics.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming and Automated Reasoning, 2000

Hypersequent and the Proof Theory of Intuitionistic Fuzzy Logic.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 2000

1999

Note on the Generalization of Calculations.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1999

Cut Normal Forms and Proof Complexity.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1999

Interpolation in fuzzy logic.

[BibT_eX]

[DOI]

Arch. Math. Log., 1999

Analytic Calculi for Projective Logics.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1999

On the Undecidability of some Sub-Classical First-Order Logics.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1999

System Description: CutRes 0.1: Cut Elimination by Resolution.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1999

1998

Embedding Logics into Product Logic.

[BibT_eX]

[DOI]

Stud Logica, 1998

Labeled Calculi and Finite-Valued Logics.

[BibT_eX]

[DOI]

Stud Logica, 1998

Note on generalizing theorems in algebraically closed fields.

[BibT_eX]

[DOI]

Arch. Math. Log., 1998

Proof Theory of Fuzzy Logics: Urquhart's C and Related Logics.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 1998, 1998

Compact Propositional Gödel Logics.

[BibT_eX]

[DOI]

Proceedings of the 28th IEEE International Symposium on Multiple-Valued Logic, 1998

Quantifier Elimination in Fuzzy Logic.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 12th International Workshop, 1998

1997

Lean Induction Principles for Tableaux.

[BibT_eX]

[DOI]

Uwe Egly

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1997

1996

Completeness of a First-Order Temporal Logic with Time-Gaps.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1996

The Axiom of Choice in Quantum Theory.

[BibT_eX]

[DOI]

Norbert Brunner

Karl Svozil

Math. Log. Q., 1996

Combining Many-valued and Intuitionistic Tableaux.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving with Analytic Tableaux and Related Methods, 1996

Intuitionistic Counterparts of Finitely-Valued Logics.

[BibT_eX]

[DOI]

Proceedings of the 26th IEEE International Symposium on Multiple-Valued Logic, 1996

Fast Cut-Elimination by Projection.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 10th International Workshop, 1996

MUltlog 1.0: Towards an Expert System for Many-Valued Logics.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

J. Symb. Comput., 1995

Generalizing Theorems in Real Closed Fields.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1995

Non-elementary Speedups between Different Versions of Tableaux.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 9th International Workshop, 1995

1994

On Skolemization and Proof Complexity.

[BibT_eX]

[DOI]

Fundam. Informaticae, 1994

A Non-Elementary Speed-Up in Proof Length by Structural Clause Form Transformation

[BibT_eX]

[DOI]

Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

A New Frame For Common-Sense Reasoning - Towards Local Inconsistencies.

[BibT_eX]

[DOI]

Karin Hörwein

Proceedings of the KI-94: Advances in Artificial Intelligence, 1994

Approximating Propositional Calculi by Finite-Valued Logics.

[BibT_eX]

[DOI]

Proceedings of the 24th IEEE International Symposium on Multiple-Valued Logic, 1994

Semi-Unification and Generalizations of a Particularly Simple Form.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 8th International Workshop, 1994

1993

Elimination of Cuts in First-order Finite-valued Logics.

[BibT_eX]

J. Inf. Process. Cybern., 1993

Dual systems of sequents and tableaux for many-valued logics.

[BibT_eX]

Bull. EATCS, 1993

MULTILOG: A System for Axiomatizing Many-valued Logics.

[BibT_eX]

[DOI]

Arie Ovrutcki

Proceedings of the Logic Programming and Automated Reasoning,4th International Conference, 1993

Systematic Construction of Natural Deduction Systems for Many-Valued Logics.

[BibT_eX]

[DOI]

Proceedings of the 23rd IEEE International Symposium on Multiple-Valued Logic, 1993

The Application of Kripke-Type Structures to Regional Development Programs.

[BibT_eX]

[DOI]

Proceedings of the Database and Expert Systems Applications, 4th International Conference, 1993

Short Proofs of Tautologies Using the Schema of Equivalence.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 7th Workshop, 1993

1992

Note on calculi for a three-valued logic for logic programming..

[BibT_eX]

Bull. EATCS, 1992

Complexity of Resolution Proofs and Function Introduction.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1992

Resolution for Many-Valued Logics.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming and Automated Reasoning, 1992

Algorithmic Structuring of Cut-free Proofs.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 6th Workshop, 1992

1991

A Formal Model for the Support of Analogical Reasoning in Legal Expert Systems.

[BibT_eX]

Gerald Quirchmayr

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.

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Symbolic and Algebraic Computation, 1990

1989

An Effective Decision Algorithm for Propositional Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the 5. Österreichische Artificial Intelligence-Tagung, 1989

1987

Automatisches Beweisen für Logiksysteme, in denen Widersprüche behandelt werden können.

[BibT_eX]

[DOI]

Proceedings of the 3. Österreichische Artificial Intelligence-Tagung, 1987

Strong splitting rules in automated theorem proving.

[BibT_eX]

[DOI]

Proceedings of the EUROCAL '87, 1987

1986

Kripke-type semantics for da Costa's paraconsistent logic C<sub>ω</sub>.

[BibT_eX]

[DOI]

Notre Dame J. Formal Log., 1986

1985

Eine Methode zur automatischen Problemreduktion.

[BibT_eX]

[DOI]