| Publication | Date of Publication | Type |
|---|
Interpolation Results for Arrays with Length and MaxDiff
ACM Transactions on Computational Logic | 2023-11-03 | Paper |
Profiniteness, Monadicity and Universal Models in Modal Logic
| 2023-05-08 | Paper |
The Invariance Modality
Outstanding Contributions to Logic | 2023-04-05 | Paper |
Combined covers and Beth definability
| 2022-11-09 | Paper |
Combination of uniform interpolants via Beth definability
Journal of Automated Reasoning | 2022-10-24 | Paper |
Admissibility of \(\Pi_2\)-inference rules: interpolation, model completion, and contact algebras
Annals of Pure and Applied Logic | 2022-10-14 | Paper |
scientific article; zbMATH DE number 7585710 (Why is no real title available?)
| 2022-09-15 | Paper |
scientific article; zbMATH DE number 7566058 (Why is no real title available?)
| 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)
Journal of Automated Reasoning | 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
Journal of Automated Reasoning | 2021-06-09 | Paper |
Diego's theorem for nuclear implicative semilattices
Indagationes Mathematicae. New Series | 2021-03-14 | Paper |
Free Heyting algebra endomorphisms: Ruitenburg’s Theorem and beyond
Mathematical Structures in Computer Science | 2020-12-08 | Paper |
SMT-based verification of data-aware processes: a model-theoretic approach
Mathematical Structures in Computer Science | 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
ACM Transactions on Computational Logic | 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
Annals of Pure and Applied Logic | 2018-06-05 | Paper |
scientific article; zbMATH DE number 6863852 (Why is no real title available?)
| 2018-04-23 | Paper |
Monadic second order logic as the model companion of temporal logic
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science | 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
Journal Of Logic And Computation | 2018-02-13 | Paper |
Cardinality constraints for arrays (decidability results and applications)
Formal Methods in System Design | 2018-01-08 | Paper |
Interpolation, amalgamation and combination (the non-disjoint signatures case)
| 2018-01-04 | Paper |
A comprehensive combination framework
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
A model-theoretic characterization of monadic second order logic on infinite words
Journal of Symbolic Logic | 2017-06-01 | Paper |
A new acceleration-based combination framework for array properties
Frontiers of Combining Systems | 2017-02-27 | Paper |
Counting constraints in flat array fragments
Automated Reasoning | 2016-09-05 | Paper |
Fixed-Point Elimination in the Intuitionistic Propositional Calculus
Lecture Notes in Computer Science | 2016-06-10 | Paper |
Decision procedures for flat array properties
Journal of Automated Reasoning | 2016-05-26 | Paper |
Admissible bases via stable canonical rules
Studia Logica | 2016-05-17 | Paper |
Universal guards, relativization of quantifiers, and failure models in model checking modulo theories
Journal of Satisfiability, Boolean Modeling and Computation | 2016-02-23 | Paper |
Booster: an acceleration-based verification framework for array programs
Automated Technology for Verification and Analysis | 2015-12-17 | Paper |
LTL over description logic axioms
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Free modal algebras revisited: the step-by-step method
Leo Esakia on Duality in Modal and Intuitionistic Logics | 2015-06-19 | Paper |
Unified correspondence
Outstanding Contributions to Logic | 2015-05-11 | Paper |
Light-weight SMT-based model checking
Electronic Notes in Theoretical Computer Science | 2015-03-18 | Paper |
The logic of transitive and dense frames: from the step-frame analysis to full cut-elimination
Logic Journal of the IGPL | 2015-02-12 | Paper |
An extension of lazy abstraction with interpolation for programs with arrays
Formal Methods in System Design | 2014-12-05 | Paper |
The bounded proof property via step algebras and step frames
Annals of Pure and Applied Logic | 2014-09-10 | Paper |
Quantifier-free interpolation in combinations of equality interpolating theories
ACM Transactions on Computational Logic | 2014-04-16 | Paper |
Bounded proofs and step frames
Lecture Notes in Computer Science | 2013-10-04 | Paper |
Definability of accelerated relations in a theory of arrays and its applications
Frontiers of Combining Systems | 2013-09-20 | Paper |
Automated termination in model-checking modulo theories
International Journal of Foundations of Computer Science | 2013-07-30 | Paper |
Quantifier Elimination and Provers Integration
Electronic Notes in Theoretical Computer Science | 2013-04-19 | Paper |
From strong amalgamability to modularity of quantifier-free interpolation
Automated Reasoning | 2012-09-05 | Paper |
Continuity, freeness, and filtrations
Journal of Applied Non-Classical Logics | 2012-07-17 | Paper |
Lazy abstraction with interpolants for arrays
Logic for Programming, Artificial Intelligence, and Reasoning | 2012-06-15 | Paper |
Unification in modal and description logics
Logic Journal of the IGPL | 2012-06-08 | Paper |
Quantifier-free interpolation of a theory of arrays
Logical Methods in Computer Science | 2012-05-16 | Paper |
Rewriting-based quantifier-free interpolation for a theory of arrays
| 2012-04-24 | Paper |
A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints
Frontiers of Combining Systems | 2011-10-07 | Paper |
Automated Termination in Model Checking Modulo Theories
Lecture Notes in Computer Science | 2011-10-07 | Paper |
An algebraic approach to subframe logics. Modal case
Notre Dame Journal of Formal Logic | 2011-06-03 | Paper |
Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
Logical Methods in Computer Science | 2011-03-08 | Paper |
MCMT: a model checker modulo theories
Automated Reasoning | 2010-09-14 | Paper |
Algebraic and model theoretic techniques for fusion decidability in modal logics
| 2010-02-24 | Paper |
Goal-directed invariant synthesis for model checking modulo theories
Lecture Notes in Computer Science | 2009-12-01 | Paper |
Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
Automated Reasoning | 2009-03-12 | Paper |
Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
Automated Deduction – CADE-21 | 2009-03-06 | Paper |
Towards SMT Model Checking of Array-Based Systems
Automated Reasoning | 2008-11-27 | Paper |
Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies
Logics in Artificial Intelligence | 2008-10-30 | Paper |
Noetherianity and Combination Problems
Frontiers of Combining Systems | 2008-09-16 | Paper |
Conservative extensions in modal logic
| 2008-07-01 | Paper |
Decision procedures for extensions of the theory of arrays
Annals of Mathematics and Artificial Intelligence | 2007-10-23 | Paper |
Automated Reasoning
Lecture Notes in Computer Science | 2007-09-25 | Paper |
Connecting many-sorted theories
Journal of Symbolic Logic | 2007-07-09 | Paper |
An algebraic approach to subframe logics. Intuitionistic case
Annals of Pure and Applied Logic | 2007-06-25 | Paper |
Automated Deduction – CADE-20
Lecture Notes in Computer Science | 2006-11-01 | Paper |
A new combination procedure for the word problem that generalizes fusion decidability results in modal logics
Information and Computation | 2006-10-25 | Paper |
Frontiers of Combining Systems
Lecture Notes in Computer Science | 2006-10-10 | Paper |
Frontiers of Combining Systems
Lecture Notes in Computer Science | 2006-10-10 | Paper |
Filtering unification and most general unifiers in modal logic
Journal of Symbolic Logic | 2005-08-29 | Paper |
Model-theoretic methods in combined constraint satisfiability
Journal of Automated Reasoning | 2005-06-22 | Paper |
Unification, finite duality and projectivity in varieties of Heyting algebras
Annals of Pure and Applied Logic | 2004-08-06 | Paper |
scientific article; zbMATH DE number 1989653 (Why is no real title available?)
| 2003-10-09 | Paper |
Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics
Trends in Logic -- Studia Logica Library | 2003-09-08 | Paper |
Combining word problems through rewriting in categories with products
Theoretical Computer Science | 2003-07-29 | Paper |
scientific article; zbMATH DE number 1867302 (Why is no real title available?)
| 2003-06-21 | Paper |
A Resolution/Tableaux Algorithm for Projective Approximations in IPC
Logic Journal of the IGPL | 2003-02-25 | Paper |
On canonicity and strong completeness conditions in intermediate propositional logics
Studia Logica | 2001-03-19 | Paper |
Best solving modal equations
Annals of Pure and Applied Logic | 2000-12-06 | Paper |
Constructive canonicity in non-classical logics
Annals of Pure and Applied Logic | 2000-12-06 | Paper |
Unification in intuitionistic logic
Journal of Symbolic Logic | 1999-09-12 | Paper |
Model completions and r-Heyting categories
Annals of Pure and Applied Logic | 1998-05-11 | Paper |
Unification through projectivity
Journal Of Logic And Computation | 1998-03-25 | Paper |
Relational and partial variable sets and basic predicate logic
Journal of Symbolic Logic | 1997-04-24 | Paper |
scientific article; zbMATH DE number 868087 (Why is no real title available?)
| 1996-09-16 | Paper |
A sheaf representation and duality for finitely presented Heyting algebras
Journal of Symbolic Logic | 1996-05-13 | Paper |
Undefinability of propositional quantifiers in the modal system S4
Studia Logica | 1996-02-07 | Paper |
scientific article; zbMATH DE number 795162 (Why is no real title available?)
| 1995-12-13 | Paper |
An algebraic theory of normal forms
Annals of Pure and Applied Logic | 1995-03-22 | Paper |
scientific article; zbMATH DE number 496003 (Why is no real title available?)
| 1994-02-07 | Paper |
Quantified extensions of canonical propositional intermediate logics
Studia Logica | 1993-04-01 | Paper |
Incompleteness results in Kripke semantics
Journal of Symbolic Logic | 1992-06-27 | Paper |
Modal logics withn-ary connectives
Zeitschrift für Mathematische Logik und Grundlagen der Mathematik | 1990-01-01 | Paper |
Directed frames
Archive for Mathematical Logic | 1989-01-01 | Paper |
Presheaf semantics and independence results for some non-classical first- order logics
Archive for Mathematical Logic | 1989-01-01 | Paper |
scientific article; zbMATH DE number 4202257 (Why is no real title available?)
| 1988-01-01 | Paper |
scientific article; zbMATH DE number 4072929 (Why is no real title available?)
| 1988-01-01 | Paper |
scientific article; zbMATH DE number 3963825 (Why is no real title available?)
| 1986-01-01 | Paper |
scientific article; zbMATH DE number 3999891 (Why is no real title available?)
| 1985-01-01 | Paper |
scientific article; zbMATH DE number 3999892 (Why is no real title available?)
| 1985-01-01 | Paper |
scientific article; zbMATH DE number 4002091 (Why is no real title available?)
| 1985-01-01 | Paper |
A calculus for modal compact Hausdorff spaces
| N/A | Paper |
