6 citations · 16 across the 12 of their papers we have counts for
14 papers
Interpolation in Proof Theory
Iris van der Giessen, Raheleh Jalali, Roman Kuznets
This chapter provides a comprehensive overview of proof-theoretic methods for establishing interpolation properties across a range of logics, including classical, intuitionistic, m…
Proof Complexity of Linear Logics
Amirhossein Akbar Tabatabai, Raheleh Jalali
Proving proof-size lower bounds for , the sequent calculus for classical propositional logic, remains one of the major open problems in proof complexity. We shed new l…
Feasibility of Primality in Bounded Arithmetic
Raheleh Jalali, Ondřej Ježil
We prove the correctness of the AKS algorithm \cite{AKS} within the bounded arithmetic theory or, equivalently, the first-order consequences of the theory exp…
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…
On the Completeness of Interpolation Algorithms
Stefan Hetzl, Raheleh Jalali
Craig interpolation is a fundamental property of classical and non-classic logics with a plethora of applications from philosophical logic to computer-aided verification. The quest…
Extensions of K5: Proof Theory and Uniform Lyndon Interpolation
Iris van der Giessen, Raheleh Jalali, Roman Kuznets
We introduce a Gentzen-style framework, called layered sequent calculi, for modal logic K5 and its extensions KD5, K45, KD45, KB5, and S5 with the goal to investigate the uniform L…
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…
Universal Proof Theory: Feasible Admissibility in Intuitionistic Modal Logics
Amirhossein Akbar Tabatabai, Raheleh Jalali
In this paper, we introduce a general family of sequent-style calculi over the modal language and its fragments to capture the essence of all constructively acceptable systems. Cal…
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…
Uniform interpolation via nested sequents and hypersequents
Iris van der Giessen, Raheleh Jalali, Roman Kuznets
A modular proof-theoretic framework was recently developed to prove Craig interpolation for normal modal logics based on generalizations of sequent calculi (e.g., nested sequents,…
Proof Complexity of Substructural Logics
Raheleh Jalali
In this paper, we investigate the proof complexity of a wide range of substructural systems. For any proof system at least as strong as Full Lambek calculus, $\mathbf{…
Universal Proof Theory: Semi-analytic Rules and Uniform Interpolation
Amirhossein Akbar Tabatabai, Raheleh Jalali
In \cite{Craig}, we introduced a syntactically defined and highly general class of calculi known as \emph{semi-analytic}. We then demonstrated that any sufficiently strong (modal)…
Universal Proof Theory: Semi-analytic Rules and Craig Interpolation
Amirhossein Akbar Tabatabai, Raheleh Jalali
We provide a general and syntactically-defined family of sequent calculi, called \emph{semi-analytic}, to formalize the informal notion of a "nice" sequent calculus. We show that a…