3 papers
cs.LO2026
A decision procedure for intuitionistic modal logic IS4 (and IK4)
Marianna Girlando, Roman Kuznets, Sonia Marin +1
In this paper, we show that the two intuitionistic modal logics IS4 and IK4 are decidable. We provide a constructive decision procedure, that, given a formula, produces either a pr…
cs.LO2025
Proof Compression via Subatomic Logic and Guarded Substitutions
Victoria Barrett, Alessio Guglielmi, Benjamin Ralph +1
Subatomic logic is a recent innovation in structural proof theory where atoms are no longer the smallest entity in a logical formula, but are instead treated as binary connectives.…
cs.LO2025
Intuitionistic BV (Extended version)
Matteo Acclavio, Lutz Strassburger
We present the logic IBV, which is an intuitionistic version of BV, in the sense that its restriction to the MLL connectives is exactly IMLL, the intuitionistic version of MLL. For…