6 citations · 10 across the 13 of their papers we have counts for
13 papers
The logic of bunched implications is undecidable
Nick Galatos, Peter Jipsen, Søren Brinck Knudstorp +1
The logic of bunched implications (BI), introduced by O'Hearn and Pym (1999), has attracted significant attention due to its elegant proof calculus, varied semantics, and close con…
Hypersequent Calculi Have Ackermannian Complexity
A. R. Balasubramanian, Vitor Greati, Revantha Ramanayake
For substructural logics with contraction or weakening admitting cut-free sequent calculi, proof search was analyzed using well-quasi-orders on (Dickson's lemma), yi…
Predicative Ordinal Recursion on the Constructive Veblen Hierarchy
Amirhossein Akbar Tabatabai, Vitor Greati, Revantha Ramanayake
Inspired by Leivant's work on absolute predicativism, Bellantoni and Cook in 1992 introduced a structurally restricted form of recursion called predicative recursion. Using this re…
Complexities of Well-Quasi-Ordered Substructural Logics
Nikolaos Galatos, Vitor Greati, Revantha Ramanayake +1
Substructural logics are formal logical systems that omit familiar structural rules of classical and intuitionistic logic such as contraction, weakening, exchange (commutativity),…
Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof
Manfred Borzechowski, Malvin Gattinger, Helle Hvid Hansen +3
We show that Propositional Dynamic Logic (PDL) has the Craig Interpolation Property. This question has been open for many years. Three proof attempts were published, but later crit…
Deducibility in the full Lambek calculus with weakening is HAck-complete
Vitor Greati, Revantha Ramanayake
We prove that the problem of deciding the consequence relation of the full Lambek calculus with weakening is complete for the class HAck of hyper-Ackermannian problems (i.e., level…
Internal and External Calculi: Ordering the Jungle without Being Lost in Translations
Tim S. Lyon, Agata Ciabattoni, Didier Galmiche +5
This paper gives a broad account of the various sequent-based proof formalisms in the proof-theoretic literature. We consider formalisms for various modal and tense logics, intuiti…
Cut-restriction: from cuts to analytic cuts
Agata Ciabattoni, Timo Lang, Revantha Ramanayake
Cut-elimination is the bedrock of proof theory with a multitude of applications from computational interpretations to proof analysis. It is also the starting point for important me…
A theory of cut-restriction: first steps
Agata Ciabattoni, Timo Lang, Revantha Ramanayake
Cut-elimination is the bedrock of proof theory. It is the algorithm that eliminates cuts from a sequent calculus proof that leads to cut-free calculi and applications. Cut-eliminat…
Decidability and Complexity in Weakening and Contraction Hypersequent Substructural Logics
A. R. Balasubramanian, Timo Lang, Revantha Ramanayake
We establish decidability for the infinitely many axiomatic extensions of the commutative Full Lambek logic with weakening FLew (i.e. IMALLW) that have a cut-free hypersequent proo…
Display to Labeled Proofs and Back Again for Tense Logics
Agata Ciabattoni, Tim S. Lyon, Revantha Ramanayake +1
We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus f…
Inducing syntactic cut-elimination for indexed nested sequents
Revantha Ramanayake
The key to the proof-theoretic study of a logic is a proof calculus with a subformula property. Many different proof formalisms have been introduced (e.g. sequent, nested sequent,…
A syntactic proof of decidability for the logic of bunched implication BI
Revantha Ramanayake
The logic of bunched implication BI provides a framework for reasoning about resource composition and forms the basis for an assertion language of separation logic which is used to…