8 papers
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…
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…
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…
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: 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)…
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…