39 citations · 60 across the 14 of their papers we have counts for
15 papers
Six Proofs of Interpolation for the Modal Logic K
Nick Bezhanishvili, Balder ten Cate, Rosalie Iemhoff
In this chapter, we present six different proofs of Craig interpolation for the modal logic K, each using a different set of techniques (model-theoretic, proof-theoretic, syntactic…
A Deep-Inference Sequent Calculus for Basic Propositional Team Logic (Without Delving Too Deep)
Aleksi Anttila, Rosalie Iemhoff, Fan Yang
We introduce a sequent calculus for the propositional team logic with both the split disjunction and the inquisitive disjunction consisting of a Gentzen-style system (G3-like) for…
Skolemization In Intermediate Logics
Matthias Baaz, Mariami Gamsakhurdia, Rosalie Iemhoff +1
Skolemization, with Herbrand's theorem, underpins automated theorem proving and various transformations in computer science and mathematics. Skolemization removes strong quantifier…
A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised
Ian Shillito, Iris van der Giessen, Rajeev Goré +1
We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong Löb logic , an intuit…
Universal Proof Theory, TACL 2022 Lecture Notes
Rosalie Iemhoff, Raheleh Jalali
These lecture notes survey the emerging area of Universal Proof Theory, which investigates general questions about the existence, equivalence, and characterization of good proof sy…
Logics and Admissible Rules of Constructive Set Theories
Rosalie Iemhoff, Robert Passmann
We survey the logical structure of constructive set theories and point towards directions for future research. Moreover, we analyse the consequences of being extensible for the log…
Proof Theory for Lax Logic
Rosalie Iemhoff
(A mistake has been discovered in this paper, implying that the main theorem stating that PLL has uniform interpolation cannot be considered proven (see Corollary 1 for the details…
Uniform Lyndon Interpolation for Basic Non-normal Modal and Conditional Logics
Amirhossein Akbar Tabatabai, Rosalie Iemhoff, Raheleh Jalali
In this paper, a proof-theoretic method to prove uniform Lyndon interpolation for non-normal modal and conditional logics is introduced and applied to show that the logics $\mathsf…
Uniform Lyndon interpolation for intuitionistic monotone modal logic
Amirhossein Akbar Tabatabai, Rosalie Iemhoff, Raheleh Jalali
In this paper we show that the intuitionistic monotone modal logic has the uniform Lyndon interpolation property (ULIP). The logic is a non-normal modal…
Reasoning in circles
Rosalie Iemhoff
Circular proofs, introduced by Daniyar Shamkanov, are proofs in which assumptions are allowed that are not axioms but do appear at least twice along a branch. Shamkanov has shown t…
The G4i analogue of a G3i calculus
Rosalie Iemhoff
This paper provides a method to obtain terminating analytic calculi for a large class of intuitionistic modal logics. For a given logic L with a cut-free calculus G that is an exte…
Proof Theory for Intuitionistic Strong Löb Logic
Iris van der Giessen, Rosalie Iemhoff
This paper introduces two sequent calculi for intuitionistic strong Löb logic : a terminating sequent calculus based on the terminating sequent c…
Logics of Intuitionistic Kripke-Platek Set Theory
Rosalie Iemhoff, Robert Passmann
We investigate the logical structure of intuitionistic Kripke-Platek set theory IKP, and show that the first-order logic of IKP is intuitionistic first-order logic IQC.
Questions and dependency in intuitionistic logic
Ivano Ciardelli, Rosalie Iemhoff, Fan Yang
In recent years, the logic of questions and dependencies has been investigated in the closely related frameworks of inquisitive logic and dependence logic. These investigations hav…
Structural completeness in propositional logics of dependence
Rosalie Iemhoff, Fan Yang
In this paper we prove that three of the main propositional logics of dependence (including propositional dependence logic and inquisitive logic), none of which is structural, are…