1 citations · 2 across the 8 of their papers we have counts for
9 papers
Intuitionistic Justification Logic, Semantically
Sonia Marin, Paaras Padhiar, Ian Shillito
Justification logics are explicit versions of modal logic. In the classical setting, this means boxes are refined with explicit proof terms and interact with each other through pro…
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…
Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM
Hugo Férée, Ian Shillito
Pitts' proof-theoretic technique for uniform interpolation, which generates uniform interpolants from terminating sequent calculi, has only been applied to logics on an intuitionis…
Duality for Constructive Modal Logics: from Sahqlvist to Goldblatt-Thomason
Jim de Groot, Ian Shillito, Ranald Clouston
We carry out a semantic study of the constructive modal logic CK. We provide a categorical duality linking the algebraic and birelational semantics of the logic. We then use this t…
Bi-intuitionistic logics through the abstract algebraic logic lens
Jonte Deakin, Ian Shillito
Since the discovery of critical mistakes in Rauszer's work on bi-intuitionistic logics, solid foundations for these have progressively been rebuilt. However, the algebraic treatmen…
Semantical Analysis of Intuitionistic Modal Logics between CK and IK
Jim de Groot, Ian Shillito, Ranald Clouston
The intuitionistic modal logics considered between Constructive K (CK) and Intuitionistic K (IK) differ in their treatment of the possibility (diamond) connective. It was recently…
Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents
Tim S. Lyon, Ian Shillito, Alwen Tiu
It is well-known that extending the Hilbert axiomatic system for first-order intuitionistic logic with an exclusion operator, that is dual to implication, collapses the domains of…
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…
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…