Focusing is a general technique for syntactically compartmentalizing#R##N#the non-deterministic choices in a proof system, which not only#R##N#improves proof search but also has the representational benefit of#R##N#distilling sequent proofs into synthetic normal forms.  However, since#R##N#focusing is usually specified as a restriction of the sequent#R##N#calculus, the technique has not been transferred to logics that lack a#R##N#(shallow) sequent presentation, as is the case for some of the logics#R##N#of the modal cube.  We have recently extended the focusing technique#R##N#to classical nested sequents, a generalization of ordinary sequents.#R##N#In this work we further extend focusing to intuitionistic nested#R##N#sequents, which can capture all the logics of the intuitionistic S5#R##N#cube in a modular fashion.  We present an internal cut-elimination#R##N#procedure for the focused system which in turn is used to show its#R##N#completeness.
['Kaustuv Chaudhuri', 'Sonia Marin', 'Lutz Straßburger']
Modular Focused Proof Systems for Intuitionistic Modal Logics