1 citations · 1 across the 3 of their papers we have counts for
4 papers · 1 filter
Uniform interpolation with constructive diamond
Iris van der Giessen, Ian Shillito
Uniform interpolation is a strong form of interpolation providing an interpretation of propositional quantifiers within a propositional logic. Pitts' seminal work establishes this…
Mechanised uniform interpolation for modal logics K, GL, and iSL
Hugo Férée, Iris van der Giessen, Sam van Gool +1
The uniform interpolation property in a given logic can be understood as the definability of propositional quantifiers. We mechanise the computation of these quantifiers and prove…
Intuitionistic Gödel-Löb logic, à la Simpson: labelled systems and birelational semantics
Anupam Das, Iris van der Giessen, Sonia Marin
We derive an intuitionistic version of Gödel-Löb modal logic () in the style of Simpson, via proof theoretic techniques. We recover a labelled system, , by…
A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised
Ian Shillito, Iris van der Giessen, Rajeev Goré +1
We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong Löb logic , an intuit…