| Publication | Date of Publication | Type |
|---|
| Interpolation Results for Arrays with Length and MaxDiff | 2023-11-03 | Paper |
| Profiniteness, Monadicity and Universal Models in Modal Logic | 2023-05-08 | Paper |
| The Invariance Modality | 2023-04-05 | Paper |
| Combined covers and Beth definability | 2022-11-09 | Paper |
| Combination of uniform interpolants via Beth definability | 2022-10-24 | Paper |
| Admissibility of \(\Pi_2\)-inference rules: interpolation, model completion, and contact algebras | 2022-10-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5104701 | 2022-09-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5094130 | 2022-08-02 | Paper |
| Admissibility of $\Pi_2$-Inference Rules: interpolation, model completion, and contact algebras | 2022-01-16 | Paper |
| Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) | 2021-11-24 | Paper |
| Interpolation and amalgamation for arrays with MaxDiff | 2021-10-18 | Paper |
| Higher-order quantifier elimination, counter simulations and fault-tolerant systems | 2021-06-09 | Paper |
| Diego's theorem for nuclear implicative semilattices | 2021-03-14 | Paper |
| Free Heyting algebra endomorphisms: Ruitenburg’s Theorem and beyond | 2020-12-08 | Paper |
| SMT-based verification of data-aware processes: a model-theoretic approach | 2020-12-08 | Paper |
| From model completeness to verification of data aware processes | 2020-06-04 | Paper |
| Model completeness, covers and superposition | 2020-03-10 | Paper |
| Fixed-point Elimination in the Intuitionistic Propositional Calculus | 2019-11-22 | Paper |
| Ruitenburg's Theorem via Duality and Bounded Bisimulations | 2019-07-24 | Paper |
| Free Heyting Algebra Endomorphisms: Ruitenburg's Theorem and Beyond | 2019-01-04 | Paper |
| Modularity results for interpolation, amalgamation and superamalgamation | 2018-06-05 | Paper |
| Monadic second order logic as the model companion of temporal logic | 2018-04-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4636285 | 2018-04-23 | Paper |
| Fixed-point elimination in the Intuitionistic Propositional Calculus (extended version) | 2018-03-05 | Paper |
| One-step Heyting Algebras and Hypersequent Calculi with the Bounded Proof Property | 2018-02-13 | Paper |
| Cardinality constraints for arrays (decidability results and applications) | 2018-01-08 | Paper |
| Interpolation, amalgamation and combination (the non-disjoint signatures case) | 2018-01-04 | Paper |
| A comprehensive combination framework | 2017-07-12 | Paper |
| A MODEL-THEORETIC CHARACTERIZATION OF MONADIC SECOND ORDER LOGIC ON INFINITE WORDS | 2017-06-01 | Paper |
| A New Acceleration-Based Combination Framework for Array Properties | 2017-02-27 | Paper |
| Counting Constraints in Flat Array Fragments | 2016-09-05 | Paper |
| Fixed-Point Elimination in the Intuitionistic Propositional Calculus | 2016-06-10 | Paper |
| Decision procedures for flat array properties | 2016-05-26 | Paper |
| Admissible bases via stable canonical rules | 2016-05-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2786907 | 2016-02-23 | Paper |
| Booster: An Acceleration-Based Verification Framework for Array Programs | 2015-12-17 | Paper |
| LTL over description logic axioms | 2015-09-17 | Paper |
| Free Modal Algebras Revisited: The Step-by-Step Method | 2015-06-19 | Paper |
| Unified Correspondence | 2015-05-11 | Paper |
| Light-Weight SMT-based Model Checking | 2015-03-18 | Paper |
| The logic of transitive and dense frames: from the step-frame analysis to full cut-elimination | 2015-02-12 | Paper |
| An extension of lazy abstraction with interpolation for programs with arrays | 2014-12-05 | Paper |
| The bounded proof property via step algebras and step frames | 2014-09-10 | Paper |
| Quantifier-free interpolation in combinations of equality interpolating theories | 2014-04-16 | Paper |
| Bounded Proofs and Step Frames | 2013-10-04 | Paper |
| Definability of Accelerated Relations in a Theory of Arrays and Its Applications | 2013-09-20 | Paper |
| AUTOMATED TERMINATION IN MODEL-CHECKING MODULO THEORIES | 2013-07-30 | Paper |
| Quantifier Elimination and Provers Integration | 2013-04-19 | Paper |
| From Strong Amalgamability to Modularity of Quantifier-Free Interpolation | 2012-09-05 | Paper |
| Continuity, freeness, and filtrations | 2012-07-17 | Paper |
| Lazy Abstraction with Interpolants for Arrays | 2012-06-15 | Paper |
| Unification in modal and description logics | 2012-06-08 | Paper |
| Quantifier-Free Interpolation of a Theory of Arrays | 2012-05-16 | Paper |
| Rewriting-based Quantifier-free Interpolation for a Theory of Arrays. | 2012-04-24 | Paper |
| Automated Termination in Model Checking Modulo Theories | 2011-10-07 | Paper |
| A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints | 2011-10-07 | Paper |
| An algebraic approach to subframe logics. Modal case | 2011-06-03 | Paper |
| Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis | 2011-03-08 | Paper |
| MCMT: A Model Checker Modulo Theories | 2010-09-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3408136 | 2010-02-24 | Paper |
| Goal-Directed Invariant Synthesis for Model Checking Modulo Theories | 2009-12-01 | Paper |
| Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures | 2009-03-12 | Paper |
| Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems | 2009-03-06 | Paper |
| Towards SMT Model Checking of Array-Based Systems | 2008-11-27 | Paper |
| Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies | 2008-10-30 | Paper |
| Noetherianity and Combination Problems | 2008-09-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3509053 | 2008-07-01 | Paper |
| Decision procedures for extensions of the theory of arrays | 2007-10-23 | Paper |
| Automated Reasoning | 2007-09-25 | Paper |
| Connecting many-sorted theories | 2007-07-09 | Paper |
| An algebraic approach to subframe logics. Intuitionistic case | 2007-06-25 | Paper |
| Automated Deduction – CADE-20 | 2006-11-01 | Paper |
| A new combination procedure for the word problem that generalizes fusion decidability results in modal logics | 2006-10-25 | Paper |
| Frontiers of Combining Systems | 2006-10-10 | Paper |
| Frontiers of Combining Systems | 2006-10-10 | Paper |
| Filtering unification and most general unifiers in modal logic | 2005-08-29 | Paper |
| Model-theoretic methods in combined constraint satisfiability | 2005-06-22 | Paper |
| Unification, finite duality and projectivity in varieties of Heyting algebras | 2004-08-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4430400 | 2003-10-09 | Paper |
| Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics | 2003-09-08 | Paper |
| Combining word problems through rewriting in categories with products | 2003-07-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4793390 | 2003-06-21 | Paper |
| A Resolution/Tableaux Algorithm for Projective Approximations in IPC | 2003-02-25 | Paper |
| On canonicity and strong completeness conditions in intermediate propositional logics | 2001-03-19 | Paper |
| Constructive canonicity in non-classical logics | 2000-12-06 | Paper |
| Best solving modal equations | 2000-12-06 | Paper |
| Unification in intuitionistic logic | 1999-09-12 | Paper |
| Model completions and r-Heyting categories | 1998-05-11 | Paper |
| Unification through projectivity | 1998-03-25 | Paper |
| Relational and partial variable sets and basic predicate logic | 1997-04-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4873970 | 1996-09-16 | Paper |
| A sheaf representation and duality for finitely presented Heyting algebras | 1996-05-13 | Paper |
| Undefinability of propositional quantifiers in the modal system S4 | 1996-02-07 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4845311 | 1995-12-13 | Paper |
| An algebraic theory of normal forms | 1995-03-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4277651 | 1994-02-07 | Paper |
| Quantified extensions of canonical propositional intermediate logics | 1993-04-01 | Paper |
| Incompleteness results in Kripke semantics | 1992-06-27 | Paper |
| Modal logics withn-ary connectives | 1990-01-01 | Paper |
| Presheaf semantics and independence results for some non-classical first- order logics | 1989-01-01 | Paper |
| Directed frames | 1989-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3351360 | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3804674 | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3731600 | 1986-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3754618 | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4726226 | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4726227 | 1985-01-01 | Paper |
