21 citations · 36 across the 5 of their papers we have counts for
5 papers · 1 filter
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…
Sequent Calculus in the Topos of Trees
Ranald Clouston, Rajeev Goré
Nakano's "later" modality, inspired by Gödel-Löb provability logic, has been applied in type systems and program logics to capture guarded recursion. Birkedal et al modelled this m…
Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures
Alwen Tiu, Egor Ianovski, Rajeev Gore
A grammar logic refers to an extension to the multi-modal logic K in which the modal axioms are generated from a formal grammar. We consider a proof theory, in nested sequent calcu…
Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic
Rajeev Gore, Linda Postniece, Alwen Tiu
We consider an extension of bi-intuitionistic logic with the traditional modalities from tense logic Kt. Proof theoretically, this extension is obtained simply by extending an exis…
Optimal and Cut-free Tableaux for Propositional Dynamic Logic with Converse
Rajeev Goré, Florian Widmann
We give an optimal (EXPTIME), sound and complete tableau-based algorithm for deciding satisfiability for propositional dynamic logic with converse (CPDL) which does not require the…