6 citations · 16 across the 12 of their papers we have counts for
8 papers · 1 filter
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…
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…
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,…
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…